람다 대수 (λ代數, 영어 : lambda calculus ) 또는 λ-대수 또는 람다 계산 (λ計算) 또는 람다 계산법 (λ計算法)은 추상화 와 함수 적용 등의 논리 연산 을 다루는 형식 체계 이다.[ 1] 람다 (λ)가 사용된다. 람다 대수의 항들에 대하여 알파 동치와 베타 축약 등의 연산을 수행할 수 있다. 알파 동치는 제한 변수를 변경하는 변환으로서 이름 충돌 을 방지하기 위해 사용되며, 드 브루인 첨수 를 사용할 경우 이는 필요 없다. 베타 축약은 함수 적용을 적절한 치환 연산 결과로 대신하는 변환이며, 베타 축약에 대한 주어진 항의 표준형이 (존재할 경우) 알파 동치 아래 유일하다는 사실은 처치-로서 정리 의 따름정리이다.
1930년대 알론조 처치 가 수학기초론 을 연구하는 과정에서 람다 대수의 형식을 제안하였다. 최초의 람다 대수 체계는 논리적인 오류가 있음이 증명되었으나, 처치가 1936년에 그 속에서 계산과 관련된 부분만 따로 빼내어 후에 유형 없는 람다 대수 라고 불리게 된 체계를 발표하였다. 또한 1940년에는 더 약한 형태이지만 논리적 모순이 없는 단순 유형 람다 대수 를 도입하였다.
람다 대수는 튜링 완전성 을 만족시키며, 보편 튜링 기계 와 동치이다. 람다 대수는 프로그래밍 언어 이론 에서 중요한 역할을 하며, 리스프 를 비롯한 함수형 프로그래밍 언어 의 기반이 된다. 람다 대수는 그 밖에도 논리학 , 철학 ,[ 2] 언어학 ,[ 3] [ 4] 컴퓨터 과학 [ 5]
람다 대수는 수학자 알론조 처치 에 의해 수학기초론 연구의 일환으로 1930년대 소개됐다.[ 6] [ 7] 스티븐 클레이니 와 존 버클리 로서 가 클리네-로저 역설 을 제창하면서 1935년 논리적 모순 을 보이기 위해 도입됐다.[ 8] [ 9]
그 후인 1936년 처치는 독립적으로 현재에는 유형 없는 람다 대수라고 불리는 계산에 관련한 부분을 출판했다.[ 10] 단순 유형 람다 대수 이다.[ 11]
1960년대에 람다 대수와 프로그래밍 언어의 관계가 명확히 밝혀지기 전까지는 λ-대수는 단지 형식주의 (formalism)일 뿐이었다. 감사하게도 리처드 몬터규 와 언어학자들이 λ-대수를 자연어 (natural language)의 의미론에 적용함으로써, λ-대수는 언어학과[ 12] [ 13]
함수 는 컴퓨터 과학 과 수학 의 기초를 이루는 개념이다. 람다 대수는 함수를 단순하게 표현할 수 있도록 하여 '함수의 계산'이라는 개념을 더 깊이 이해할 수 있게 돕는다.
예를 들어 항등 함수
I
(
x
)
=
x
{\displaystyle I(x)=x}
x
{\displaystyle x}
x
{\displaystyle x}
s
(
x
,
y
)
=
x
×
x
+
y
×
y
{\displaystyle s(x,y)=x\times x+y\times y}
x
{\displaystyle x}
y
{\displaystyle y}
함수가 반드시 이름을 가질 필요는 없다. 함수
s
{\displaystyle s}
(
x
,
y
)
↦
x
×
x
+
y
×
y
{\displaystyle (x,y)\mapsto x\times x+y\times y}
I
(
x
)
=
x
{\displaystyle I(x)=x}
x
↦
x
{\displaystyle x\mapsto x}
함수의 입력 변수의 이름 또한 필요 없다.
x
↦
x
{\displaystyle x\mapsto x}
y
↦
y
{\displaystyle y\mapsto y}
(
x
,
y
)
↦
x
×
x
+
y
×
y
{\displaystyle (x,y)\mapsto x\times x+y\times y}
(
u
,
v
)
↦
u
×
u
+
v
×
v
{\displaystyle (u,v)\mapsto u\times u+v\times v}
두 개 이상의 입력을 받는 함수는 하나의 입력을 받아 또다른 함수를 출력하는 함수로 다시 쓸 수 있다. 예를 들어,
(
x
,
y
)
↦
x
×
x
+
y
×
y
{\displaystyle (x,y)\mapsto x\times x+y\times y}
x
↦
(
y
↦
x
×
x
+
y
×
y
)
{\displaystyle x\mapsto (y\mapsto x\times x+y\times y)}
커링 (currying)
s
(
x
,
y
)
{\displaystyle s(x,y)}
(
x
↦
(
y
↦
x
×
x
+
y
×
y
)
)
(
5
)
(
2
)
{\displaystyle (x\mapsto (y\mapsto x\times x+y\times y))(5)(2)}
=
(
y
↦
5
×
5
+
y
×
y
)
(
2
)
{\displaystyle =(y\mapsto 5\times 5+y\times y)(2)}
=
5
×
5
+
2
×
2
{\displaystyle =5\times 5+2\times 2}
추상화:
λ
x
.
t
{\displaystyle \lambda x.t}
x
{\displaystyle x}
t
{\displaystyle t}
λ
x
.
x
2
+
2
{\displaystyle \lambda x.x^{2}+2}
f
(
x
)
=
x
2
+
2
{\displaystyle f(x)=x^{2}+2}
x
{\displaystyle x}
t
{\displaystyle t}
속박 된다.
자유 변수: 자유 변수(free variable)는 람다 추상화를 통해 표현에 묶이지 않은 변수를 말한다. 자유 변수의 집합은 귀납적으로 정의된다.
x
{\displaystyle x}
x
{\displaystyle x}
λ
x
.
t
{\displaystyle \lambda x.t}
x
{\displaystyle x}
t
{\displaystyle t}
두 표현
t
{\displaystyle t}
s
{\displaystyle s}
t
s
{\displaystyle ts}
t
{\displaystyle t}
s
{\displaystyle s}
예를 들어,
λ
x
.
x
{\displaystyle \lambda x.x}
λ
x
.
x
+
y
{\displaystyle \lambda x.x+y}
y
{\displaystyle y}
람다 대수의 언어는 변수, 상수, 람다 기호, 괄호, 온점으로 구성된다. 변수와 상수는 (후술할) 람다 항의 기초 구성원들이며, 람다 항에 등장하는 자유 변수는 (이후 정의할) 치환 연산을 통해 다른 람다 항으로 치환될 수 있다. 람다 기호는 (후술할) 추상화 연산을 나타내는 기호이다. 괄호와 온점은 이론적으로는 불필요하지만, 여러 가지 편의를 위해 사용된다. 구체적으로, 다음과 같은 데이터가 주어졌다고 하자.
가산 무한 정렬 전순서 집합
(
I
,
≤
)
{\displaystyle (I,\leq )}
I
{\displaystyle I}
최대 원소 를 갖지 않아야 한다.집합
J
{\displaystyle J}
J
=
∅
{\displaystyle J=\varnothing }
순수 람다 대수 (純粹λ代數, 영어 : pure lambda calculus )라고 한다. (여기서
I
{\displaystyle I}
(
I
,
J
)
{\displaystyle (I,J)}
각
i
∈
I
{\displaystyle i\in I}
x
i
{\displaystyle {\mathsf {x}}_{i}}
각
j
∈
J
{\displaystyle j\in J}
a
j
{\displaystyle {\mathsf {a}}_{j}}
람다 기호
λ
{\displaystyle \lambda }
괄호
(
)
{\displaystyle ()}
.
{\displaystyle .}
람다 항 (λ項, 영어 : lambda term )은 변수와 상수들로부터 시작하여 유한 차례 적용 및 추상화를 가하여 얻는, 람다 대수 기호들의 문자열이다. 즉, 이는 다음과 같은 문법을 따른다.
모든 변수와 상수는 람다 항이다.
두 람다 항
M
{\displaystyle M}
N
{\displaystyle N}
(
M
N
)
{\displaystyle (MN)}
N
{\displaystyle N}
M
{\displaystyle M}
적용 (適用, 영어 : application )이라고 한다.
람다 항
M
{\displaystyle M}
x
{\displaystyle x}
(
λ
x
.
M
)
{\displaystyle (\lambda x.M)}
x
{\displaystyle x}
M
{\displaystyle M}
추상화 (抽象化, 영어 : abstraction )라고 한다. 괄호 사용을 줄이기 위해 단순히
M
1
M
2
⋯
M
n
{\displaystyle M_{1}M_{2}\cdots M_{n}}
(
⋯
(
(
M
1
M
2
)
M
3
)
⋯
M
n
)
{\displaystyle (\cdots ((M_{1}M_{2})M_{3})\cdots M_{n})}
λ
x
.
M
1
⋯
M
n
{\displaystyle \lambda x.M_{1}\cdots M_{n}}
(
λ
x
.
(
⋯
(
(
M
1
M
2
)
M
3
)
⋯
M
n
)
)
{\displaystyle (\lambda x.(\cdots ((M_{1}M_{2})M_{3})\cdots M_{n}))}
λ
x
1
.
⋯
λ
x
n
.
M
{\displaystyle \lambda x_{1}.\cdots \lambda x_{n}.M}
λ
x
1
⋯
x
n
.
M
{\displaystyle \lambda x_{1}\cdots x_{n}.M}
(
λ
x
1
.
⋯
(
λ
x
n
−
1
.
(
λ
x
n
.
M
)
)
⋯
)
{\displaystyle (\lambda x_{1}.\cdots (\lambda x_{n-1}.(\lambda x_{n}.M))\cdots )}
x
{\displaystyle x}
y
{\displaystyle y}
z
{\displaystyle z}
λ
x
.
x
λ
x
.
λ
y
.
x
y
z
{\displaystyle \lambda x.x\lambda x.\lambda y.xyz}
는
(
λ
x
.
(
x
(
λ
x
.
(
λ
y
.
(
(
x
y
)
z
)
)
)
)
)
{\displaystyle (\lambda x.(x(\lambda x.(\lambda y.((xy)z)))))}
를 나타낸다.
람다 항에 등장하는 변수들은 자유 변수 (自由變數, 영어 : free variable )와 제한 변수 (制限變數, 영어 : bound variable )로 분류된다. 람다 항
M
{\displaystyle M}
x
{\displaystyle x}
M
{\displaystyle M}
x
{\displaystyle x}
M
{\displaystyle M}
λ
x
.
N
{\displaystyle \lambda x.N}
x
{\displaystyle x}
x
{\displaystyle x}
λ
x
.
N
{\displaystyle \lambda x.N}
x
{\displaystyle x}
M
{\displaystyle M}
FV
(
M
)
{\displaystyle \operatorname {FV} (M)}
M
{\displaystyle M}
변수
x
{\displaystyle x}
FV
(
x
)
=
{
x
}
{\displaystyle \operatorname {FV} (x)=\{x\}}
상수
a
{\displaystyle a}
FV
(
a
)
=
∅
{\displaystyle \operatorname {FV} (a)=\varnothing }
두 람다 항
M
{\displaystyle M}
N
{\displaystyle N}
FV
(
M
N
)
=
FV
(
M
)
∪
FV
(
N
)
{\displaystyle \operatorname {FV} (MN)=\operatorname {FV} (M)\cup \operatorname {FV} (N)}
람다 항
M
{\displaystyle M}
x
{\displaystyle x}
FV
(
λ
x
.
M
)
=
FV
(
M
)
∖
{
x
}
{\displaystyle \operatorname {FV} (\lambda x.M)=\operatorname {FV} (M)\setminus \{x\}}
람다 항
M
{\displaystyle M}
M
{\displaystyle M}
닫힌 람다 항 (닫힌λ項, 영어 : closed lambda term )이라고 한다.
예를 들어, 변수
x
{\displaystyle x}
y
{\displaystyle y}
z
{\displaystyle z}
(
λ
x
.
λ
y
.
x
y
z
)
x
{\displaystyle (\lambda x.\lambda y.xyz)x}
의 자유 변수의 집합은
{
x
,
z
}
{\displaystyle \{x,z\}}
{
y
}
{\displaystyle \{y\}}
주어진 람다 항에 등장하는 자유 변수를 또 다른 람다 항으로 치환 (置換, 영어 : substitution )하는 연산을 정의할 수 있다. 치환 연산의 정의는 자연스러우며, 다만 원래 람다 항의 의미가 변질되는 경우에는 알파 변환이 선행되어야 한다 (이는 아래 네 번째 조건의 세 번째 경우에 해당한다). 구체적으로, 람다 항
M
{\displaystyle M}
N
{\displaystyle N}
x
{\displaystyle x}
x
{\displaystyle x}
N
{\displaystyle N}
M
{\displaystyle M}
치환 실례 (置換實例, 영어 : substitution instance )
M
[
N
/
x
]
{\displaystyle M[N/x]}
M
{\displaystyle M}
변수
y
{\displaystyle y}
y
[
N
/
x
]
=
{
N
y
=
x
y
y
≠
x
{\displaystyle y[N/x]={\begin{cases}N&y=x\\y&y\neq x\end{cases}}}
상수
a
{\displaystyle a}
a
[
N
/
x
]
=
a
{\displaystyle a[N/x]=a}
람다 항
M
{\displaystyle M}
M
′
{\displaystyle M'}
(
M
M
′
)
[
N
/
x
]
=
(
M
[
N
/
x
]
)
(
M
′
[
N
/
x
]
)
{\displaystyle (MM')[N/x]=(M[N/x])(M'[N/x])}
람다 항
M
{\displaystyle M}
y
{\displaystyle y}
(
λ
y
.
M
)
[
N
/
x
]
=
{
λ
y
.
M
y
=
x
λ
y
.
(
M
[
N
/
x
]
)
(
y
≠
x
)
∧
(
y
∉
FV
(
N
)
∨
x
∉
FV
(
M
)
)
λ
z
.
(
M
[
z
/
y
]
[
N
/
x
]
)
(
y
≠
x
)
∧
(
y
∈
FV
(
N
)
∧
x
∈
FV
(
M
)
)
∧
(
z
=
min
{
w
∈
I
:
w
>
max
(
FV
(
M
)
∪
FV
(
N
)
)
}
)
{\displaystyle (\lambda y.M)[N/x]={\begin{cases}\lambda y.M&y=x\\\lambda y.(M[N/x])&(y\neq x)\land (y\not \in \operatorname {FV} (N)\lor x\not \in \operatorname {FV} (M))\\\lambda z.(M[z/y][N/x])&(y\neq x)\land (y\in \operatorname {FV} (N)\land x\in \operatorname {FV} (M))\land (z=\min\{w\in I\colon w>\max(\operatorname {FV} (M)\cup \operatorname {FV} (N))\})\end{cases}}}
예를 들어,
(
(
λ
x
.
λ
y
.
x
y
z
)
x
)
[
y
w
/
x
]
=
(
λ
x
.
λ
y
.
x
y
z
)
(
y
w
)
{\displaystyle ((\lambda x.\lambda y.xyz)x)[yw/x]=(\lambda x.\lambda y.xyz)(yw)}
(
(
λ
x
.
λ
y
.
x
y
z
)
x
)
[
y
w
/
z
]
=
(
λ
x
.
λ
v
.
x
v
y
w
)
x
(
v
=
min
{
u
∈
I
:
u
>
max
{
x
,
y
,
z
,
w
}
}
)
{\displaystyle ((\lambda x.\lambda y.xyz)x)[yw/z]=(\lambda x.\lambda v.xvyw)x\qquad (v=\min\{u\in I\colon u>\max\{x,y,z,w\}\})}
이다.
알파 동치 (α同値, 영어 : alpha equivalence )는 제한 변수 변경을 통해 주어진 람다 항을 새로운 람다 항으로 변환하는 방법이다. 람다 항
M
{\displaystyle M}
λ
x
.
P
{\displaystyle \lambda x.P}
P
{\displaystyle P}
y
{\displaystyle y}
λ
y
.
P
[
y
/
x
]
{\displaystyle \lambda y.P[y/x]}
N
{\displaystyle N}
M
{\displaystyle M}
N
{\displaystyle N}
알파 동치 라고 하며,
M
≡
α
N
{\displaystyle M\equiv _{\alpha }N}
예를 들어,
(
λ
x
.
x
y
)
(
λ
y
.
y
x
)
≡
α
(
λ
z
.
z
y
)
(
λ
y
.
y
x
)
≡
α
(
λ
z
.
z
y
)
(
λ
w
.
w
x
)
{\displaystyle {\begin{aligned}(\lambda x.xy)(\lambda y.yx)&\equiv _{\alpha }(\lambda z.zy)(\lambda y.yx)\\&\equiv _{\alpha }(\lambda z.zy)(\lambda w.wx)\\\end{aligned}}}
이다.
베타 축약 (β縮約, 영어 : beta reduction )은 추상화된 함수의 적용을 적절한 치환 실례로 바꾸는 것을 통해 람다 항을 변환하는 방법이다. 람다 항
M
{\displaystyle M}
(
λ
x
.
P
)
Q
{\displaystyle (\lambda x.P)Q}
P
[
Q
/
x
]
{\displaystyle P[Q/x]}
N
{\displaystyle N}
M
⊳
β
,
1
N
{\displaystyle M\vartriangleright _{\beta ,1}N}
M
{\displaystyle M}
N
{\displaystyle N}
N
{\displaystyle N}
M
{\displaystyle M}
베타 축약 이라고 하며,
M
⊳
β
N
{\displaystyle M\vartriangleright _{\beta }N}
다음 조건을 만족시키는 람다 항의 열
M
=
M
0
,
M
1
,
…
,
M
n
=
N
{\displaystyle M=M_{0},M_{1},\dots ,M_{n}=N}
임의의
k
∈
{
0
,
…
,
n
−
1
}
{\displaystyle k\in \{0,\dots ,n-1\}}
M
k
≡
α
M
k
+
1
{\displaystyle M_{k}\equiv _{\alpha }M_{k+1}}
M
k
⊳
β
,
1
N
k
+
1
{\displaystyle M_{k}\vartriangleright _{\beta ,1}N_{k+1}}
두 람다 항
M
{\displaystyle M}
N
{\displaystyle N}
M
{\displaystyle M}
N
{\displaystyle N}
베타 동치 (β同値, 영어 : beta equivalence )라고 하며,
M
≡
β
N
{\displaystyle M\equiv _{\beta }N}
다음 조건을 만족시키는 람다 항의 열
M
=
M
0
,
M
1
,
…
,
M
n
=
N
{\displaystyle M=M_{0},M_{1},\dots ,M_{n}=N}
임의의
k
∈
{
0
,
…
,
n
−
1
}
{\displaystyle k\in \{0,\dots ,n-1\}}
M
k
⊳
β
M
k
+
1
{\displaystyle M_{k}\vartriangleright _{\beta }M_{k+1}}
M
k
⊲
β
M
k
+
1
{\displaystyle M_{k}\vartriangleleft _{\beta }M_{k+1}}
(처치-로서 정리 )
M
⊳
β
P
{\displaystyle M\vartriangleright _{\beta }P}
N
⊳
β
P
{\displaystyle N\vartriangleright _{\beta }P}
P
{\displaystyle P}
람다 항
N
{\displaystyle N}
(
λ
x
.
P
)
Q
{\displaystyle (\lambda x.P)Q}
N
{\displaystyle N}
베타 표준형 (β標準型, 영어 : beta normal form )이라고 한다. 베타 표준형
N
{\displaystyle N}
M
{\displaystyle M}
M
⊳
β
N
{\displaystyle M\vartriangleright _{\beta }N}
N
{\displaystyle N}
M
{\displaystyle M}
베타 표준형 이라고 한다. 처치-로서 정리에 따라, 주어진 람다 항의 베타 표준형이 존재할 경우, 이는 (알파 동치를 무시하면) 유일하다.
N
{\displaystyle \mathbb {N} }
람다 대수의 언어를 사용하여 자연수 의 페아노 산술 을 다음과 같이 표현할 수 있다.
(처치 숫자, 영어 : Church numeral )
n
¯
=
λ
f
.
λ
x
.
f
n
x
(
n
∈
N
)
{\displaystyle {\bar {n}}=\lambda f.\lambda x.f^{n}x\qquad (n\in \mathbb {N} )}
plus
=
λ
m
.
λ
n
.
λ
f
.
λ
x
.
m
f
(
n
f
x
)
{\displaystyle \operatorname {plus} =\lambda m.\lambda n.\lambda f.\lambda x.mf(nfx)}
times
=
λ
m
.
λ
n
.
λ
f
.
λ
x
.
m
(
n
f
)
x
{\displaystyle \operatorname {times} =\lambda m.\lambda n.\lambda f.\lambda x.m(nf)x}
여기서
f
n
=
f
⋯
f
⏟
n
{\displaystyle f^{n}=\underbrace {f\cdots f} _{n}}
이다.
μ-재귀 함수 는 람다 대수의 언어를 사용하여 표현할 수 있다. 즉, 임의의 부분 재귀 함수
f
:
(
N
∙
)
d
→
N
∙
{\displaystyle f\colon (\mathbb {N} _{\bullet })^{d}\to \mathbb {N} _{\bullet }}
f
¯
{\displaystyle {\bar {f}}}
[ 1] :332, §43.8, Definition 276
N
∙
=
N
⊔
{
∙
N
}
{\displaystyle \mathbb {N} _{\bullet }=\mathbb {N} \sqcup \{\bullet _{\mathbb {N} }\}}
점을 가진 집합 이다.)
임의의
(
n
1
,
…
,
n
d
)
∈
N
∙
d
{\displaystyle (n_{1},\dots ,n_{d})\in \mathbb {N} _{\bullet }^{d}}
f
(
n
1
,
…
,
n
d
)
=
∙
N
{\displaystyle f(n_{1},\dots ,n_{d})=\bullet _{\mathbb {N} }}
f
¯
n
¯
1
⋯
n
¯
d
{\displaystyle {\bar {f}}{\bar {n}}_{1}\cdots {\bar {n}}_{d}}
임의의
(
n
1
,
…
,
n
d
)
∈
N
∙
d
{\displaystyle (n_{1},\dots ,n_{d})\in \mathbb {N} _{\bullet }^{d}}
f
(
n
1
,
…
,
n
d
)
∈
N
{\displaystyle f(n_{1},\dots ,n_{d})\in \mathbb {N} }
f
¯
n
¯
1
⋯
n
¯
d
{\displaystyle {\bar {f}}{\bar {n}}_{1}\cdots {\bar {n}}_{d}}
f
(
n
1
,
…
,
n
d
)
¯
{\displaystyle {\overline {f(n_{1},\dots ,n_{d})}}}
↑ 가 나 Mazzola, Guerino; Milmeister, Gérard; Weissmann, Jody (2005). 《Comprehensive Mathematics for Computer Scientists 2》. Universitext (영어). Berlin, Heidelberg: Springer. doi :10.1007/b138337 . ISBN 978-3-540-20861-7 LCCN 2004102307 . ↑ Coquand, Thierry, "Type Theory" , The Stanford Encyclopedia of Philosophy (Summer 2013 Edition), Edward N. Zalta (ed.).
↑ Moortgat, Michael (1988). 《Categorial Investigations: Logical and Linguistic Aspects of the Lambek Calculus》 . Foris Publications. ISBN 9789067653879 ↑ Bunt, Harry; Muskens, Reinhard, 편집. (2008), 《Computing Meaning》 , Springer, ISBN 9781402059575 ↑ Mitchell, John C. (2003), 《Concepts in Programming Languages》 , Cambridge University Press, 57쪽, ISBN 9780521780988 ↑ Church, A. (1932). “A set of postulates for the foundation of logic”. 《Annals of Mathematics》. Series 2 33 (2): 346–366. doi :10.2307/1968337 . JSTOR 1968337 . ↑ For a full history, see Cardone and Hindley's "History of Lambda-calculus and Combinatory Logic" (2006).
↑ Kleene, S. C. ; Rosser, J. B. (July 1935). “The Inconsistency of Certain Formal Logics”. 《The Annals of Mathematics》 36 (3): 630. doi :10.2307/1968646 . ↑ Church, Alonzo (December 1942). “Review of Haskell B. Curry, The Inconsistency of Certain Formal Logics ”. 《The Journal of Symbolic Logic》 7 (4): 170–171. doi :10.2307/2268117 . JSTOR 2268117 . ↑ Church, A. (1936). “An unsolvable problem of elementary number theory”. 《American Journal of Mathematics》 58 (2): 345–363. doi :10.2307/2371045 . JSTOR 2371045 . ↑ Church, A. (1940). “A Formulation of the Simple Theory of Types”. 《Journal of Symbolic Logic》 5 (2): 56–68. doi :10.2307/2266170 . JSTOR 2266170 . ↑ Partee, B. B. H.; ter Meulen, A.; Wall, R. E. (1990). 《Mathematical Methods in Linguistics》 . Springer. 2016년 12월 29일에 확인함 . ↑ Alama, Jesse "The Lambda Calculus" , The Stanford Encyclopedia of Philosophy (Summer 2013 Edition), Edward N. Zalta (ed.).
자유 변수와 종속 변수 문서를 참고하십시오.
![{\displaystyle M[N/x]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/85d0869688cae4f01602d967b629a45abb7834af)
![{\displaystyle y[N/x]={\begin{cases}N&y=x\\y&y\neq x\end{cases}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ddad88d27608d40e676520235521de3134ab0a3f)
![{\displaystyle a[N/x]=a}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f1f6c17fdf14c40af180473a08411e1cf803191f)
![{\displaystyle (MM')[N/x]=(M[N/x])(M'[N/x])}](https://wikimedia.org/api/rest_v1/media/math/render/svg/450dc80b62ac091b566e9d1768d841b3a4812f87)
![{\displaystyle (\lambda y.M)[N/x]={\begin{cases}\lambda y.M&y=x\\\lambda y.(M[N/x])&(y\neq x)\land (y\not \in \operatorname {FV} (N)\lor x\not \in \operatorname {FV} (M))\\\lambda z.(M[z/y][N/x])&(y\neq x)\land (y\in \operatorname {FV} (N)\land x\in \operatorname {FV} (M))\land (z=\min\{w\in I\colon w>\max(\operatorname {FV} (M)\cup \operatorname {FV} (N))\})\end{cases}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/1fd2c8b20f904250b00d3ee6da8cc42de4d48ee6)
![{\displaystyle ((\lambda x.\lambda y.xyz)x)[yw/x]=(\lambda x.\lambda y.xyz)(yw)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/8765d74dee8bf5ea722387c790475ae74d28384e)
![{\displaystyle ((\lambda x.\lambda y.xyz)x)[yw/z]=(\lambda x.\lambda v.xvyw)x\qquad (v=\min\{u\in I\colon u>\max\{x,y,z,w\}\})}](https://wikimedia.org/api/rest_v1/media/math/render/svg/8cc6b1421a9a1aa2b0054ac97903b0024b5d3a3d)
![{\displaystyle \lambda y.P[y/x]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/13a157d46e603fa5efddba7747b50c0b0334f2e7)
![{\displaystyle P[Q/x]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b5ff9e9e8795eaf3282205f351bdfd601aaf896a)
