問題タブ [lambda-calculus]

私は本The Lambda calculusの演習問題に取り組んでいます。私が立ち往生している質問の 1 つは、次のことを証明することです。アプリケーションが連想的でないことを示します。実際、x(yz) は (xy)z と等しくありません

これが私がこれまでに取り組んできたことです：

これは正しいです？理解を助けてください。

本Lambda Calculusの演習を続けると、問題は次のようになります。

λ微積分アルファベットの記号は常に幅 0.5cm であると仮定します。少なくとも (10^10)^10 光年の長さを持つ通常の形を持つ、長さが 20 cm 未満の λ 項を書き留めます。光の速度は c = 3 * (10^10) cm/秒です。

この質問で何をする必要があるかについては、まったくわかりません。質問とここで何をする必要があるかを理解するのに役立つヒントを教えてください。最終的な答えを解決したり言及したりしないでください。

返信を願っています。

よろしく、ダーキー

ラムダ式の場合、自由変数がどのように C コードに変換できる(x (λx y. x y) z h)かがわかりませんでした。x (outer x)zh

よろしく、ダーキー

このFinally Tagless EDSLでY-Combitorを表現する方法を見つけようとしています:

確かではありませんが、「lam」と「app」を使用して Y-Combinator のデフォルトの実装が可能になるはずです。

誰でも方法を知っていますか？「無限型を構築できない」という理由で、最初の試みは失敗します。

乾杯、ギュンター

全て、

以下は、削減するのが難しいと感じているラムダ式です。つまり、この問題の対処方法を理解できません。

(λm λn λa λb . m (nab) b) (λ f x. x) (λ f x. fx)

これは私が試したものですが、行き詰まっています：

上記の式を : (λm.E) M は
E= (λn λa λb. m (nab) b)
M = (λf x. x)(λ f x. fx) と等しくなります。

=> (λn λa λb. (λ f x. x) (λ f x. fx) (nab) b)

上記の式を (λn.E)M と考えると、
E = (λa λb. (λ f x. x) (λ f x. fx) (nab) b)
M = ??

..そして私は迷子になりました!!

任意のラムダ計算式の場合、リダクションを実行する手順はどうあるべきかを理解するのを手伝ってもらえますか?

SKI と BCKW の微積分の作成方法と考え方は理解できますが、実際の使用法を見つけることができません。多分私は十分に深く見ていませんか？つまり、Java サーブレットは S を広範囲に使用し、Python ジェネレーターは BCW の例であり、木の森を見通すことができないのだろうか?

http://muaddibspace.blogspot.com/2008/01/type-in​​ference -for-simply-typed-lambda.html は、Prolog の単純型付けラムダ計算の簡潔な定義です。

それは問題ないように見えますが、彼は Y コンビネータに型を割り当てることを主張しています... 一方、非常に現実的な意味で、ラムダ計算に型を追加する全体的な目的は、Y コンビネータのようなものに型を割り当てることを拒否することです。

彼の間違い、あるいはおそらく私の誤解がどこにあるのか、正確にわかる人はいますか?

私は SICP を使って作業していますが、問題 2.6によって私は困惑しています。チャーチ数を扱う場合、0 と 1 を特定の公理を満たす任意の関数にエンコードするという概念は理にかなっているように思われます。さらに、ゼロの定義と add-1 関数を使用して個々の数を直接定式化することは理にかなっています。プラス演算子を形成する方法がわかりません。

これまでのところ、私はこれを持っています。

lambda calculusのウィキペディアのエントリを調べたところ、 plus の定義は PLUS := λmnfx.mf (nfx) であることがわかりました。その定義を使用して、次の手順を定式化することができました。

私が理解していないのは、以前に派生したプロシージャによって提供された情報のみを使用して、そのプロシージャを直接派生させる方法です。厳密な証明のような形式でこれに答えることができる人はいますか? 直感的には何が起こっているのか理解できると思いますが、Richard Feynman がかつて言ったように、「構築できなければ、理解することはできません...」

I am writing a lambda calculus in F#, but I am stuck on implementing the beta-reduction (substituting formal parameters with the actual parameters).

example of usage:

So I'd love to hear some suggestions in regards to how others might go about this. Any ideas would be greatly appreciated.

Thanks!

F# を使用してラムダ計算を作成しています。私は現在、固定小数点演算子 (Y コンビネーターとも呼ばれます) を実装する方法を見つけようとして立ち往生しています。

それ以外は順調だと思います。式は、次の判別共用体で表されます。

私のeval機能はうまくいっているようです。次の例はすべて、期待どおりの結果をもたらします。
例 1:
> eval (Fun("x",Plus(Const 7,Var("x"))));;
val it : Expr = Fun ("x",Plus (Const 7,Var "x"))
例 2:
> eval (App(Fun("x",Plus(Const 7,Var("x"))),Const 3));;
val it : Expr = Const 10
例 3:
> eval (If(Const 0,Const 3,Const 4));;
val it : Expr = Const 4

しかし、前述したように、ラムダ計算内で固定小数点演算子を実装するのが困難です。ここでは次のように定義されています。
Y = lambda G. (lambda g. G(g g)) (lambda g. G(g g))

誰か提案はありますか？Yコンビネータに関する他の質問を見てきましたが、うまく採用できたものは見つかりませんでした。

すべての助けに感謝します。

編集：コードのタイプミスを修正しました...以前は、識別された組合のMult代わりに持っていました。Minusふと気がついたのがおかしい！