람다 대수 문서 원본 보기

{{위키데이터 속성 추적}}
'''람다 대수'''(λ代數, {{llang|en|lambda calculus}}) 또는 '''λ-대수''' 또는 '''람다 계산'''(λ計算) 또는 '''람다 계산법'''(λ計算法)은 [[추상화 (컴퓨터 과학)|추상화]]와 함수 적용 등의 [[논리 연산]]을 다루는 [[형식 체계]]이다.<ref name="Mazzola">{{서적 인용
|성1=Mazzola
|이름1=Guerino
|성2=Milmeister
|이름2=Gérard
|성3=Weissmann
|이름3=Jody
|제목=Comprehensive Mathematics for Computer Scientists 2
|언어=en
|총서=Universitext
|출판사=Springer
|위치=Berlin, Heidelberg
|날짜=2005
|isbn=978-3-540-20861-7
|doi=10.1007/b138337
|lccn=2004102307
}}</ref> 람다 대수의 항은 변수와 추상화 및 적용 연산을 통해 구성되며 (비순수 람다 대수에서는 상수 역시 구성에 참여한다), 추상화의 기호로는 그리스 문자 [[람다]](λ)가 사용된다. 람다 대수의 항들에 대하여 알파 동치와 베타 축약 등의 연산을 수행할 수 있다. 알파 동치는 제한 변수를 변경하는 변환으로서 [[이름 충돌]]을 방지하기 위해 사용되며, [[드 브루인 첨수]]를 사용할 경우 이는 필요 없다. 베타 축약은 함수 적용을 적절한 치환 연산 결과로 대신하는 변환이며, 베타 축약에 대한 주어진 항의 표준형이 (존재할 경우) 알파 동치 아래 유일하다는 사실은 [[처치-로서 정리]]의 따름정리이다.

1930년대 [[알론조 처치]]가 [[수학기초론]]을 연구하는 과정에서 람다 대수의 형식을 제안하였다. 최초의 람다 대수 체계는 논리적인 오류가 있음이 증명되었으나, 처치가 1936년에 그 속에서 계산과 관련된 부분만 따로 빼내어 후에 [[유형 없는 람다 대수]]라고 불리게 된 체계를 발표하였다. 또한 1940년에는 더 약한 형태이지만 논리적 모순이 없는 [[단순 유형 람다 대수]]를 도입하였다.

