ベータ版のために以下の関数を定義しましたが、フリー変数が有界になるケースをどう考えるべきかはわかりません。Haskellを使ったラムダ計算のベータ縮小
data Term = Variable Char | Lambda Char Term | Pair Term Term deriving (Show,Eq)
--substition
s[M:x]= if (s=x) then M else s
AB[M:x]= (A[M:x] B [x:M])
Lambda x B[M:x] = Lambda x B
Lambda y P[M:x]= if x=y then Lambda y P else Lambda y P (M:x)
--beta reduction
Reduce [s]= s
Reduce[Lambda x B]M = B[M:x]
Reduce[L1 L2] = (Reduce [L1] Reduce [L2])
HAMMARコメントに与えたリンクは、詳細な解決策を説明します。
私は別のソリューションを提供したいと思います。 Nicolaas Govert de Bruijn、オランダの数学者、alternative notation for lambda termsを発明しました。考え方は、変数にシンボルを使用する代わりに、数値を使用するということです。変数をバインドする抽象概念が見つかるまで、各変数を交差させる必要のあるラムダの数を表す数で置き換えます。抽象化の後には、全く情報を持つ必要はありません。例えば：
λx. λy. x
λ λ 2
又は
λx. λy. λz. (x z) (y z)
に変換されるが
λ λ λ 3 1 (2 1)
に変換され、この表記は、いくつかの著しい利点を有します。特に、変数がないので、変数の名前の変更はなく、α変換はありません。置換する際にインデックスの番号を変更する必要がありますが、名前の競合をチェックしたり、名前を変更したりする必要はありません。上記のWikipediaの記事は、この表記法でβ低減がどのように機能するかの例を示しています。