lambda-calculus

6熱

1答えて

ベータ版のために以下の関数を定義しましたが、フリー変数が有界になるケースをどう考えるべきかはわかりません。 data Term = Variable Char | Lambda Char Term | Pair Term Term deriving (Show,Eq) --substition s[M:x]= if (s=x) then M else s AB[M:x]= (A[M:x] B

5熱

1答えて

ラムダ計算、通常の順序、ノーマル形式、

ラムダ計算では、用語が正規形である場合、通常の順序削減戦略は常にそれを生成します。私はちょうど上記の命題を厳密に証明する方法を疑問に思っていますか？

2熱

1答えて

ラムダ計算（SML） - 私は教会の数字上の指数関数で理解しようとしている別の

に教会の番号を適用します。それには fun power m n f = n m f; を、私は掛け算を参照してください。乗算は： fun times m n f = m (n f); となり、私は間違っていることを知っています。問題は、どの機能が教会番号を別のものに適用するのか理解できないことです。たとえば、この式では何が生成されますか？ (fn x => fn y => x (x y

12熱

2答えて

関数式を解くための最先端の方法は何ですか？

では、次の式を満たすλ計算プログラム、T、見つけたいと仮定します。この場合には (T (λ f x . x)) = (λ a t . a) (T (λ f x . (f x))) = (λ a t . (t a)) (T (λ f x . (f (f x)))) = (λ a b t . (t a b)) (T (λ f x . (f (f (f x)))) = (λ a b c t

2熱

1答えて

バイナリラムダ計算の出力をモデル化する方法は？

私はJohn Tromp's binary lambda calculus のインタプリタを記述しようとしています、私は次の操作を行うためのコードを書かれている：ベータ減らす定期的に型指定されていないラムダ計算を表すいくつかのデータ構造にバイナリ入力をパースしますこの用語何が起こりますか？「出力」はどのように解釈されますか？が出力さ a）に戻って同じ符号を介してバイナリ翻訳結果の用語、

1熱

2答えて

ラムダ微積分/式の評価

ラムダ計算にはnotesを読んでいましたが、始めに式の1つを減らしたり評価したりするのに問題があります。特に、関数（λf.λx.f（f（x）））（λy.y^ 2）（5）。どのようにこれを正確に開始しますか？私の数学的な直感では、（λf.λx.f（f（x）））（5^2）のように進んでいて、f（x）はマップ X | - > X^2 ので、F（f（x）が）=（F）^ 2 = X^4 ので、更なる

5熱

1答えて

暗黙のパラメータはGHCのインライン化の難しさですか？

私は、キシコフとシャンによるFunctional Pearl: Implicit Configurationsの記事で説明されているimplicit parametersへの反対について不思議です。暗黙的なパラメータがあると、インラインコード（β-reduce）には聞こえません。本当に？ GHCは渡された暗黙のパラメータと同じ範囲にインラインする必要がありますか？用語の行動は、その署名の追加

1熱

2答えて

再帰ラムダ計算関数

が((x y)(x P)(P z))というようなラムダ微積分関数Pを作成したいと思います。私はYコンビネータ/チューリングコンビネータの変種、すなわち形λg.(g g)の関数を使用しようとしました。なぜなら、関数自体を再現する必要があるからですが、私は前方を見ることができません。どんな助けでも大歓迎です。

0熱

1答えて

よく入力された型の悪いラムダ用語

私は、適用されたラムダ計算を理解しようとしています。これまでは、型推論の仕組みを理解していました。しかし、私は、用語がよくタイプされているか、またはタイプミスであるということの意味に従うことができません。そして、どのタイプが適切なタイプのものか、タイプの悪いものかを決定する方法はありますか？たとえば、λ用語twをλx[(x x)]と定義します。どのようにそれはよく型付けされたまたは悪い型の用語で

6熱

1答えて

Binary Lambda Calculusはカッコをどのようにエンコードしますか？

BLCはカッコをどのようにエンコードしますか？たとえば、次のようになります。 λa.λb.λc.(a ((b c) d)) BLCでエンコードされますか？注：Wikipediaの記事はあまり知られていない表記法を使用しており、括弧を含まない単純な例と分析が難しい非常に複雑な例を提供しています。この論文は、その面で似ています。