람다 대수는 [[튜링 완전성]]을 만족시키며, [[보편 튜링 기계]]와 동치이다. 람다 대수는 [[프로그래밍 언어 이론]]에서 중요한 역할을 하며, [[리스프]]를 비롯한 [[함수형 프로그래밍 언어]]의 기반이 된다. 람다 대수는 그 밖에도 [[논리학]], [[철학]],<ref>Coquand, Thierry, [http://plato.stanford.edu/archives/sum2013/entries/type-theory/ "Type Theory"], ''The Stanford Encyclopedia of Philosophy'' (Summer 2013 Edition), Edward N. Zalta (ed.).</ref> [[언어학]],<ref>{{서적 인용|url=https://books.google.com/books?id=9CdFE9X_FCoC |title=Categorial Investigations: Logical and Linguistic Aspects of the Lambek Calculus |first=Michael |last=Moortgat |publisher=Foris Publications |year=1988 |isbn=9789067653879}}</ref><ref>{{인용|url=https://books.google.com/books?id=nyFa5ngYThMC |title=Computing Meaning |editor1-first=Harry |editor1-last=Bunt |editor2-first=Reinhard |editor2-last=Muskens |publisher=Springer |year=2008 |isbn=9781402059575}}</ref> [[컴퓨터 과학]]<ref>{{인용|title=Concepts in Programming Languages|first=John C.|last=Mitchell|publisher=Cambridge University Press|year=2003|isbn=9780521780988|page=57|url=https://books.google.com/books?id=7Uh8XGfJbEIC&pg=PA57}}</ref> 등의 여러 분야에서 응용된다.

== 역사 ==
람다 대수는 수학자 [[알론조 처치]]에 의해 [[수학기초론]] 연구의 일환으로 1930년대 소개됐다.<ref>{{저널 인용|first=A. |last=Church |authorlink=알론조 처치 |title=A set of postulates for the foundation of logic |journal=Annals of Mathematics |series=Series 2 |volume=33 |issue=2 |pages=346–366 |year=1932 |doi=10.2307/1968337 |jstor=1968337}}</ref><ref>For a full history, see Cardone and Hindley's "History of Lambda-calculus and Combinatory Logic" (2006).</ref> 최초의 시스템은 [[스티븐 클레이니]]와 [[존 버클리 로서]]가 [[클리네-로저 역설]]을 제창하면서 1935년 [[무모순성|논리적 모순]]을 보이기 위해 도입됐다.<ref>{{저널 인용|last1=Kleene|first1=S. C.|authorlink1=스티븐 클레이니|last2=Rosser|first2=J. B.|authorlink2=존 버클리 로서|title=The Inconsistency of Certain Formal Logics|url=https://archive.org/details/sim_annals-of-mathematics_1935-07_36_3/page/n24|journal=The Annals of Mathematics|date=July 1935|volume=36|issue=3|pages=630|doi=10.2307/1968646}}</ref><ref>{{저널 인용|last=Church|first=Alonzo|authorlink=알론조 처치|title=Review of Haskell B. Curry, ''The Inconsistency of Certain Formal Logics''|journal=The Journal of Symbolic Logic|date=December 1942|volume=7|issue=4|pages=170–171|doi=10.2307/2268117|jstor=2268117}}</ref>

그 후인 1936년 처치는 독립적으로 현재에는 유형 없는 람다 대수라고 불리는 계산에 관련한 부분을 출판했다.<ref>{{저널 인용|first=A. |last=Church |authorlink=알론조 처치 |title=An unsolvable problem of elementary number theory |url=https://archive.org/details/sim_american-journal-of-mathematics_1936-04_58_2/page/n107 |journal=American Journal of Mathematics |volume=58 |number=2 |year=1936 |pages=345–363 |doi=10.2307/2371045 |jstor=2371045 }}</ref> 1940년, 그는 또한 계산적으로는 떨어지지만 논리적으로 무결한 시스템을 공개했다. 이것이 [[단순 유형 람다 대수]]이다.<ref>{{저널 인용| last1 = Church | authorlink=알론조 처치 | first1 = A. | year = 1940 | title = A Formulation of the Simple Theory of Types | journal = Journal of Symbolic Logic | volume = 5 | issue = 2 | pages = 56–68 | doi=10.2307/2266170 |jstor=2266170}}</ref>

1960년대에 람다 대수와 프로그래밍 언어의 관계가 명확히 밝혀지기 전까지는 λ-대수는 단지 형식주의 (formalism)일 뿐이었다. 감사하게도 [[리처드 몬터규]]와 언어학자들이 λ-대수를 자연어 (natural language)의 의미론에 적용함으로써, λ-대수는 언어학과<ref name='mm-linguistics'>{{서적 인용|last1=Partee|first1=B. B. H.|last2=ter Meulen|first2=A.|last3=Wall|first3=R. E.|title=Mathematical Methods in Linguistics |url=https://books.google.com/books?id=qV7TUuaYcUIC&pg=PA317 |accessdate=29 Dec 2016|year=1990|publisher=Springer}}</ref>컴퓨터 과학<ref>Alama, Jesse [http://plato.stanford.edu/entries/lambda-calculus/ "The Lambda Calculus"], ''The Stanford Encyclopedia of Philosophy'' (Summer 2013 Edition), Edward N. Zalta (ed.).</ref> 양쪽 분야에서 인정받는 위치를 차지했다.

== 도입 ==
=== 함수의 표현 ===
[[함수]]는 [[컴퓨터 과학]]과 [[수학]]의 기초를 이루는 개념이다. 람다 대수는 함수를 단순하게 표현할 수 있도록 하여 '함수의 계산'이라는 개념을 더 깊이 이해할 수 있게 돕는다.

예를 들어 항등 함수 <math>I(x) = x</math>는 하나의 입력 <math>x</math>를 받아 다시 <math>x</math>를 결과로 내놓는다고 하자. 한편 함수 <math>s(x, y) = x \times x + y \times y</math>는 입력 <math>x</math>와 <math>y</math>를 받아 두 수의 제곱의 합을 내놓는다고 하자. 이 두 예제로부터 세 가지 유용한 사실을 알 수 있다.
# 함수가 반드시 이름을 가질 필요는 없다. 함수 <math>s</math>는 이름을 제거하고 <math>(x, y) \mapsto x \times x + y \times y</math> 와 같은 형태로 쓸 수 있다. 또한 항등 함수 <math>I(x) = x</math>는 <math>x \mapsto x</math>의 형태로 쓸 수 있다.
# 함수의 입력 변수의 이름 또한 필요 없다. <math>x \mapsto x</math> 와 <math>y \mapsto y</math>는 변수의 이름은 다르지만 같은 항등 함수를 의미한다. 또한 <math>(x, y) \mapsto x \times x + y \times y</math> 와 <math>(u, v) \mapsto u \times u + v \times v</math>는 같은 함수를 나타낸다.
# 두 개 이상의 입력을 받는 함수는 하나의 입력을 받아 또다른 함수를 출력하는 함수로 다시 쓸 수 있다. 예를 들어, <math>(x, y) \mapsto x \times x + y \times y</math>는 <math>x \mapsto (y \mapsto x \times x + y \times y)</math> 와 같은 형태로 다시 쓸 수 있다. 함수를 이와 같이 변환하는 것을 ''[[커링]] (currying)''이라고 한다. 위의 함수 <math>s(x,y)</math>는 다음과 같이 단일 입력 함수를 두 번 적용하는 것으로 이해할 수 있다.
<blockquote><math>( x \mapsto (y \mapsto x \times x + y \times y) ) (5) (2)</math><br /><math>= (y \mapsto 5 \times 5 + y \times y) (2)</math><br /><math>= 5 \times 5 + 2 \times 2</math></blockquote>

=== 핵심 개념 ===
추상화: <math>\lambda x.t</math>는 단일 입력 <math>x</math>를 받아 <math>t</math>의 표현으로 치환하는 익명의 함수를 지칭한다. 예를 들어 <math>\lambda x.x^2+2</math>는 함수 <math>f(x)=x^2+2</math>의 람다 추상화이다. 람다 추상화를 통해 함수를 정의한다는 것은 함수를 정의하기만 하고 함수를 수행(호출)하지는 않는다는 것을 의미한다. 람다 추상화를 통해 변수 <math>x</math>는 표현 <math>t</math>에 [[자유변수와 속박변수|속박]]된다.

자유 변수: 자유 변수(free variable)는 람다 추상화를 통해 표현에 묶이지 않은 변수를 말한다. 자유 변수의 집합은 귀납적으로 정의된다.
* <math>x</math>의 자유 변수는 <math>x</math>뿐이다.
* <math>\lambda x.t</math>의 자유변수는 <math>x</math>를 제외하고 <math>t</math>에 등장하는 변수들이다.
* 두 표현 <math>t</math>와 <math>s</math>의 결합 <math>ts</math>의 자유변수의 집합은 <math>t</math>의 자유변수의 집합과 <math>s</math>의 자유변수의 집합의 합집합이다.
예를 들어, <math>\lambda x.x</math>에는 자유 변수가 없지만, <math>\lambda x.x+y</math>에는 자유변수가 <math>y</math> 하나이다.

== 정의 ==
람다 대수의 언어는 변수, 상수, 람다 기호, 괄호, 온점으로 구성된다. 변수와 상수는 (후술할) 람다 항의 기초 구성원들이며, 람다 항에 등장하는 자유 변수는 (이후 정의할) 치환 연산을 통해 다른 람다 항으로 치환될 수 있다. 람다 기호는 (후술할) 추상화 연산을 나타내는 기호이다. 괄호와 온점은 이론적으로는 불필요하지만, 여러 가지 편의를 위해 사용된다. 구체적으로, 다음과 같은 데이터가 주어졌다고 하자.
* [[가산 무한]] [[정렬 전순서 집합]] <math>(I,\le)</math>. 또한 <math>I</math>는 [[최대 원소]]를 갖지 않아야 한다.
* 집합 <math>J</math> 만약 <math>J=\varnothing</math>일 경우, 이 람다 대수를 '''순수 람다 대수'''(純粹λ代數, {{llang|en|pure lambda calculus}})라고 한다.
(여기서 <math>I</math>가 최대 원소를 갖지 않는 정렬 전순서 집합이어야 하는 것은 치환의 정의에서 주어진 모든 변수들보다 큰 변수들의 집합의 최소 원소를 취할 수 있어야 하기 때문이다.) 그렇다면, <math>(I,J)</math>에 대한 람다 대수의 언어는 다음과 같은 기호들로 구성된다.
* 각 <math>i\in I</math>에 대하여, 변수 <math>\mathsf x_i</math>
* 각 <math>j\in J</math>에 대하여, 상수 <math>\mathsf a_j</math>
* 람다 기호 <math>\lambda</math>
* 괄호 <math>()</math> 및 온점 <math>.</math>

'''람다 항'''(λ項, {{llang|en|lambda term}})은 변수와 상수들로부터 시작하여 유한 차례 적용 및 추상화를 가하여 얻는, 람다 대수 기호들의 문자열이다. 즉, 이는 다음과 같은 문법을 따른다.
* 모든 변수와 상수는 람다 항이다.
* 두 람다 항 <math>M</math>, <math>N</math>에 대하여, 문자열 <math>(MN)</math>은 람다 항이다. 이를 <math>N</math>에 대한 <math>M</math>의 '''적용'''(適用, {{llang|en|application}})이라고 한다.
* 람다 항 <math>M</math> 및 변수 <math>x</math>에 대하여, 문자열 <math>(\lambda x.M)</math>은 람다 항이다. 이를 <math>x</math>에 대한 <math>M</math>의 '''추상화'''(抽象化, {{llang|en|abstraction}})라고 한다.

괄호 사용을 줄이기 위해 단순히 <math>M_1M_2\cdots M_n</math>은 <math>(\cdots((M_1M_2)M_3)\cdots M_n)</math>을 나타내고, <math>\lambda x.M_1\cdots M_n</math>은 <math>(\lambda x.(\cdots((M_1M_2)M_3)\cdots M_n))</math>을, <math>\lambda x_1.\cdots\lambda x_n.M</math> (또는 <math>\lambda x_1\cdots x_n.M</math>)은 <math>(\lambda x_1.\cdots(\lambda x_{n-1}.(\lambda x_n.M))\cdots)</math>을 나타내는 데 사용할 수 있다. 예를 들어, 변수 <math>x</math>, <math>y</math>, <math>z</math>에 대하여,
:<math>\lambda x.x\lambda x.\lambda y.xyz</math>
는
:<math>(\lambda x.(x(\lambda x.(\lambda y.((xy)z)))))</math>
를 나타낸다.

== 연산 ==
=== 자유 변수와 제한 변수 ===
{{참고|자유 변수와 종속 변수}}
람다 항에 등장하는 변수들은 '''자유 변수'''(自由變數, {{llang|en|free variable}})와 '''제한 변수'''(制限變數, {{llang|en|bound variable}})로 분류된다. 람다 항 <math>M</math>과 변수 <math>x</math>에 대하여, 만약 <math>M</math>에 등장하는 모든 <math>x</math>가 <math>M</math> 속 <math>\lambda x.N</math>과 같은 꼴의 부분 람다 항에 등장한다면 <math>x</math>는 제한 변수이며, 만약 적어도 한 <math>x</math>가 <math>\lambda x.N</math>과 같은 꼴의 부분 람다 항에 등장하지 않는다면 <math>x</math>는 자유 변수이다. 즉, 람다 항 <math>M</math>의 자유 변수의 집합 <math>\operatorname{FV}(M)</math>는 <math>M</math>의 구조에 따라 다음과 같이 재귀적으로 정의된다.
* 변수 <math>x</math>에 대하여, <math>\operatorname{FV}(x)=\{x\}</math>
* 상수 <math>a</math>에 대하여, <math>\operatorname{FV}(a)=\varnothing</math>
* 두 람다 항 <math>M</math>, <math>N</math>에 대하여, <math>\operatorname{FV}(MN)=\operatorname{FV}(M)\cup\operatorname{FV}(N)</math>
* 람다 항 <math>M</math> 및 변수 <math>x</math>에 대하여, <math>\operatorname{FV}(\lambda x.M)=\operatorname{FV}(M)\setminus\{x\}</math>
람다 항 <math>M</math>에 등장하는 변수 가운데 자유 변수가 아닌 것들을 <math>M</math>의 제한 변수라고 한다. 자유 변수를 갖지 않는 람다 항을 '''닫힌 람다 항'''(닫힌λ項, {{llang|en|closed lambda term}})이라고 한다.

예를 들어, 변수 <math>x</math>, <math>y</math>, <math>z</math>에 대하여,
:<math>(\lambda x.\lambda y.xyz)x</math>
의 자유 변수의 집합은 <math>\{x,z\}</math>이며, 제한 변수의 집합은 <math>\{y\}</math>이다.

=== 치환 ===
{{참고|치환 실례}}
주어진 람다 항에 등장하는 자유 변수를 또 다른 람다 항으로 '''치환'''(置換, {{llang|en|substitution}})하는 연산을 정의할 수 있다. 치환 연산의 정의는 자연스러우며, 다만 원래 람다 항의 의미가 변질되는 경우에는 알파 변환이 선행되어야 한다 (이는 아래 네 번째 조건의 세 번째 경우에 해당한다). 구체적으로, 람다 항 <math>M</math>, <math>N</math> 및 변수 <math>x</math>에 대하여, <math>x</math>를 <math>N</math>으로 치환한 <math>M</math>의 '''치환 실례'''(置換實例, {{llang|en|substitution instance}}) <math>M[N/x]</math>는 <math>M</math>의 구조에 따라 다음과 같이 재귀적으로 정의된다.
* 변수 <math>y</math>에 대하여,{{mindent|<math>y[N/x]=\begin{cases}
N&y=x\\
y&y\ne x
\end{cases}
</math>}}
* 상수 <math>a</math>에 대하여, <math>a[N/x]=a</math>
* 람다 항 <math>M</math>, <math>M'</math>에 대하여, <math>(MM')[N/x]=(M[N/x])(M'[N/x])</math>
* 람다 항 <math>M</math> 및 변수 <math>y</math>에 대하여,{{mindent|<math>(\lambda y.M)[N/x]=\begin{cases}
\lambda y.M&y=x\\
\lambda y.(M[N/x])&(y\ne x)\land(y\not\in\operatorname{FV}(N)\lor x\not\in\operatorname{FV}(M))\\
\lambda z.(M[z/y][N/x])&(y\ne 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}
</math>}}

예를 들어,
: <math>((\lambda x.\lambda y.xyz)x)[yw/x]=(\lambda x.\lambda y.xyz)(yw)</math>
: <math>((\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\}\})</math>
이다.

=== 알파 동치 ===
'''알파 동치'''(α同値, {{llang|en|alpha equivalence}})는 제한 변수 변경을 통해 주어진 람다 항을 새로운 람다 항으로 변환하는 방법이다. 람다 항 <math>M</math>이 부분 람다 항 <math>\lambda x.P</math>를 가질 경우, 이를 <math>P</math>의 자유 변수가 아닌 변수 <math>y</math>에 대하여 <math>\lambda y.P[y/x]</math>로 바꾸면 새로운 람다 항을 얻는다. 이와 같은 과정을 유한 번 거듭하여 람다 항 <math>N</math>를 얻을 경우, 두 람다 항 <math>M</math>, <math>N</math>이 서로 '''알파 동치'''라고 하며, <math>M\equiv_\alpha N</math>라고 표기한다.

예를 들어,
:<math>\begin{align}(\lambda x.xy)(\lambda y.yx)
&\equiv_\alpha (\lambda z.zy)(\lambda y.yx)\\
&\equiv_\alpha (\lambda z.zy)(\lambda w.wx)\\
\end{align}
</math>
이다.

=== 베타 축약 ===
'''베타 축약'''(β縮約, {{llang|en|beta reduction}})은 추상화된 함수의 적용을 적절한 치환 실례로 바꾸는 것을 통해 람다 항을 변환하는 방법이다. 람다 항 <math>M</math>가 부분 람다 항 <math>(\lambda x.P)Q</math>를 가질 경우, 이를 <math>P[Q/x]</math>로 대신하여 새로운 람다 항 <math>N</math>를 얻을 수 있다. 이 경우 <math>M\vartriangleright_{\beta,1}N</math>이라고 표기한다. 두 람다 항 <math>M</math>, <math>N</math>이 다음 조건을 만족시키면, <math>N</math>이 <math>M</math>의 '''베타 축약'''이라고 하며, <math>M\vartriangleright_\beta N</math>이라고 표기한다.
* 다음 조건을 만족시키는 람다 항의 열 <math>M=M_0,M_1,\dots,M_n=N</math>이 존재한다.
** 임의의 <math>k\in\{0,\dots,n-1\}</math>에 대하여, <math>M_k\equiv_\alpha M_{k+1}</math>이거나 <math>M_k\vartriangleright_{\beta,1}N_{k+1}</math>

두 람다 항 <math>M</math>, <math>N</math>에 대하여, 다음 두 조건이 서로 동치이며, 이를 만족시키는 <math>M</math>, <math>N</math>을 서로 '''베타 동치'''(β同値, {{llang|en|beta equivalence}})라고 하며, <math>M\equiv_\beta N</math>이라고 표기한다.
* 다음 조건을 만족시키는 람다 항의 열 <math>M=M_0,M_1,\dots,M_n=N</math>이 존재한다.
** 임의의 <math>k\in\{0,\dots,n-1\}</math>에 대하여, <math>M_k\vartriangleright_\beta M_{k+1}</math>이거나 <math>M_k\vartriangleleft_\beta M_{k+1}</math>
* ([[처치-로서 정리]]) <math>M\vartriangleright_\beta P</math>이며 <math>N\vartriangleright_\beta P</math>인 람다 항 <math>P</math>가 존재한다.

람다 항 <math>N</math>이 <math>(\lambda x.P)Q</math>와 같은 꼴의 부분 람다 항을 가지지 않는다면, <math>N</math>을 '''베타 표준형'''(β標準型, {{llang|en|beta normal form}})이라고 한다. 베타 표준형 <math>N</math>이 람다 항 <math>M</math>의 베타 축약이라면 (즉, <math>M\vartriangleright_\beta N</math>이라면), <math>N</math>을 <math>M</math>의 '''베타 표준형'''이라고 한다. 처치-로서 정리에 따라, 주어진 람다 항의 베타 표준형이 존재할 경우, 이는 (알파 동치를 무시하면) 유일하다.

== 응용 ==
<math>\mathbb N</math>이 음이 아닌 정수의 집합이라고 하자.

=== 산술의 표현 ===
람다 대수의 언어를 사용하여 [[자연수]]의 [[페아노 산술]]을 다음과 같이 표현할 수 있다.
* (처치 숫자, {{llang|en|Church numeral}}) <math>\bar n=\lambda f.\lambda x.f^nx\qquad(n\in\mathbb N)</math>
* <math>\operatorname{plus}=\lambda m.\lambda n.\lambda f.\lambda x.mf(nfx)</math>
* <math>\operatorname{times}=\lambda m.\lambda n.\lambda f.\lambda x.m(nf)x</math>
여기서
:<math>f^n=\underbrace{f\cdots f}_n</math>
이다.

=== μ-재귀 함수의 표현 ===
[[μ-재귀 함수]]는 람다 대수의 언어를 사용하여 표현할 수 있다. 즉, 임의의 부분 재귀 함수 <math>f\colon(\mathbb N_\bullet)^d\to\mathbb N_\bullet</math>에 대하여, 다음 두 조건을 만족시키는 람다 항 <math>\bar f</math>가 존재한다.<ref name="Mazzola" />{{rp|332, §43.8, Definition 276}} (여기서 <math>\mathbb N_\bullet=\mathbb N\sqcup\{\bullet_{\mathbb N}\}</math>는 [[점을 가진 집합]]이다.)
* 임의의 <math>(n_1,\dots,n_d)\in\mathbb N_\bullet^d</math>에 대하여, 만약 <math>f(n_1,\dots,n_d)=\bullet_{\mathbb N}</math>이라면, <math>\bar f{\bar n}_1\cdots{\bar n}_d</math>는 베타 표준형을 갖지 않는다.
* 임의의 <math>(n_1,\dots,n_d)\in\mathbb N_\bullet^d</math>에 대하여, 만약 <math>f(n_1,\dots,n_d)\in\mathbb N</math>이라면, <math>\bar f{\bar n}_1\cdots{\bar n}_d</math>는 <math>\overline{f(n_1,\dots,n_d)}</math>를 베타 표준형으로 갖는다.

== 같이 보기 ==
* [[데카르트 닫힌 범주]]
* [[클로저 (프로그래밍 언어)]]
* [[도메인 이론]]
* [[평가 전략 (컴퓨터 프로그래밍)]]
* [[함수형 프로그래밍]]
* [[클레이니-로서 역설]]
* [[재작성]]

== 각주 ==
{{각주}}

== 참고 문헌 ==
* {{인용|first1=Alonzo|last1=Church|author1-link=알론조 처치|first2=J. Barkley|last2=Rosser|author2-link=존 버클리 로서|jstor=1989762|title=Some properties of conversion|journal=Transactions of the American Mathematical Society|volume=39|issue=3|date=May 1936|pages=472–482}}

== 외부 링크 ==
{{위키공용분류}}
* {{웹 인용|url=https://plato.stanford.edu/entries/lambda-calculus/|성1=Alama|이름1=Jesse|성2=Korbmacher|이름2=Johannes|제목=The Lambda Calculus|웹사이트=Stanford Encyclopedia of Philosophy|issn=1095-5054}}

{{계산 이론}}
{{전거 통제}}

[[분류:람다 대수| ]]
[[분류:미국의 발명품]]
[[분류:코드 예시에 관한 문서]]
[[분류:계산 가능성 이론]]
[[분류:정형 기법]]
[[분류:계산 모형]]
[[분류:이론 컴퓨터 과학]]
[[분류:1936년 컴퓨팅]]