問題タブ [lambda-calculus]

計算モデルが同等であることをどのように証明できるかについての説明を求めています。同等性の証明が省略されていることを除いて、私はこの主題に関する本を読んでいます。2つの計算モデルが同等であるとはどういう意味かについての基本的な考え方があります（オートマトンビュー：同じ言語を受け入れる場合）。同等性について他の考え方はありますか？チューリングマシンモデルがラムダ計算と同等であることを証明する方法を理解するのを手伝っていただければ、それで十分です。

単純型付きラムダ計算で型付きラムダ計算が一意であるという証明は、紙の上では簡単です。私が精通しているという証拠は、タイピングの派生に関する完全な帰納法によって進められます。ただし、タイピング派生のタイプで表されるタイピング派生が一意であることを証明するのに苦労しています。dec Γ x τここで、変数のxタイプτがenvironmentの場合、述語はtrueですΓ。型付き述語Jは通常どおりに定義され、単純型付きラムダ計算の型付き規則を読み取るだけです。

Jタイピングの派生が一意であることを証明するときに、タイプの用語の構造を公開するのに問題があります。たとえば、私は次の補題のいずれd1かで誘導することはできますが、その後破壊して逆に誘導することはできません。Coqによって表示されるエラーメッセージ（用語を抽象化すると、タイプが正しくない用語になります）は少しわかりにくく、Coqwikiは何の助けにもなりません。参考までに、これは私が証明しようとしている見出語です。d2d1d2

タイプがユニークであることを証明するときなど、用語を導入するときに問題はありません。

編集：問題が発生した結果を示すために必要な最小限の定義を追加しました。huitseekerのコメントに応えて、J抽出などの操作を実行し、Coqでこれまで行ったことのない一意性などの結果を証明するために、派生を構造化オブジェクトとして入力することについて推論したかったので、この種が選択されました。

コメントの最初の部分に応じて、またはのinductionいずれd1かd2で実行できますが、実行後は、、、または残りの用語をinduction使用できません。これは、両方の構造を公開することはできず、両方のプルーフツリーについて推論することはできないことを意味します。私がそうしようとしたときに私が受け取るエラーは、残りの用語を抽象化すると、タイプが正しくない用語につながることを示しています。destructcaseinductiond1d2

ライブラリdependent inductionからいくつかの結果を試してみましたが、成功しませんでした。Coq.Logic派生がユニークであるということは、証明するのが簡単な命題であるように思われます。

私が質問を表現した愚かな方法については申し訳ありませんが、ここにいくつかの説明があります.javascriptでラムダ計算を試していますが、いくつかの小さな問題があります. (私を助けるためにラムダ計算について何も知る必要はありません)

私はこの機能を持っています（教会の数字1 btw）：

期待どおりに動作し、上記とまったく同じ結果が得られます。

予期せぬ動作をし、以下を与えます:

javascript が 'c' を関数 num1 に置き換えないのはなぜですか? しかし

与えます:

そして、最初の c が、実際には想定どおりに関数に置き換えられたことを示しています。「c」が置き換えられなかった場合、次のようになります。

全体として、コードは想定どおりに機能していますが、「c」が置き換えられた関数を出力していません。私に何ができる？後で、さらに関数を追加しますが、'c' が置き換えられないため、num1(asd)見分けることができなくなります。num1(jkl)

ご助力ありがとうございます！

だれも

Java で基本的なラムダ式操作 (できれば型付きラムダを使用) を行う予定です。

私が使用しているライブラリ (安定版またはそれ以外) はありますか?

更新: より明示的に述べると、ラムダ式を操作したい、たとえば、ファイル内でいくつかのラムダ式を解析し、それらのいくつかを組み合わせて新しい式を作成します。基本的に、それは関数型プログラミングというよりは構文解析です。

不滅の言葉をフィーチャーしたTシャツが販売されていたことを誓います。

のどの部分

分かりませんか？

私の場合、答えは...すべてです！

特に、Haskellの論文ではこのような表記がよく見られますが、それが何を意味するのかわかりません。数学のどの分野になっているのかわかりません。

もちろん、ギリシャ文字の文字と「∉」（通常、何かが集合の要素ではないことを意味します）などの記号を認識します。

一方、私はこれまで「⊢」を見たことがありません（ウィキペディアはそれが「パーティション」を意味するかもしれないと主張しています）。ここでの括線の使用にも慣れていません。（通常、それは分数を示しますが、ここではそうではないようです。）

誰かが少なくとも、このシンボルの海が何を意味するのかを理解するためにどこから始めればよいかを教えてくれるなら、それは役に立ちます。

Agdaでは、aのタイプはforall、次のすべてがタイプを持つように決定されますSet1（ここSet1で、はタイプであり、タイプSetはAタイプですSet）。

ただし、次のタイプは次のとおりSetです。

タイプがあった場合、矛盾が生じることは理解してSetいSetますが、上記の3つの用語のいずれかにタイプがあった場合、どのように矛盾が生じるかはわかりませSetん。それらを使用してFalseを証明できますか？それらを使用してそれを示すことができますSet : Setか？

これはアルファ変換です。これで完了しましたが、これが正解かどうかはよくわかりません。

これは正しい答えですか？

ラムダ用語は次のようになります。

• 変数
• ラムダ抽象化（たとえば\x.t）
• 応用。tとsがラムダ項の場合、tsはアプリケーションです。

したがって、左側の部分（たとえば(\x.t)a）に抽象化されたアプリケーションは見栄えがします。関数呼び出しのように見えます。しかし、左側が可変または他のアプリケーションである場合、アプリケーションはどういう意味ですか？はどういう意味ですかab、((\x.x)a)bまたは変数であるa(\x.x)場合はどうaなりますか？b

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

(λmn(λsz.ms(nsz)))(λsz.sz)(λsz.sz)

私はこれで迷っています。

誰かが私を正しい方向に導くことができれば、それは大歓迎です

Haskellのラムダ計算、特にチャーチ数で遊んでいます。私は次のように定義しています：

これは機能します：

これは発生チェックで失敗します：

私は自分の定数で遊んだことがありますが、それらは正しいようiszeroです。multこれを入力可能にする方法はありますか？自分のやっていることはあまりにもクレイジーだとは思いませんでしたが、何か間違ったことをしているのではないでしょうか。