Mathematica でコンビネータ {S,K,I} の通常のリダクション戦略を実装するにはどうすればよいですか? ルールは次のとおりです: S[x][y][z]->x[y][z[y]] K[x][y][z]->x
また、Y コンビネータ (固定小数点) があるため、Y[a]=a[Ya]] となります。
そして、たとえば S[K][K][a] = K[a][K[a]]=a のように式を「評価」する必要があります
削減の 1 つのステップを持つことが非常に重要です。このように、結果はアプリケーションの 1 つのステップで何度も..
提案をお待ちしております。
evalコンビネータ評価の 1 ステップを実行する関数を定義しましょう。まず、単一のステップを正確に構成するものを検討する必要があります。任意に、一番左の式を最初に評価し、そこから内側に向かって作業します。
ClearAll[eval]
eval[e_] := Module[{r = eval1[e]}, r /; r =!= e]
eval[e:f_[g_]] := Module[{r = eval[f][g]}, r /; r =!= e]
eval[e:f_[g_]] := Module[{r = f[eval[g]]}, r /; r =!= e]
eval[e_] := e
ルールは、実際に式が変更された場合にのみ適用されることに注意してください。これらの定義のぎこちなさは、Mathematica には、任意に長いカリー化された引数リストに一致するパターン式がないためです。
これで、認識されるコンビネータS、K、およびI を定義できます。
ClearAll[eval1]
eval1[s[f_][g_][h_]] := f[h][g[h]]
eval1[k[f_][_]] := f
eval1[i[f_]] := f
Iここでは主に Mathematicaが虚数単位である組み込み記号 をレンダリングする方法を避けるために，記号は小文字になっています．
その他のコンビネータは変数として扱われ、評価されません。
eval1[e_] := e
これで、基本的なケースを試すことができます。
i[f] // eval
(* f *)
k[f][g] // eval
(* f *)
s[f][g][h] // eval
(* f[h][g[h]] *)
evalAllさらに興味深いケースとして、評価チェーンのすべてのステップを示す を定義しましょう。
ClearAll[evalAll]
evalAll[e_, n_:Infinity] := FixedPointList[eval, e, n+1] // Most // Column
s[k][k][a] // evalAll
(*
s[k][k][a]
k[a][k[a]]
a
*)
s[s[m][n][r]][k[a][b]][c] // evalAll
(*
s[s[m][n][r]][k[a][b]][c]
s[m][n][r][c][k[a][b][c]]
m[r][n[r]][c][k[a][b][c]]
m[r][n[r]][c][a[c]]
*)
f[s[i[k]][k][g][i[f]]] // evalAll
(*
f[s[i[k]][k][g][i[f]]]
f[i[k][g][k[g]][i[f]]]
f[k[g][k[g]][i[f]]]
f[g[i[f]]]
f[g[f]]
*)
evalAllオプションの「count」引数を使用して、表示されるステップ数を制限します。これは、 Yコンビネータの直接式のような発散式に役立ちます。
eval1[y[f_]] := f[y[f]]
y[f] // evalAll[#, 4]&
(*
y[f]
f[y[f]]
f[f[y[f]]]
f[f[f[y[f]]]]
f[f[f[f[y[f]]]]]
*)
...しかし、そのようなシーケンスをSKIの観点から表現する方が楽しいです:
Module[{y = s[k[s[i][i]]][s[s[k[s]][k]][k[s[i][i]]]]}
, evalAll[y[f], 28]
]
(*
s[k[s[i][i]]][s[s[k[s]][k]][k[s[i][i]]]][f]
k[s[i][i]][f][s[s[k[s]][k]][k[s[i][i]]][f]]
s[i][i][s[s[k[s]][k]][k[s[i][i]]][f]]
i[s[s[k[s]][k]][k[s[i][i]]][f]][i[s[s[k[s]][k]][k[s[i][i]]][f]]]
s[s[k[s]][k]][k[s[i][i]]][f][i[s[s[k[s]][k]][k[s[i][i]]][f]]]
s[k[s]][k][f][k[s[i][i]][f]][i[s[s[k[s]][k]][k[s[i][i]]][f]]]
k[s][f][k[f]][k[s[i][i]][f]][i[s[s[k[s]][k]][k[s[i][i]]][f]]]
s[k[f]][k[s[i][i]][f]][i[s[s[k[s]][k]][k[s[i][i]]][f]]]
k[f][i[s[s[k[s]][k]][k[s[i][i]]][f]]][k[s[i][i]][f][i[s[s[k[s]][k]][k[s[i][i]]][f]]]]
f[k[s[i][i]][f][i[s[s[k[s]][k]][k[s[i][i]]][f]]]] <-- f[...]
f[s[i][i][i[s[s[k[s]][k]][k[s[i][i]]][f]]]]
f[i[i[s[s[k[s]][k]][k[s[i][i]]][f]]][i[i[s[s[k[s]][k]][k[s[i][i]]][f]]]]]
f[i[s[s[k[s]][k]][k[s[i][i]]][f]][i[i[s[s[k[s]][k]][k[s[i][i]]][f]]]]]
f[s[s[k[s]][k]][k[s[i][i]]][f][i[i[s[s[k[s]][k]][k[s[i][i]]][f]]]]]
f[s[k[s]][k][f][k[s[i][i]][f]][i[i[s[s[k[s]][k]][k[s[i][i]]][f]]]]]
f[k[s][f][k[f]][k[s[i][i]][f]][i[i[s[s[k[s]][k]][k[s[i][i]]][f]]]]]
f[s[k[f]][k[s[i][i]][f]][i[i[s[s[k[s]][k]][k[s[i][i]]][f]]]]]
f[k[f][i[i[s[s[k[s]][k]][k[s[i][i]]][f]]]][k[s[i][i]][f][i[i[s[s[k[s]][k]][k[s[i][i]]][f]]]]]]
f[f[k[s[i][i]][f][i[i[s[s[k[s]][k]][k[s[i][i]]][f]]]]]] <-- f[f[...]]
f[f[s[i][i][i[i[s[s[k[s]][k]][k[s[i][i]]][f]]]]]]
f[f[i[i[i[s[s[k[s]][k]][k[s[i][i]]][f]]]][i[i[i[s[s[k[s]][k]][k[s[i][i]]][f]]]]]]]
f[f[i[i[s[s[k[s]][k]][k[s[i][i]]][f]]][i[i[i[s[s[k[s]][k]][k[s[i][i]]][f]]]]]]]
f[f[i[s[s[k[s]][k]][k[s[i][i]]][f]][i[i[i[s[s[k[s]][k]][k[s[i][i]]][f]]]]]]]
f[f[s[s[k[s]][k]][k[s[i][i]]][f][i[i[i[s[s[k[s]][k]][k[s[i][i]]][f]]]]]]]
f[f[s[k[s]][k][f][k[s[i][i]][f]][i[i[i[s[s[k[s]][k]][k[s[i][i]]][f]]]]]]]
f[f[k[s][f][k[f]][k[s[i][i]][f]][i[i[i[s[s[k[s]][k]][k[s[i][i]]][f]]]]]]]
f[f[s[k[f]][k[s[i][i]][f]][i[i[i[s[s[k[s]][k]][k[s[i][i]]][f]]]]]]]
f[f[k[f][i[i[i[s[s[k[s]][k]][k[s[i][i]]][f]]]]][k[s[i][i]][f][i[i[i[s[s[k[s]][k]][k[s[i][i]]][f]]]]]]]]
f[f[f[k[s[i][i]][f][i[i[i[s[s[k[s]][k]][k[s[i][i]]][f]]]]]]]] <-- f[f[f[...]]]
*)