α-同値
α-同値(α-equivalent) / α同値関係
ラムダ式内の束縛変数xを別の束縛変数yに置き換えても同値であるような関係
以下のようなやつ
(1)$ P =_α P \quad \mathrm{for\ all\ P }
(2) $ \lambda x.P =_α \lambda y.P[x:=y] \quad (\text{if}\ y \notin \mathrm{FV}(P))
$ P : 前項(pre-terms)の集合$ \Lambda^{-} の要素$ P
ref: 『Lectures on the Curry-Howard Isomorphism』 P2, 4
$ \lambda x. M = \lambda y[y/x] M \quad (y \notin FV(M))
$ FV(M) : ラムダ式$ M に含まれる自由変数の集合
確認用
Q. α-同値
参考
Sørensen, M. H. 『Lectures on the Curry-Howard Isomorphism』. 2013. P2, 4
大堀 淳. 『新装版 プログラミング言語の基礎理論』. 共立出版. 2019/08/13. P19
調査用
Google.icon α-同値(日)
Google.icon Α-equivalent(英)
Wikipedia.icon
α-同値 - Wikipedia(日)
α-同値(検索) - Wikipedia(日)
Wikipedia.icon
Α-equivalent - Wikipedia(英)
Α-equivalent(検索) - Wikipedia(英)
#自由変数の補足