問題タブ [k-combinator]

私はラムダ計算が初めてで、次のことを証明するのに苦労しています。

SKK と II はベータ版に相当します。

どこ

S = ラムダ xyz.xz(yz) K = ラムダ xy.x I = ラムダ xx

SKKを開いてベータ削減しようとしましたが、どこにも行きませんでした。S、Kを拡張せずにSKKをさらに削減できるとは思わないでください.

Kコンビネータはで、K := (λxy.x)固定小数点コンビネータはY := λf.(λx.f x x) (λx.f x x)です。私は計算しようとしましたYK：

YKは の不動点だからですK:

任意の e。しかし、KIeに等しい必要がありますI!

Kコンビネータは定数関数であることを思い出してください。常に最初の引数を返します。

「モッキンバードをモックする」という本の中で、著者は話す鳥を含む魔法の森の例を示しています。鳥には行動があります：

鳥AとBがあれば、BからAの名前を呼び出すと、Aはあなたに鳥の名前を呼び出すことで応答します。この鳥はABによって指定されます。

森がA、B、Cの3羽の鳥で構成されているとします。少なくとも1羽の鳥がKコンビネータのように振る舞うことは可能ですか？

以下は、魔法の森の鳥の可能な行動のセットを示す表です。最初の列には、森の中の各鳥の名前があります。一番上の行には、各鳥に呼び出される可能性のある名前があります。体は名前に対する鳥の反応です。たとえば、鳥AにAの名前を呼び出すと、鳥AはCで応答します（行2、列2を参照）。簡潔に言えば、AA =Cです。鳥AにBの名前を呼び出すと、鳥AはBで応答します（行2、列3を参照）。簡潔に言えば、AB = Bです。ACの空のスロットにはどのような値を入れる必要がありますか？

鳥AをKコンビネータのように動作させることができるかどうかを見てみましょう。上記の値のセットは有望に見えます：

• すべてのyについてAA=CおよびCy=A。つまり、すべてのyに対して（AA）y=Aです。

• すべてのyについてAB=BおよびBy=B。つまり、すべてのyに対して（AB）y=Bです。

空のスロット（AC）にはどのような値を配置する必要がありますか？すべての場合を考慮してください：

• AC = Aの場合、Ayの値はすべてのyに対してCでなければなりませんが、これは明らかに誤りです。したがって、Aを空のスロットの正しい値にすることはできません。

• AC = Bの場合、Byの値はすべてのyに対してCでなければならず、これは明らかに誤りです。したがって、Bを空のスロットの正しい値にすることはできません。

• AC = Cの場合、Cyの値はすべてのyに対してCでなければなりませんが、これは明らかに誤りです。したがって、Cを空のスロットの正しい値にすることはできません。

したがって、すべてのyについて、条件（AC）y=Cを満たすために空のスロットに値を配置することはできません。

私の知る限り、鳥をKコンビネータのように振る舞わせることは不可能です。あなたが私を間違っていると証明してくれることを願っています。

ラムダと組み合わせ項を表すデータ型がいくつかあるとします。

ラムダ項の自由変数のリストを取得する関数もあります。

ラムダ項を組み合わせ項に変換するには、抽象的な排除規則が役立ちます。

1) T[x] => x

2) T[(E₁ E₂)] => (T[E₁] T[E₂])

3) T[λx.E] => (KT[E]) (E で x が自由に発生しない場合)

4) T[λx.x] => I

5) T[λx.λy.E] => T[λx.T[λy.E]] (x が E に自由に現れる場合)

6) T[λx.(E₁ E₂)] => (ST[λx.E₁] T[λx.E₂])

この定義は次の理由で有効ではありません5):

だから、私が今持っているものは次のとおりです。

私が欲しいのは（私がそれを正しく計算することを願っています）：

質問:

ラムダ項と組み合わせ項が異なるタイプの表現を持っている場合、どの5)ように定式化できますか?

こんにちは、これらのコンビネータ SK = KI の証明に問題があります

括弧 [] で囲まれた手順は、私が行っている手順を示しているだけです。たとえば、[λxy.x / x] in λyz.xz(yz) は、式 λyz.xz(yz) のすべての x を (λxy.x) に置き換えようとしていることを意味します。

私がこれまでに試したことはSKを減らすことであり、これを得ました：

そしてKIを減らすと、これが得られました：

2 つの答えは、私 (λyz.zz) と λy に等しくないように見えますが。λx.x 誰か私が何を間違えたのか説明してくれませんか? ありがとうございました。

私は最近 F# を取り上げており (私のバックグラウンドは C# です)、サイトhttp://fsharpforfunandprofit.comを読んでいます。

コンビネータのセクションであるhttp://fsharpforfunandprofit.com/posts/defining-functions/にアクセスしました。ケストレルを除いて、私はそれらすべてを理解しています（Yコンビネーターまたはセージバードは私の心を狂わせますが！）。Scott Wlaschin は (F# で) 次のように定義しています。

これが役立つ状況を一生理解することはできません。最初は、関数に値を渡してから元の値を取得できるように、チェーン演算子として使用できるのではないかと考えました。私は以前にそのような演算子を自分で書いたことがありますが、ご覧のとおり、同じではありません。

K コンビネータ (値 5) を部分的に適用すると、引数を無視して代わりに 5 を返す関数が返されます。これも役に立ちません。

これがどこで使用されるかの簡単な例を教えてください。

フリップのラムダを SKI コンビネータに変換するのに問題があります (意味があることを願っています)。これが私の変換です：

B、C、K、Wシステムで正しく理解すると、Cはフリップであり、SKI用語での定義は ですS (S (K (S (K S) K)) S) (K K)。明らかに、私の答えは C コンビネータと同じではありません...変換に使用したルールは次のとおりです。

私は何が欠けていますか？

単純に型指定されたラムダ計算型チェッカーを実装しようとしています。サニティ テストを実行しているときに (SKK) と入力しようとすると、型チェッカーが次のエラーをスローします。

TypeMismatch {firstType = t -> t, secondType = t -> t -> t}

問題のある用語は明らかに（SKK）です

(\x:t -> t -> t.\y:t -> t.\z:t.x z (y z)) (\x:t.\y:t.x) (\\x:t.\y:t.x)

この Haskell コードをタイプチェックすると正常に動作するため、ポリモーフィズムの欠如から問題が発生すると思います。

しかし、私がタイプを特化した場合:

参考までに、私の型システムは次のように単純です。

data Type = T | TArr Type Type

完全なソース

タップ関数 (K-Combinator とも呼ばれます) の関数シグネチャが以下にあることを本で読みました。

「この関数は、入力オブジェクト a と、a に対して何らかのアクションを実行する関数を受け取ります。指定されたオブジェクトで指定された関数を実行し、オブジェクトを返します。」

1. 関数シグネチャのアスタリスク (*) の意味を説明してくれる人はいますか?
2. 以下の実装は正しいですか？
3. 3 つの実装がすべて正しい場合、いつどれを使用する必要がありますか? 例はありますか？

実装 1:

実装 2:

実装 3: