ラムダ計算とコンビネータ論理を学んでいるが、コンビネータ代数やラムダ代数などの専門用語が出てきて、いつも分からなくなるので、メモ。
参考
The Lambda Calculus: Its Syntax and Semantics
H. P. Barendregt
5.1.1 定義 適用構造体
(i) もし、$\cdot$が${\bf X}$上の二項演算であれば、$\mathfrak{M}=({\bf X},\cdot)$は適用構造体(applicative structure)である。ちなみに$\mathfrak{M}$はドイツ旧字体の$M$である。
(ii) もしそのような構造体が$a,b\in{\bf X}$に対して次のことを満たせば、外延的(extensional)と呼ぶ。
$$(\forall x\in{\bf X}\quad a\cdot x=b\cdot x)\ \Rightarrow\ a=b$$
記述法について
(i) 代数として、$a\cdot b$は普通$ab$と書かれる。
もし$\vec{b}=b_1,b_2,\dots,b_n$ならば、
$a\vec{b}=ab_1\cdots b_n=(\cdots((ab_1)b_2)\cdots b_n)$となる。
5.1.2 定義
$\mathfrak{M}$を適用構造体する。
$\mathfrak{M}$上の項のある集合を$\mathscr{T}(\mathfrak{M})$と記述し、次のように帰納的に定義する：
$v_0,v_1,v_2,\dots\in\mathscr{T}(\mathfrak{M}),$ （変数）
$a\in\mathscr{T}(\mathfrak{M})\Rightarrow c_a\in\mathscr{T}(\mathfrak{M}),$ （定数）
$A,B\in\mathscr{T}(\mathfrak{M})\Rightarrow (AB)\in\mathscr{T}(\mathfrak{M})$
5.1.7 定義 コンビネータ代数
コンビネータ代数とは、次を満たす要素を持つ適用構造体$\mathfrak{M}=({\bf X},\cdot,k,s)$である。
$$k\cdot x\cdot y=x$$
$$s\cdot x\cdot y\cdot z=x\cdot z\cdot (y\cdot z)$$
ちなみに
$$i=s\cdot k\cdot k$$と定義する。
5.1.8 定義 コンビネータ代数の抽象化
$\mathfrak{M}$をコンビネータ代数とする。
(i) それぞれ$k, s$を指し示す新しい定数$K, S$で$\mathscr{T}(\mathfrak{M})$に拡張する。更に、$I=SKK$と定義する。
項$A\in\mathscr{T}(\mathfrak{M})$と変数$x$に対して、次のように帰納的に$\lambda^*x.A\in\mathscr{T}(\mathfrak{M})$を定義する：
$$\lambda^*x.x=I$$
$P$が$x$を含まないならば、$\lambda^*x.P=KP$
$$\lambda^*x.PQ=S(\lambda^*x.P)(\lambda^*x.Q)$$
5.2.2 定義 ラムダ代数
(i) コンビネータ代数は、もし、全ての$A, B\in\mathscr{T}(\mathfrak{M})$に対して次が成り立てば、ラムダ代数と呼ばれる。
$$\lambda\vdash A_\lambda=B_\lambda\ \Rightarrow\ \mathfrak{M}\vdash A=B $$
演習問題
Lambda-Calculus and Combinators: An Introduction
J. Roger Hindley, Jonathan P. Seldin (2008)
に演習問題があった。
演習問題 14.10
コンビネータ代数$\mathscr{T}(\mathfrak{M})\equiv(X,\cdot,i,k,s)$において原始要素$i,k,s$が異なることを示せ：
$$i\neq k\neq s\neq i$$
証明
コンビネータ代数は2つ以上の要素を持つ。
もし$i=k$あるいは$k=s$あるいは$s=i$の場合、全ての$d\in\mathscr{T}(\mathfrak{M})$に対して$d=i$となることを示したい。
- もし$i=k$ならば、全ての$c,d\in\mathscr{T}(\mathfrak{M})$に対して
$c\cdot d=(i\cdot c)\cdot d=(k\cdot c)\cdot d=c$
とくに$c=i$と置くと、$i\cdot d=i$となり、よって、
$$d=i\cdot d=i$$
全ての項$d\in\mathscr{T}(\mathfrak{M})$が$i$と等しくなるので、矛盾が生じた。
- もし$k=s$ならば、全ての$b,c,d\in\mathscr{T}(\mathfrak{M})$に対して
$b\cdot d=(k\cdot b\cdot c)\cdot d=(s\cdot b\cdot c)\cdot d=b\cdot d\cdot(c\cdot d)$
ここで$b=k\cdot i,\quad c=i$と置くと、
$i=k\cdot i\cdot d=b\cdot d=b\cdot d\cdot (c\cdot d)$
$=(k\cdot i)\cdot d\cdot(i\cdot d)=i\cdot d=d$
よって
$$d=i$$
同じく矛盾が生じる。
- もし$s=i$ならば、全ての$b,c,d\in\mathscr{T}(\mathfrak{M})$に対して
$b\cdot d\cdot (c\cdot d)=s\cdot b\cdot c\cdot d=i\cdot b\cdot c\cdot d=b\cdot c\cdot d$
ここで$b=k,\quad c=i$と置くと、
左辺：$=k\cdot d\cdot (i\cdot d)=d$
右辺：$b\cdot c\cdot d=k\cdot i\cdot d=i$
つまり、$$d=i$$
同じく矛盾が生じる。
従って、$i,k,s$はお互いに異なっている。