組み合わせ論理(combinatory logic)の体系 CLw におけるCL−項の正規化を行います。
Javaアプリケーションです。
javacコマンドでコンパイル後、classファイルをjavaコマンドで起動します。
CL-項を入力するとw-正規形が出力されます。
!qと入力することで終了します。
変数 : x, y, z... (英小文字1字で表現)
定数 : K, S
- 変数と定数はCL-項 【原始】
MとNが共にCL-項ならば、(MN)もCL-項 【適用】
x, K, (xy), (K(xy)), (((S(xy))z)(K(xy))) は全てCL-項
括弧は、左から順に省略することができます。
(((S(xy))z)(K(xy))) → ((S(xy))z)(K(xy))
→ (S(xy))z(K(xy)) → S(xy)z(K(xy)) ※これ以上は省略できない
括弧を補う場合も左から順に付けていきます。
Sxyz → (Sx)yz → ((Sx)y)z → (((Sx)y)z)
基本定数S, K以外にも、以下のような定数があります。
全てSとKで表現し直すことができます。
【I】 I ≡ SKK
【B】 B ≡ S(KS)K
【C】 C ≡ S(BBS)(KK)
【W】 W ≡ SS(KI)
MとNがCL-項の時、下記3つの表現をCLwの式という。
M |>1 N
M |> N
M = N
公理とは、常に「正しい」と評価される式のことです。
算数でいうと、1 = 1は正しいので公理ですが、1 = 2は正しくないので公理ではありません。
公理の型を公理型といいます。
CLwの公理型は以下の3つです。M, N, RはCL−項とします。
【K】 KMN |>1 M
【S】 SMNR |>1 MR(NR)
【ρ】 M |> M
公理型を用いて、左辺のCL-項を右辺のCL-項に変形させることをweak変形といいます。
例えば、Kxyに公理型【K】を適用すると、Kxy |>1 xとなります。
すなわち、Kxyをweak変形させるとxになります。
weak変形はCL-項の一部分に適用させることもできます。
例えば、KxyzのKxyの部分に公理型【K】を適用し、xに変形します。
残ったzをくっつけると、xzになります。
すなわち、Kxyzをweak変形させるとxzになります。
ただし、一部分に適用させる場合は、注意が必要です。
例えば、xKyzのKyzには、公理型【K】は適用できません。
なぜなら、xKyzに括弧を補うと((xK)y)z)となり、Kyzは同じ固まりではないからです。
weak変形を繰り返し、これ以上変形できない形(w-正規形)まで変形することを正規化といいます。
S(Kx)yz |>1 Kxz(yz) |>1 x(yz)
1回目の変形では公理型【S】を適用しています。2回目の変形では公理型【K】を適用しています。
これはこれ以上変形できないため、S(Kx)yzのw-正規形はx(yz)となります。