型なしラムダ計算用のインタープリター(またはコンパイラー)はありますか?(このスレッドによると、それは可能です。)特に言語の多く(数字やブール演算子など)が(ユーザーまたはライブラリによって)実装されている場合は、プログラミング言語としてはほとんど役に立たないことを認識しています。言語自体。しかし、それでも微積分を学び、探索するのに役立つ楽しいツールになると思います。このため、コンパイラよりもインタプリタの方が望ましいでしょう。どちらでも機能します。誰かがそのようなプログラムを知っていますか?
7 に答える
ラムダ抽象化を持つ型指定されていない言語を使用できます。たとえば、Python や JavaScript です。主な欠点は 2 つあります。
- これらの言語には遅延評価がありません。これは、通常の形式であっても、すべてのラムダ項が収束するわけではないことを意味します。これを考慮して、それに応じてタスクを変更する必要があります。
- 結果は、通常の形式のラムダ項として表示されません。結果から何を期待するかを理解し、言語を使用してそれを表示できるものに評価する必要があります。
これを知った上で、Python で例を作りましょう: まず、数字と教会数字の間で変換するヘルパー関数を作成します:
# Construct Church numeral from an integer
def int2church(n):
def repeat(f, m, x):
if (m == 0): return x
else: return f(repeat(f, m-1, x))
return lambda f: (lambda x: repeat(f, n, x))
def church2int(l):
return l(lambda x: x + 1)(0)
これで、数値に対する標準操作を定義できます。
zero = int2church(0)
one = int2church(1)
pred = lambda n: lambda f: lambda x: n(lambda g: lambda h: h(g(f)))(lambda u: x)(lambda u: u)
mul = lambda m: lambda n: (lambda f: m(n(f)))
expn = lambda n: lambda m: m(n)
tetra = lambda n: lambda m: m(expn(n))(one)
たとえば4 3を計算します。
expn = lambda n: (lambda m: m(n))
a = int2church(4)
b = int2church(3)
print church2int(expn(a)(b))
またはテトレーション:
a = int2church(5)
b = int2church(2)
print church2int(tetra(a)(b))
さらに興味深いものを表現できるようにするために、Y コンビネータを定義できます。
y = lambda f: (lambda x: f(lambda v: x(x)(v))) (lambda x: f(lambda v: x(x)(v)))
たとえば、階乗を計算します。
true = lambda x: (lambda y: x)
false = lambda x: (lambda y: y)
iszero = lambda n: n(lambda x: false)(true)
fact = y(lambda r: lambda n: iszero(n)(one)(mul(n)(lambda x: r(pred(n))(x))))
print church2int(fact(int2church(6)))
Y コンビネータは、厳密な評価による無限再帰を避けるために、 η-expansionと階乗関数を使用した厳密な評価に適合させる必要があることに注意してください。
Benjamin Pierce は、彼の教科書「 Types and Programming Languages」に付随する、型なしおよび単純型付きの λ 計算の実装を提供しています。これらは OCaml で書かれており、定義例が含まれています。ただし、単純な λ 計算用のインタープリターまたはコンパイラーを作成することは難しくありません。
私は関数型プログラミングコースのティーチングアシスタントです。教育目的のために、このオンラインラムダ微積分レジューサーは、微積分を探求するための楽しくて便利なツールであると考えています。試してみたい場合は、SML のソース コードも利用できます。
いくつかのトリックを使用すると、ほとんどすべての関数型言語でこれを行うことができます。少なくとも、Haskell と OCaml でこのようなものを見たことがあります。ただし、型システムの制限を回避する必要がある場合もあります。通常、統一されたシステムとして実装することにより、「型指定のない」機能を取得します。したがって、各ラムダ関数には型があります
type lambda = lambda -> lambda
たとえばデフォルト設定では、OCaml はそのような再帰型を許可しませんが、たとえば次のように定義することで回避できます。
type lambda = L of lambda -> lambda
今年初めに書いた。 こちらです。
私は、ラムダ計算の仕組みを学ぶために、私がpureƒnと呼んでいるラムダ計算ベースの言語用のWeb ホスト型インタープリターを作成しました。表記の複雑さを最小限に抑えたインタラクティブな方法で、コンピューター サイエンスの基本原則の一部を学び、体験したい人にとっては役立つかもしれません。
pureƒnは、ラムダ計算の機能に基づくプログラミング環境ですが、表記が簡略化されています。pureƒnは、機能抽象化の定義、適用、削減を可能にします。表記法と構文は最小限ですが、基礎となる概念を簡単に理解できるようにするのに十分です。
基礎となるコンパイラは Python で記述されており、抽象化を相互に適用すると (可能であれば) 自動的に通常の形式に縮小する関数にコンパイルします。これは、S、K、および I コンビネータ関数を定義し、それらを SKK として適用すると、返される関数は I のように動作する関数だけでなく、I 関数になることを意味します。つまり、次のことが当てはまります。
>>>S(K)(K) is I
True
これはPythonで書かれたものです。非常に未熟に見えますが、1 つの Python を実装するという興味深いスタートです。モジュールによって異なりますply
。
これは、C++ 用の (一種の) 別のものです。非常に興味深いものです。
あなたの主な意図が、ラムダ計算 (たとえば、自分で算術演算を導出しようとする) と特定の教会の数とブール値の学習に関連する基本的な自動化を取得することである場合、原始的ですが実装が簡単な解決策は、自分自身を小さなものに制限することです。 Python のサブセットで、独自の Church 数字と演算子を定義し、それらを通常の Python 型に変換する関数でチェックできます。教会の数字に対してこれを行う関数:
lambda churchnum: churchnum(lambda x: x+1)(0)
そして、Church ブール値用の 1 つ:
lambda churchbool: churchbool(True)(False)