型なしラムダ計算で量化子を定義できるか

Question

型なしラムダ計算で量化子を定義できるか

私は型なしラムダ計算で2x=x+xが簡約した結果がtrueになるようにうまくxや=などを定義したいと思っています.(xは自然数) xを定義するためには量化子の定義が不可欠です。
しかし、型なしラムダ計算はチューリング完全なので量化子を定義できるはずなのですが、調べても見つかりません。どのようにすればいいか教えていただきたいです。

Comments

[Zuishin]

どのプログラミング言語の話でしょうか？
数学の問題ではありませんか？
またチューリング完全なら量化子を定義できるというところがどういう意味かよくわかりません。無関係のように見えます。

この質問の背景を明確にしてください。それによってはここではなく数学の掲示板で聞くべきことになると思います。

[milano]

どのプログラミング言語という話ではなく、型ありラムダ計算では、そもそも量化子をはじめから公理に加えているのですが、型なしラムダ計算はどんな数学の体系でも表せるので量化子をラムダ計算で定義できるのではないかと思いました。

[Zuishin]

ではここで聞くことではありませんね。

[milano]

わかりました

Answer 1

ラムダ計算をどのように勉強しているのか分からないのですが、おそらく誤解をしていると思われる箇所がいくつかあります。

• ラムダ計算では普通、関数のようなものは頭に置きます。2x=x+xのようなものを表現する時は、= (* 2 x) (+ x x)と書くのが一般的です。
• 単に簡約と言った時、普通はβ-reductionを指します。これは(λx.e) eみたいな形(β-redexと呼ぶ)のラムダ式を含んでいないとそれ以上簡約できません。
• 型無しラムダ計算と言えばみんな大体同じものを思い浮かべますが、型ありラムダ計算(型付きラムダ計算と言うのが一般的)と言うだけだと、いろいろ種類があって一つを特定できないです。
• 量化子を公理に加えているのは、型に関してのものであって、xと言う変数を量化するものではないです。勉強不足で自信はないですが。
• 型無しラムダ計算がチューリング完全と言うのは、church数とかを入出力としたときの話です。チューリング完全だと量化子を定義できるって話をどこで聞いたか分かりませんが、おそらく入力を量化式として処理をしても有限時間で計算が終わるとかそんな話だと思います。ですので、「だからラムダ式そのものを量化できる」とはならないです。ただ、「だから量化出来ない」ともならないので、もしかしたら　難しそうだけど上手いやり方はあるかもしれません。

うまくxや=などを定義したいとの事ですが、*や+の定義を考えてみるのはどうでしょう。
*はλm.λn.m (+ n) 0のようなコンビネータとして定義されます。

「=」をβ-equivalenceと捉えれば、
* 2 x
= (λm.λn.m (+ n) 0) 2 x
= (λn.2 (+ n) 0) x
= 2 (+ x) 0
= 1 (+ x) (+ x 0)
= 1 (+ x) x
= 0 (+ x x)
= + x x

だいぶ端折りましたが、これで* 2 x = + x xの証明自体は出来ます。

Comments

[milano]

ラムダ計算について誤解しているところがありました。指摘していただきありがとうございます。