問題タブ [lambda-calculus]

私はこのコードを取ることになっています：

そして、どこにも書き直さないでください（またはさせてください）。

Lambda関数で記述することを意味します（\ x-> ...）

HaskellでLambda関数を再利用しようとしています。何か案は？

ラムダ計算の定理としては、2つ以上の引数をとる関数を、1つの引数をとる関数のチェーンとしてカリー化することで記述できることがよく知られています。

これは、関数の動作を研究するだけでなく、実際の使用（Haskellなど）でも非常に強力であることが証明されています。

ただし、値を返す関数については説明されていないようです。プログラマーは通常、いくつかのメタオブジェクト（Rのリスト、C ++の構造など）を返すことにより、関数から複数の値を返すことができないことに対処します。それはいつもちょっとした悩みの種として私を襲ってきましたが、便利なものです。

例えば：

質問

1. ラムダ計算は、戻り値の多様性について何か言いたいことがありますか？もしそうなら、驚くべき結論が出ますか？
2. 同様に、どの言語でも真の複数の戻り値を許可していますか？

ウィキペディアよりもラムダキューブという用語をうまく説明できません。

[...] λ-cube は、単純に型付けされたラムダ計算を原点に配置された立方体の頂点として開始し、構成の微積分 (より高次の依存的に型付けされたポリモーフィック ラムダ計算) を正反対の頂点として使用します。立方体の各軸は、新しい形式の抽象化を表します。

• タイプに応じた用語、またはポリモーフィズム。システム F、別名 2 次ラムダ計算は、このプロパティのみを課すことによって得られます。
• 型に応じた型、または型演算子。型演算子 λω を使用した単純型付きラムダ計算は、このプロパティのみを課すことによって得られます。システム F と組み合わせると、システム Fω が得られます。
• 用語に依存する型、または依存型。このプロパティのみを課すと、LF に密接に関連する型システムである λΠ が生成されます。

8 つのすべての計算には、抽象化の最も基本的な形式、用語に依存する用語、単純型付けされたラムダ計算のような通常の関数が含まれます。3 つの抽象化をすべて備えた立方体で最も豊富な微積分は、構造の微積分です。8 つの計算はすべて、強力に正規化されています。

Java、Scala、Haskell、Agda、Coq などの言語で、この洗練されていない計算では達成できない各改良のコード例を見つけることは可能ですか?

型指定されていないラムダ計算で次のベータ削減が許可される理由がわかりません。

u具体的には、2 つのパラメーターをパーツ内のv1つのパラメーターに渡す方法を理解できません。上記を許可するには、カリー化を使用して2つのパラメーターを使用する必要はありませんか? このような-xλx.x

与えられた

と

(SKK) 形式または同等の拡張形式から開始した場合、同じ式 (SKK) の 2 つのベータ版の同等の形式が型なしラムダ計算で異なる結果をもたらす方法を理解できません。

圧縮された形式と展開された形式では括弧が異なるようです。実際、最初のものは次のように括弧で囲まれています。

2番目は次のようになります。

誰かがこれについて何か洞察を持っていますか??? ありがとうございました

型クラスで方程式（または関数宣言？）を見たことがありません。型クラスに方程式があるのはなぜですか？

私は_が何かに一致するための用語であることを知っています。しかし、どのm >> = \ _-> nが一致しますか？

ウィキペディアのラムダ計算の前任者関数の説明に行き詰まっています。

ウィキペディアには次のように書かれています。

誰かが削減プロセスを段階的に説明できますか?

ありがとう。

(これはこのサイトで既に回答されているはずですが、C の変数で free() を呼び出すという概念が検索に殺到します。)

f x = M x ==> Mx が「M でフリーでない」場合のように定義された「イータ リダクション」という用語に出くわしました。つまり、私はそれが言おうとしていることの要点を理解していると思います.関数をポイントフリースタイルに変換するときに何をするかのように見えますが、 x がフリーではないという修飾子が何を意味するのかわかりません.

私が読んでいるコンピュータープログラムの構造と解釈の本は、ゼロとインクリメント関数を定義することによって教会の数字を提示しています

これは私にはかなり複雑に思え、それを理解して 1 つ ( λf.λx. f x) と 2 つ( ) を導出するのに非常に長い時間がかかりましたλf.λx. f (f x)。

ゼロを空のラムダとして、代わりにこの方法で数値をエンコードする方がはるかに簡単ではないでしょうか?

λ. λこれで、1 つ ( ) と 2 つ( ) などを導出するのは簡単λ. λ. λです。

これは、ラムダで数値を表現するためのはるかに明白で直感的な方法のように思えます。このアプローチには何らかの問題があり、教会の数字がそのように機能する正当な理由がありますか? このアプローチはすでに証明されていますか?

高階関数を使用して、型指定されていないラムダ計算でさまざまな型をエンコードできます。

あまり一般的でないタイプを埋め込む研究が行われているかどうか疑問に思っていました。任意の型を埋め込むことができると主張する定理があれば素晴らしいでしょう。たとえば、kind * の型のみを埋め込むことができるなど、制限があるかもしれません。

あまり一般的ではないタイプを表現できるのであれば、例を見るのは素晴らしいことです。モナド型クラスのメンバーがどのように見えるかを特に知りたいです。