問題タブ [s-combinator]

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

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

どこ

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

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

私はラムダ計算を学び始めており、Erlang で I、S、K コンビネータを実装する必要があります。もちろん、S、K、I は次の略です。

S = λxyz.xz(yz) K = λxy.x I = λx.x

紙の上で I=SKK 変換を理解するのに問題はありません (ここで提示されているように: SKK と II がベータ版であることを証明するには、ラムダ計算です) が、関数型言語と高次関数に関しては理解できないようです。 ..

私はなんとか I と K を実行しました（モジュールで言ってみましょうtest）：

また、K x (K x) (SKK x = K x (K x)) の実行方法も知っています。

しかし、Sコンビネータを書くことはできません。私は試した：

それでも、SKK x を x に変換することはできません

私はこのように実行しようとします:

私は完全に迷っているので、助けていただければ幸いです。

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

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

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

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 誰か私が何を間違えたのか説明してくれませんか? ありがとうございました。

Sコンビネータのアナログは、標準関数のみを使用して (方程式で定義せずに)、ラムダ (無名関数) を使用せずに Haskell で表現できますか? のタイプであると期待してい(a -> b -> c) -> (a -> b) -> a -> cます。

たとえば、Kコンビネータの類似物はちょうどconstです。

実際、私は\f x -> f x x標準関数を使用して関数を表現しようとしていますが、最初から標準の非線形関数を考えることはできません(これは、その引数を複数回使用する関数です)。

フリップのラムダを 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

完全なソース