람다 대수

"오늘의AI위키"는 AI 기술로 일관성 있고 체계적인 최신 지식을 제공하는 혁신 플랫폼입니다.
"오늘의AI위키"의 AI를 통해 더욱 풍부하고 폭넓은 지식 경험을 누리세요.

1. 개요

람다 대수는 1930년대 알론조 처치에 의해 소개된 수학의 기초 연구의 일환으로, 함수를 표현하고 계산하는 데 사용되는 형식적 체계이다. 람다 대수는 함수를 익명으로 표현하고, 함수 적용과 추상화 등의 연산을 통해 튜링 완전성을 갖는다. 람다 대수는 α-변환, β-축약, η-축약과 같은 규칙을 통해 람다 항을 변환하며, 이를 통해 산술, 논리, 자료 구조 등을 표현할 수 있다. 람다 대수는 프로그래밍 언어 이론, 함수형 프로그래밍, 컴퓨터 과학 등 다양한 분야에 응용되며, 프로그래밍 언어의 의미론을 이해하는 데 중요한 역할을 한다.

더 읽어볼만한 페이지

1936년 컴퓨팅 - 튜링 기계
튜링 기계는 앨런 튜링이 제시한 계산 모델로, 테이프 위에서 기계적으로 작동하며, 유한한 상태, 테이프, 헤드, 명령 표를 통해 작동하고, 계산 가능성과 알고리즘의 한계를 연구하는 데 사용된다.
람다 대수 - 익명 함수
익명 함수는 이름이 없는 함수로, 람다 추상, 람다 함수, 람다 표현식, 화살표 함수 등으로 불리며, 함수형 프로그래밍 언어에서 람다식 형태로 많이 사용되고 고차 함수의 인수, 클로저, 커링 등에 활용되지만, 재귀 호출의 어려움이나 기능 제한과 같은 단점도 존재한다.
람다 대수 - 커링
커링은 다수의 인수를 취하는 함수를 단일 인수를 취하는 함수들의 연속으로 변환하는 기법으로, 함수형 프로그래밍에서 다인수 함수를 분해하여 적용하는 방식이며, 논리학과 컴퓨터 과학에서 널리 활용되는 중요한 개념이다.
코드 예시에 관한 문서 - 순서도
순서도는 컴퓨터 알고리즘이나 프로세스를 시각적으로 표현하는 도구로, 흐름 공정 차트에서 기원하여 컴퓨터 프로그래밍 분야에서 알고리즘을 설명하는 데 사용되며, 다양한 종류와 소프트웨어 도구가 존재한다.
코드 예시에 관한 문서 - 러스트 (프로그래밍 언어)
러스트는 모질라 재단 후원으로 개발된 시스템 프로그래밍 언어로서, 높은 안정성과 병렬성을 제공하며 메모리 안전성을 보장하고 효율적인 리소스 관리를 가능하게 하여 웹 브라우저 엔진, 운영체제, 웹 서비스 등 다양한 분야에서 활용되며 개발자들에게 인기가 높다.

람다 대수
개요
유형	형식 체계
분야	수학, 컴퓨터 과학, 언어학
개발자	알론조 처치
개발 년도	1930년대
특징
주요 특징	익명 함수, 고차 함수, 클로저
영향	함수형 프로그래밍, 프로그래밍 언어 이론
이론적 기반
모태	수학적 논리학
주요 개념	함수 추상화, 함수 적용, 베타 변환
표현식
변수	x, y, z (등)
추상화	λx. 표현식
적용	(표현식 표현식)
계산 규칙
알파 변환	이름 변경
베타 축소	함수 적용 및 치환
델타 변환	상수 처리 (선택 사항)
주요 응용
프로그래밍 언어	리스프, 하스켈, 스킴 등
형식 검증	프로그램의 정확성 증명
의미론적 모델링	프로그래밍 언어의 의미 정의
관련 개념
튜링 완전성	람다 대수로 모든 계산 가능 함수 표현 가능
조합 논리	람다 대수와 동등한 계산 모델
범주론	람다 대수의 추상적 표현

2. 역사

람다 대수는 1930년대 알론조 처치에 의해 수학기초론 연구의 일환으로 소개되었다.^[48]^[49] 최초의 시스템은 1935년 스티븐 클레이니와 존 버클리 로서가 클리네-로저 역설을 제창하면서 논리적 모순을 보였다.^[50]^[51]

이후 1936년 처치는 계산에 관련한 부분(무형 람다 대수)을 출판했고,^[12] 1940년에는 논리적으로 무결한 단순 유형 람다 대수를 공개했다.^[53]

1960년대에 람다 대수와 프로그래밍 언어의 관계가 명확해졌고, 리처드 몬터규 등의 언어학자들이 자연어 의미론에 적용하면서, 언어학과^[54] 컴퓨터 과학^[55] 분야에서 중요한 위치를 차지하게 되었다.

3. 도입

람다 대수는 1930년대 알론조 처치가 수학기초론 연구의 일환으로 소개한 형식적 체계다.^[48]^[49] 처음에는 논리적 모순을 보였으나,^[50]^[51] 이후 처치는 계산에 관련된 부분(현재의 유형 없는 람다 대수)을 출판했다.^[52] 1940년에는 계산적으로는 약하지만 논리적으로 무결한 단순 유형 람다 대수를 발표했다.^[53]

1960년대 이전까지 람다 대수는 형식주의에 불과했지만, 리처드 몬터규 등의 학자들이 이를 자연어 의미론에 적용하면서 언어학과^[54] 컴퓨터 과학^[55] 분야에서 중요한 위치를 차지하게 되었다.

처음에는 수학의 기초를 위한 완전한 형식적 체계를 목표로 했으나, 러셀의 역설과 같은 문제에 취약하다는 것이 밝혀졌다. 처치는 람다 계산을 분리하여 계산 가능성 이론 연구에 사용했고, 이를 통해 일계 술어 논리의 결정 가능성 문제를 부정적으로 해결했다.

람다 대수에서 어떤 수에 2를 더하는 함수 ''f''(''x'') = ''x'' + 2는 람다식 λ''x''. ''x'' + 2로 표현된다. 변수 이름은 중요하지 않아 λ''y''. ''y'' + 2도 같은 함수를 나타낸다. 함수 적용은 좌결합이며, ''f'' ''x'' ''y'' = (''f'' ''x'') ''y''이다. 인자에 함수를 취해 3을 적용하는 함수는 λ''f''. ''f'' 3으로 표현된다. 여기에 2를 더하는 함수를 적용하면 (λ''f''. ''f'' 3) (λ''x''. ''x'' + 2)가 되는데, 이는 (λ''x''. ''x'' + 2) 3, 3 + 2와 동치이다.

람다 계산에서 함수는 인자를 하나만 받는다. 인자를 두 개 받는 함수는 커링을 통해 표현된다. 예를 들어, ''f''(''x'', ''y'') = ''x'' − ''y''는 λ''x''. (λ''y''. ''x'' − ''y'')로 표현되며, λ''xy''. ''x'' − ''y''로 줄여 쓰기도 한다. 람다식은 자유 변수를 포함할 수 있다. λ''x''. ''y''에서 ''y''는 자유 변수다. 필요에 따라 변수 이름을 바꿀 수 있는데, (λ''xy''. ''y'' ''x'') (λ''x''. ''y'')는 λ''z''.z (λ''x''. ''y'')와 동치이다.

3. 1. 함수의 표현

람다 대수는 함수를 단순하게 표현하여 '함수의 계산' 개념을 더 깊이 이해하도록 돕는다.

람다 대수에서 함수를 표현하는 세 가지 중요한 특징은 다음과 같다.

함수는 이름을 가질 필요가 없다. 예를 들어, 항등 함수 $I(x) = x$ 는 $x \mapsto x$ 와 같이 쓸 수 있다.
함수의 입력 변수 이름 또한 필요 없다. $x \mapsto x$ 와 $y \mapsto y$ 는 변수 이름은 다르지만 같은 항등 함수를 의미한다.
두 개 이상의 입력을 받는 함수는 커링을 통해 하나의 입력을 받아 또 다른 함수를 출력하는 함수로 다시 쓸 수 있다. 예를 들어, $(x, y) \mapsto x \times x + y \times y$ 는 $x \mapsto (y \mapsto x \times x + y \times y)$ 와 같이 쓸 수 있다.

3. 2. 핵심 개념

\lambda x.t

는 단일 입력

x

를 받아

t

의 표현으로 치환하는 익명의 함수를 지칭한다. 예를 들어

\lambda x.x^2+2

는 함수

f(x)=x^2+2

의 람다 추상화이다. 람다 추상화를 통해 함수를 정의한다는 것은 함수를 정의하기만 하고 함수를 수행(호출)하지는 않는다는 것을 의미한다. 람다 추상화를 통해 변수

x

는 표현

t

에 속박된다.

자유 변수(free variable)는 람다 추상화를 통해 표현에 묶이지 않은 변수를 말한다. 자유 변수의 집합은 귀납적으로 정의된다.

$x$ 의 자유 변수는 $x$ 뿐이다.
$\lambda x.t$ 의 자유변수는 $x$ 를 제외하고 $t$ 에 등장하는 변수들이다.
두 표현 $t$ 와 $s$ 의 결합 $ts$ 의 자유변수의 집합은 $t$ 의 자유변수의 집합과 $s$ 의 자유변수의 집합의 합집합이다.

예를 들어,

\lambda x.x

에는 자유 변수가 없지만,

\lambda x.x+y

에는 자유변수가

y

하나이다.

어떤 수에 2를 더하는 함수 ''f''를 생각해 보자. 이것은 일반적인 표기법으로는 ''f''(''x'') = ''x'' + 2라고 쓸 수 있을 것이다. 이 함수 ''f''는 람다 계산의 식(람다식이라고 한다)에서는 λ''x''. ''x'' + 2로 쓰인다. 변수 ''x''의 이름은 중요하지 않으며, λ''y''. ''y'' + 2라고 써도 같다. 마찬가지로, 이 함수에 3을 적용한 결과의 수 ''f''(3)은 (λ''x''. ''x'' + 2) 3으로 쓰인다. 함수의 적용은 좌결합이다. 즉, ''f'' ''x'' ''y'' = (''f'' ''x'') ''y''이다.

인자(함수의 입력)에 함수를 취하여 거기에 3을 적용하는 함수를 생각해 보자. 이것은 람다식으로는 λ''f''. ''f'' 3이 된다. 이 함수에, 아까 만든 2를 더하는 함수를 적용하면, (λ''f''. ''f'' 3) (λ''x''. ''x'' + 2)가 된다. 여기서,

: (λ''f''. ''f'' 3) (λ''x''. ''x'' + 2) 과 (λ''x''. ''x'' + 2) 3 과 3 + 2

의 3개의 표현은 모두 동치이다.

람다 계산에서는, 함수의 인자는 항상 1개이다. 인자를 2개 취하는 함수는, 1개의 인자를 취하고, 1개의 인자를 취하는 함수를 반환하는 함수로 표현된다(커링). 예를 들어, 함수 ''f''(''x'', ''y'') = ''x'' − ''y''는 λ''x''. (λ''y''. ''x'' − ''y'')가 된다. 이 식은 관례로 λ''xy''. ''x'' − ''y''라고 생략해서 쓰는 경우가 많다. 다음 3개의 식

: (λ''xy''. ''x'' − ''y'') 7 2 과 　(λ''y''. 7 − ''y'') 2 과 7 − 2

는 모두 동치가 된다.

람다식은 '''자유 변수'''(λ에 의해 바운딩되지 않은 변수)를 포함할 수도 있다. 예를 들어, 입력에 관계없이 항상 ''y''를 반환하는 함수를 나타내는 식 λ''x''. ''y''에서, 변수 ''y''는 자유 변수이다. 이러한 때에 변수 이름을 바꾸는 것이 필요할 때가 있다. 즉, 식 (λ''xy''. ''y'' ''x'') (λ''x''. ''y'')는 λ''y''. y (λ''x''. ''y'')가 아니라, λ''z''.z (λ''x''. ''y'')와 동치이다.

4. 정의

람다 대수의 언어는 변수, 상수, 람다 기호, 괄호, 온점으로 구성된다. 람다 항은 변수와 상수들로부터 시작하여 유한 차례 적용 및 추상화를 가하여 얻는 문자열이다.

'''적용''': 두 람다 항 $M$ , $N$ 에 대하여, 문자열 $(MN)$ 은 람다 항이다.
'''추상화''': 람다 항 $M$ 및 변수 $x$ 에 대하여, 문자열 $(\lambda x.M)$ 은 람다 항이다.

괄호 사용을 줄이기 위해 다음과 같은 표기법을 사용한다.

$M_1M_2\cdots M_n$ 은 $(\cdots((M_1M_2)M_3)\cdots M_n)$ 을 나타낸다.
$\lambda x.M_1\cdots M_n$ 은 $(\lambda x.(\cdots((M_1M_2)M_3)\cdots M_n))$ 을 나타낸다.
$\lambda x_1.\cdots\lambda x_n.M$ (또는 $\lambda x_1\cdots x_n.M$ )은 $(\lambda x_1.\cdots(\lambda x_{n-1}.(\lambda x_n.M))\cdots)$ 을 나타낸다.

예를 들어, 변수

x

,

y

,

z

에 대하여,

\lambda x.x\lambda x.\lambda y.xyz

는

(\lambda x.(x(\lambda x.(\lambda y.((xy)z)))))

를 나타낸다.

람다 대수는 특정 형식적 구문에 의해 정의되는 '람다 항'의 언어와 람다 항을 조작하기 위한 일련의 변환 규칙으로 구성된다. 이러한 변환 규칙은 등식 이론 또는 조작적 정의로 볼 수 있다.

이름이 없으므로 람다 대수의 모든 함수는 익명 함수이다. 하나의 입력 변수만 허용하므로 여러 변수의 함수를 구현하기 위해 커링이 사용된다.

람다식은 '''자유 변수'''(λ에 의해 바운딩되지 않은 변수)를 포함할 수도 있다. 예를 들어, 입력에 관계없이 항상 ''y''를 반환하는 함수를 나타내는 식 λ''x''. ''y''에서, 변수 ''y''는 자유 변수이다. 이럴 때 변수 이름을 바꾸는 것이 필요할 때가 있다. 즉, 식 (λ''xy''. ''y'' ''x'') (λ''x''. ''y'')는 λ''y''. y (λ''x''. ''y'')가 아니라, λ''z''.z (λ''x''. ''y'')와 동치이다.

5. 연산

람다 대수는 추상화와 적용이라는 두 가지 주요 연산을 기반으로 한다.
추상화( $\lambda x.t$ )는 단일 입력 $x$ 를 받아 $t$ 로 치환하는 익명 함수를 나타낸다. 예를 들어 $\lambda x.x^2+2$ 는 $f(x)=x^2+2$ 함수를 람다 추상화로 표현한 것이다. 람다 추상화로 함수를 정의하는 것은 함수를 정의만 하고 호출하지는 않는다는 것을 의미한다. 변수 $x$ 는 람다 추상화를 통해 표현 $t$ 에 속박된다.
적용( $t$ $s$ )은 입력 $s$ 에 대한 함수 $t$ 의 적용을 나타낸다. 즉, 입력 $s$ 에 함수 $t$ 를 호출하여 $t(s)$ 를 생성하는 것을 의미한다.

람다 대수의 구문은 일부 표현식을 유효한 람다 대수 표현식인 '''람다 항'''으로 정의한다. 유효한 람다 항은 다음 세 가지 규칙을 반복 적용하여 얻을 수 있다.

변수 자체는 유효한 람다 항이다.
$t$ 가 람다 항이고, $x$ 가 변수라면, $(\lambda x.t)$ 는 람다 항이다(''추상화'').
$t$ 와 $s$ 가 람다 항이라면, $(t$ $s)$ 는 람다 항이다(''적용'').

괄호는 항의 모호성을 제거하는 데 사용될 수 있다. 예를 들어,

\lambda x.((\lambda x.x)x)

와

(\lambda x.(\lambda x.x))x

는 서로 다른 항을 나타낸다. 전자는 함수 정의이고, 후자는 함수 적용이다.

5. 1. 자유 변수와 제한 변수

람다 항에 등장하는 변수는 '''자유 변수'''(free variable^영어)와 '''제한 변수'''(bound variable^영어)로 분류된다. 람다 추상화에 의해 묶이지 않은 변수는 자유 변수이고, 묶인 변수는 제한 변수이다.

람다 항

M

의 자유 변수의 집합

\operatorname{FV}(M)

는

M

의 구조에 따라 다음과 같이 재귀적으로 정의된다.

변수 $x$ 에 대하여, $\operatorname{FV}(x)=\{x\}$
두 람다 항 $M$ , $N$ 에 대하여, $\operatorname{FV}(MN)=\operatorname{FV}(M)\cup\operatorname{FV}(N)$
람다 항 $M$ 및 변수 $x$ 에 대하여, $\operatorname{FV}(\lambda x.M)=\operatorname{FV}(M)\setminus\{x\}$

람다 항

M

에 등장하는 변수 가운데 자유 변수가 아닌 것들을

M

의 제한 변수라고 한다. 자유 변수를 갖지 않는 람다 항을 '''닫힌 람다 항'''(닫힌λ項, closed lambda term^영어)이라고 한다.

예를 들어, 항등 함수를 나타내는 람다 항

\lambda x.x

는 자유 변수가 없지만, 함수

\lambda x. y

x

는 단일 자유 변수

y

를 갖는다.^[21]

추상 연산자 λ는 추상화 본문에서 변수가 나타나는 모든 위치에 해당 변수를 묶는다. 추상화의 범위 내에 있는 변수를 '묶여 있다'고 한다. 식 λ''x''.''M''에서 λ''x'' 부분은 ''결합자''라고 불리는데, 이는 변수 ''x''가 M 앞에 λ''x''를 붙여 묶인다는 것을 암시하기 때문이다. 다른 모든 변수는 ''자유 변수''라고 한다. 예를 들어, 식 λ''y''.''x x y''에서 ''y''는 묶인 변수이고 ''x''는 자유 변수이다. 또한 변수는 가장 가까운 추상화에 의해 묶인다. 다음 예에서 식에 있는 ''x''의 단일 발생은 두 번째 람다에 의해 묶인다: λ''x''.''y'' (λ''x''.''z x'').

5. 2. 치환

주어진 람다 항에 등장하는 자유 변수를 또 다른 람다 항으로 치환(置換, substitution^영어)하는 연산을 정의할 수 있다. 치환 연산의 정의는 자연스러우며, 다만 원래 람다 항의 의미가 변질되는 경우에는 알파 변환이 선행되어야 한다. 구체적으로, 람다 항

M

,

N

및 변수

x

에 대하여,

x

를

N

으로 치환한

M

의 치환 실례(置換實例, substitution instance^영어)

M[N/x]

는

M

의 구조에 따라 다음과 같이 재귀적으로 정의된다.

변수 $y$ 에 대하여,

y[N/x]=\begin{cases}    N&y=x\\    y&y\ne x    \end{cases}

상수 $a$ 에 대하여, $a[N/x]=a$
람다 항 $M$ , $M'$ 에 대하여, $(MM')[N/x]=(M[N/x])(M'[N/x])$
람다 항 $M$ 및 변수 $y$ 에 대하여,

(\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}

예를 들어,

:

((\lambda x.\lambda y.xyz)x)[yw/x]=(\lambda x.\lambda y.xyz)(yw)

:

((\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\}\})

이다.

t

,

s

,

r

이 람다 항이고,

x

와

y

가 변수라고 가정하자. 표기

t[x := r]

은 "포획 회피" 방식으로

t

에서

x

에 대한

r

의 대체를 나타낸다. 이것은 다음과 같이 정의된다.

$x[x := r] = r$ ; $r$ 이 $x$ 로 대체되면 $x$ 는 $r$ 이 된다.
$y[x := r] = y$ ( $x \neq y$ 인 경우); $r$ 이 $x$ 로 대체되면 $y$ ( $x$ 가 아님)는 $y$ 로 유지된다.
$(t s)[x := r] = (t[x := r])(s[x := r])$ ; 대체는 응용 프로그램의 양쪽으로 분산된다.
$(\lambda x.t)[x := r] = \lambda x.t$ ; 추상화에 의해 바인딩된 변수는 대체되지 않으며, 이러한 변수를 대체하면 추상화는 변경되지 않는다.
$(\lambda y.t)[x := r] = \lambda y.(t[x := r])$ ( $x \neq y$ 이고 $y$ 가 $r$ 의 자유 변수( $y$ 는 $r$ 에 대해 "새로운"이라고 함)에 나타나지 않는 경우); 추상화에 의해 바인딩되지 않은 변수를 대체하면, 추상화된 변수 $y$ 가 대체 항 $r$ 에 대해 "새로운" 경우 추상화의 본문에서 진행된다.

예를 들어,

(\lambda x.x)[y := y] = \lambda x.(x[y := y]) = \lambda x.x

이고

((\lambda x.y)x)[x := y] = ((\lambda x.y)[x := y])(x[x := y]) = (\lambda x.y)y

이다.

새로운 조건(

y

가

r

의 자유 변수에 없어야 함)은 대체를 통해 함수의 의미가 변경되지 않도록 하는 데 중요하다.

예를 들어, 새로운 조건을 무시하는 대체를 통해 오류가 발생할 수 있다.

(\lambda x.y)[y := x] = \lambda x.(y[y := x]) = \lambda x.x

. 이 오류 대체를 통해 상수 함수

\lambda x.y

가 항등 함수

\lambda x.x

로 바뀐다.

일반적으로, 새로운 조건을 충족하지 못하는 경우, 먼저 적절한 새로운 변수를 사용하여 알파-이름 변경을 수행하여 해결할 수 있다. 예를 들어, 대체에 대한 올바른 개념으로 다시 전환하면,

(\lambda x.y)[y := x]

에서 추상화를 새로운 변수

z

로 이름을 바꿀 수 있으며,

(\lambda z.y)[y := x] = \lambda z.(y[y := x]) = \lambda z.x

가 되며, 함수의 의미는 대체에 의해 보존된다.

치환, ''M''[''x'' := ''N'']는 표현식 ''M'' 내의 변수 ''x''의 모든 ''자유로운'' 발생을 표현식 ''N''으로 대체하는 과정이다. 람다 대수의 항에 대한 치환은 항의 구조에 대한 재귀로 정의되며, 다음과 같다 (참고: x와 y는 변수이고 M과 N은 모든 람다 표현식이다).

: ''x''[''x'' := ''N''] = ''N''

: ''y''[''x'' := ''N''] = ''y'', 만약 ''x'' ≠ ''y''

: (''M''₁ ''M''₂)[''x'' := ''N''] = ''M''₁[''x'' := ''N''] ''M''₂[''x'' := ''N'']

: (λ''x''.''M'')[''x'' := ''N''] = λ''x''.''M''

: (λ''y''.''M'')[''x'' := ''N''] = λ''y''.(''M''[''x'' := ''N'']), 만약 ''x'' ≠ ''y'' 그리고 ''y'' ∉ FV(''N'') (''FV에 대해서는 위 참조'')

추상화에 치환을 적용하기 위해서는 표현식을 α-변환해야 할 때가 있다. 예를 들어, (λ''x''.''y'')[''y'' := ''x'']의 결과가 λ''x''.''x''가 되는 것은 올바르지 않다. 치환된 ''x''가 자유로워야 했지만 결국 속박되었기 때문이다. 이 경우의 올바른 치환은 α-동등성 까지 λ''z''.''x''이다. 치환은 α-동등성까지 고유하게 정의된다.

5. 3. 알파 동치

'''알파 동치'''(alpha equivalence^영어)는 제한 변수 변경을 통해 주어진 람다 항을 새로운 람다 항으로 변환하는 방법이다. 람다 항

M

이 부분 람다 항

\lambda x.P

를 가질 경우,

P

의 자유 변수가 아닌 변수

y

에 대하여

\lambda y.P[y/x]

로 바꾸면 새로운 람다 항을 얻는다. 이와 같은 과정을 유한 번 거듭하여 람다 항

N

를 얻을 경우, 두 람다 항

M

,

N

이 서로 '''알파 동치'''라고 하며,

M\equiv_\alpha N

라고 표기한다.

예를 들어,

:

\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}

이다.

람다 항에 정의할 수 있는 기본적인 형태의 동치는 ''알파 동치''이다. 이는 추상화에서 묶인 변수의 특정 선택이 (일반적으로) 중요하지 않다는 직관을 포착한다.

예를 들어,

\lambda x.x

와

\lambda y.y

는 알파 동치인 람다 항이며, 둘 다 동일한 함수(항등 함수)를 나타낸다.

x

와

y

는 추상화에서 묶여 있지 않기 때문에 알파 동치가 아니다.

많은 표현에서 알파 동치인 람다 항을 식별하는 것이 일반적이다.

5. 4. 베타 축약

'''베타 축약'''(β縮約, beta reduction^영어)은 추상화된 함수의 적용을 적절한 치환 실례로 바꾸는 것을 통해 람다 항을 변환하는 방법이다. 람다 항

M

가 부분 람다 항

(\lambda x.P)Q

를 가질 경우, 이를

P[Q/x]

로 대신하여 새로운 람다 항

N

를 얻을 수 있다. 이 경우

M\vartriangleright_{\beta,1}N

이라고 표기한다.

두 람다 항

M

,

N

이 다음 조건을 만족시키면,

N

이

M

의 '''베타 축약'''이라고 하며,

M\vartriangleright_\beta N

이라고 표기한다.

다음 조건을 만족시키는 람다 항의 열 $M=M_0,M_1,\dots,M_n=N$ 이 존재한다.
임의의 $k\in\{0,\dots,n-1\}$ 에 대하여, $M_k\equiv_\alpha M_{k+1}$ 이거나 $M_k\vartriangleright_{\beta,1}N_{k+1}$

두 람다 항

M

,

N

에 대하여, 다음 두 조건이 서로 동치이며, 이를 만족시키는

M

,

N

을 서로 '''베타 동치'''(β同値, beta equivalence^영어)라고 하며,

M\equiv_\beta N

이라고 표기한다.

다음 조건을 만족시키는 람다 항의 열 $M=M_0,M_1,\dots,M_n=N$ 이 존재한다.
임의의 $k\in\{0,\dots,n-1\}$ 에 대하여, $M_k\vartriangleright_\beta M_{k+1}$ 이거나 $M_k\vartriangleleft_\beta M_{k+1}$
(처치-로서 정리) $M\vartriangleright_\beta P$ 이며 $N\vartriangleright_\beta P$ 인 람다 항 $P$ 가 존재한다.

람다 항

N

이

(\lambda x.P)Q

와 같은 꼴의 부분 람다 항을 가지지 않는다면,

N

을 '''베타 표준형'''(β標準型, beta normal form^영어)이라고 한다. 베타 표준형

N

이 람다 항

M

의 베타 축약이라면 (즉,

M\vartriangleright_\beta N

이라면),

N

을

M

의 '''베타 표준형'''이라고 한다. 처치-로서 정리에 따라, 주어진 람다 항의 베타 표준형이 존재할 경우, 이는 (알파 동치를 무시하면) 유일하다.

β-감소 규칙은

( \lambda x . t) s

형태의 적용이

t [ x := s]

항으로 감소한다고 명시한다. 표기

( \lambda x . t ) s \to t [ x := s ]

는

( \lambda x .t ) s

가

t [ x := s ]

로 β-감소한다는 것을 나타내는 데 사용된다.

예를 들어, 모든

s

에 대해

( \lambda x . x ) s \to x[ x := s ] = s

이다. 이는

\lambda x . x

가 실제로 항등 함수임을 보여준다. 마찬가지로,

( \lambda x . y ) s \to y [ x := s ] = y

인데, 이는

\lambda x . y

가 상수 함수임을 보여준다.

람다 대수는 Haskell 또는 Standard ML과 같은 함수형 프로그래밍 언어의 이상화된 버전으로 볼 수 있다. 이 관점에서 β-감소는 계산 단계에 해당한다. 이 단계는 더 이상 감소시킬 적용이 없을 때까지 추가적인 β-감소로 반복될 수 있다. 여기서 제시된 무형식 람다 대수에서 이 감소 과정은 종료되지 않을 수 있다. 예를 들어, 항

\Omega = (\lambda x . xx)( \lambda x . xx )

를 생각해 보자. 여기서

( \lambda x . xx)( \lambda x . xx) \to ( xx )[ x := \lambda x . xx ] = ( x [ x := \lambda x . xx ] )( x [ x := \lambda x . xx ] ) = ( \lambda x . xx)( \lambda x . xx )

이다. 즉, 항은 단일 β-감소로 자신으로 감소하며, 따라서 감소 과정은 절대 종료되지 않는다.

6. 응용

람다 대수는 튜링 완전하며, 이는 어떠한 튜링 기계도 시뮬레이션할 수 있는 보편적인 계산 모델이다.^[2] 수학, 철학,^[3] 언어학,^[4]^[5] 및 컴퓨터 과학 등 여러 분야에 응용된다.^[6]^[7]

특히, 프로그래밍 언어 이론에서 함수형 프로그래밍 언어 개발에 중요한 역할을 했으며, 함수형 프로그래밍 언어는 람다 대수를 구현한 것이다.^[8]

또한, 처치-튜링 명제에서 언급되는 계산 가능성을 정의하는 방법 중 하나이다. 처치-튜링 명제에 따르면, 자연수 함수 ''F'': '''N''' → '''N'''가 계산 가능하려면, 모든 자연수 쌍 ''x'', ''y''에 대해 ''F''(''x'')=''y''일 때만 ''f'' =_β 를 만족하는 람다 표현식 ''f''가 존재해야 한다. 여기서 와는 각각 ''x''와 ''y''에 해당하는 처치 수이며, =_β는 β-축약을 통한 동등성을 의미한다.

람다 대수는 범주론의 연구 주제이기도 하다.^[8]

6. 1. 산술의 표현

처치 숫자(Church numeral)를 사용하여 자연수의 페아노 산술을 표현할 수 있다. 덧셈, 곱셈, 뺄셈 등의 산술 연산을 람다 항으로 정의할 수 있는데, 그 예시는 다음과 같다.^[25]

처치 숫자: $\bar n=\lambda f.\lambda x.f^nx\qquad(n\in\mathbb N)$
덧셈: $\operatorname{plus}=\lambda m.\lambda n.\lambda f.\lambda x.mf(nfx)$
곱셈: $\operatorname{times}=\lambda m.\lambda n.\lambda f.\lambda x.m(nf)x$

여기서

f^n=\underbrace{f\cdots f}_n

이다.

람다 대수에서 자연수를 정의하는 방법은 여러 가지가 있지만, 가장 흔한 방법은 처치 수를 사용하는 것이다. 처치 수는 다음과 같이 정의된다.

:

:

:

:

: (이하 생략)

처치 수 n은 함수 f를 인자로 받아 f의 n번째 합성을 반환하는 고차 함수이다. 즉, f⁽⁰⁾은 항등 함수로 정의된다.

처치 수 n을 받아 n+1을 반환하는 후속 함수는 다음과 같이 정의할 수 있다. 여기서 '(mf)x'는 함수 'f'가 'x'에 'm'번 적용됨을 의미한다.

: SUCC := λ''n''.λ''f''.λ''x''.''f'' (''n'' ''f'' ''x'')

f의 m번째 합성과 f의 n번째 합성을 합성하면 f의 m+n번째 합성이 되므로, 덧셈은 다음과 같이 정의할 수 있다.

: PLUS := λ''m''.λ''n''.λ''f''.λ''x''.''m'' ''f'' (''n'' ''f'' ''x'')

또는, 숫자 m에 n을 더하는 것은 1을 m번 더하는 것으로 수행할 수 있으므로, 다음과 같이 정의할 수도 있다.

: PLUS := λ''m''.λ''n''.''m'' SUCC ''n''

마찬가지로 곱셈은 다음과 같이 정의된다.

: MULT := λ''m''.λ''n''.λ''f''.''m'' (''n'' ''f'')

또는, m과 n을 곱하는 것은 add n 함수를 m번 반복한 다음 0에 적용하는 것과 같으므로, 다음과 같이 정의할 수도 있다.

: MULT := λ''m''.λ''n''.''m'' (PLUS ''n'') 0

지수는 처치 수에서 다음과 같이 표현된다.

: POW := λ''b''.λ''e''.''e'' ''b''

PRED ''n'' = ''n'' − 1로 정의된 선행 함수는 양의 정수 n에 대해, PRED 0 = 0이며, 공식은 다음과 같다.

: PRED := λ''n''.λ''f''.λ''x''.''n'' (λ''g''.λ''h''.''h'' (''g'' ''f'')) (λ''u''.''x'') (λ''u''.''u'')

선행 함수를 사용하면 뺄셈은 다음과 같이 간단하게 정의된다.

: SUB := λ''m''.λ''n''.''n'' PRED ''m''

SUB m n는 m > n일 때는 m − n을 반환하고, 그렇지 않으면 0을 반환한다.

6. 2. μ-재귀 함수의 표현

μ-재귀 함수는 람다 대수의 언어를 사용하여 표현할 수 있다. 즉, 임의의 부분 재귀 함수

f\colon(\mathbb N_\bullet)^d\to\mathbb N_\bullet

에 대하여, 다음 두 조건을 만족시키는 람다 항

\bar f

가 존재한다.^[43] (여기서

\mathbb N_\bullet=\mathbb N\sqcup\{\bullet_{\mathbb N}\}

는 점을 가진 집합이다.)

임의의 $(n_1,\dots,n_d)\in\mathbb N_\bullet^d$ 에 대하여, 만약 $f(n_1,\dots,n_d)=\bullet_{\mathbb N}$ 이라면, $\bar f{\bar n}_1\cdots{\bar n}_d$ 는 베타 표준형을 갖지 않는다.
임의의 $(n_1,\dots,n_d)\in\mathbb N_\bullet^d$ 에 대하여, 만약 $f(n_1,\dots,n_d)\in\mathbb N$ 이라면, $\bar f{\bar n}_1\cdots{\bar n}_d$ 는 $\overline{f(n_1,\dots,n_d)}$ 를 베타 표준형으로 갖는다.

6. 3. 논리와 술어

관례에 따라 부울 값 TRUE^영어 및 FALSE^영어에 대해 다음 두 가지 정의(처치 부울로 알려짐)가 사용된다.

: TRUE := λ''x''.λ''y''.''x''^영어

: FALSE := λ''x''.λ''y''.''y''^영어

이 두 람다 항을 사용하여 일부 논리 연산자를 정의할 수 있다. (이는 단지 가능한 공식일 뿐이며, 다른 표현식도 마찬가지로 정확할 수 있다.)

: AND := λ''p''.λ''q''.''p'' ''q'' ''p''^영어

: OR := λ''p''.λ''q''.''p'' ''p'' ''q''^영어

: NOT := λ''p''.''p'' FALSE TRUE^영어

: IFTHENELSE := λ''p''.λ''a''.λ''b''.''p'' ''a'' ''b''^영어

이제 일부 논리 함수를 계산할 수 있다. 예를 들어:

: AND TRUE FALSE^영어

:: ≡ (λ''p''.λ''q''.''p'' ''q'' ''p'') TRUE FALSE →_β TRUE FALSE TRUE^영어

:: ≡ (λ''x''.λ''y''.''x'') FALSE TRUE →_β FALSE^영어

그리고 AND TRUE FALSE^영어가 FALSE^영어와 동일하다는 것을 알 수 있다.

''술어''는 부울 값을 반환하는 함수이다. 가장 기본적인 술어는 ISZERO^영어인데, 인수가 처치 숫자 0^영어이면 TRUE^영어를 반환하고, 다른 처치 숫자이면 FALSE^영어를 반환한다.

: ISZERO := λ''n''.''n'' (λ''x''.FALSE) TRUE^영어

다음 술어는 첫 번째 인수가 두 번째 인수보다 작거나 같은지 테스트한다.

: LEQ := λ''m''.λ''n''.ISZERO (SUB ''m'' ''n'')^영어

그리고 1=''m'' = ''n''^영어이므로, LEQ ''m'' ''n''^영어 및 LEQ ''n'' ''m''^영어이면 수치적 동일성을 위한 술어를 쉽게 만들 수 있다.

술어의 가용성과 TRUE^영어 및 FALSE^영어의 위 정의를 통해 람다 계산에서 "if-then-else" 식을 편리하게 작성할 수 있다. 예를 들어, 이전 함수는 다음과 같이 정의할 수 있다.

: PRED := λ''n''.''n'' (λ''g''.λ''k''.ISZERO (''g'' 1) ''k'' (PLUS (''g'' ''k'') 1)) (λ''v''.0) 0^영어

이는 ''n'' (λ''g''.λ''k''.ISZERO (''g'' 1) ''k'' (PLUS (''g'' ''k'') 1)) (λ''v''.0)^영어가 ''n''^영어 > 0에 대해 ''n''^영어 − 1 함수를 더하는 것을 귀납적으로 보여줌으로써 확인할 수 있다.^[42]

TRUE^영어나 FALSE^영어와 같은 진릿값은 관습적으로 다음과 같이 정의되는 경우가 많다. 이것들은 Church booleans^영어라고 불린다.

: TRUE := λ''x'' ''y''. ''x''^영어

: FALSE := λ''x'' ''y''. ''y''^영어

: (이 FALSE^영어는 앞서 언급한 처치 수의 0과 같은 정의임을 주의하라)

이러한 진릿값에 대해 논리 기호를 정의할 수 있다. 예를 들어, 다음과 같은 것들이 있다.

: AND := λ''p'' ''q''. ''p'' ''q'' FALSE^영어

: OR := λ''p'' ''q''. ''p'' TRUE ''q''^영어

: NOT := λ''p''. ''p'' FALSE TRUE^영어

: IFTHENELSE := λ''p'' ''x'' ''y''. ''p'' ''x'' ''y''^영어

이러한 기호를 사용한 계산의 예를 들겠다.

: AND TRUE FALSE^영어

::= (λ''p'' ''q''. ''p q'' FALSE^영어) TRUE^영어 FALSE^영어 →^β TRUE^영어 FALSE^영어 FALSE^영어

::= (λ''x'' ''y''. ''x'') FALSE^영어 FALSE^영어 →^β FALSE^영어

이상으로부터, AND TRUE FALSE^영어가 FALSE^영어와 같음을 알 수 있다.

"

: ISZERO := λ''n''. ''n'' (λ''x''. FALSE) TRUE^영어

6. 4. 쌍

처치 쌍을 사용하여 순서쌍을 표현할 수 있다. TRUE와 FALSE를 사용하여 쌍(2-튜플)을 정의할 수 있는데, 예를 들어 PAIR는 쌍(x, y)을 캡슐화하고, FIRST는 쌍의 첫 번째 요소를, SECOND는 두 번째 요소를 반환한다.^[42] 관련 수식은 다음과 같다.

:

:

:

:

연결 리스트는 빈 리스트에 대한 NIL이거나, 요소와 더 작은 리스트의 형태로 정의할 수 있다. 술어 NULL은 NIL 값을 테스트한다. ( NIL := FALSE로 정의하면, 구조를 통해 명시적인 NULL 테스트가 필요 없어진다.)^[42]

쌍의 사용 예시로, (m, n)을 (n, n+1)로 매핑하는 shift-and-increment 함수는 다음과 같이 정의할 수 있다.^[42]

:

이는 이전 함수(predecessor function)의 가장 투명한 버전을 제공하는 데 사용된다.^[42]

:

(쌍으로 구성된) 순서쌍의 데이터 타입은 TRUE와 FALSE를 사용하여 정의할 수 있다. 이것들은 Church pairs|처치 쌍^영어이라고 불린다.^[42] 관련 수식은 다음과 같다.

:

:

:

링크 타입의 리스트 구조는 빈 리스트를 위해 특별히 예약된 값(예: FALSE)을 사용하고, 리스트를 그 선두 요소와 후속 리스트의 CONS 쌍으로 표현함으로써 구현할 수 있다.^[42]

7. 추가 프로그래밍 기법

람다 계산에서 함수의 인자는 항상 1개이다. 인자를 2개 취하는 함수는 1개의 인자를 취하고, 1개의 인자를 취하는 함수를 반환하는 함수로 표현된다(커링). 예를 들어, 함수 ''f''(''x'', ''y'') = ''x'' - ''y''는 λ''x''. (λ''y''. ''x'' - ''y'')가 된다. 이 식은 관례로 λ''xy''. ''x'' - ''y''라고 생략해서 쓰는 경우가 많다. 다음 3개의 식은 모두 동치가 된다.

:(λ''xy''. ''x'' - ''y'') 7 2

:(λ''y''. 7 - ''y'') 2

:7 - 2

람다 계산 자체에는 정수나 덧셈 등이 존재하지 않지만, 산술 연산과 정수는 특정 람다식의 생략이라고 정의함으로써 인코딩할 수 있다.

람다식은 '''자유 변수'''(λ에 의해 바운딩되지 않은 변수)를 포함할 수도 있다. 예를 들어, 입력에 관계없이 항상 ''y''를 반환하는 함수를 나타내는 식 λ''x''. ''y''에서, 변수 ''y''는 자유 변수이다. 이러한 때에 변수 이름을 바꾸는 것이 필요할 때가 있다. 즉, 식 (λ''xy''. ''y'' ''x'') (λ''x''. ''y'')는 λ''y''. y (λ''x''. ''y'')가 아니라, λ''z''.z (λ''x''. ''y'')와 동치이다.

람다 대수는 계산 가능한 모든 함수를 표현할 수 있으며, 2 + 3과 같은 산술 연산도 람다식으로 표현 가능하다.

7. 1. 명명된 상수

람다 대수에서 라이브러리는 이전에 정의된 함수의 모음 형태로 나타나며, 이는 람다 항으로서 특정 상수일 뿐이다. 순수 람다 대수에는 명명된 상수의 개념이 없는데, 모든 원자 람다 항이 변수이기 때문이다. 그러나 상수를 이름으로 지정하고, 해당 변수를 주요 본문에서 바인딩하기 위해 추상화를 사용하고, 해당 추상화를 의도된 정의에 적용하여 명명된 상수를 에뮬레이션할 수 있다. 따라서 ''f''를 ''M''(다른 람다 항, "주 프로그램")에서 ''N''(일부 명시적인 람다 항)을 의미하도록 사용하려면 다음과 같이 표현할 수 있다.

:(λ''f''.''M'') ''N''

작성자는 위를 보다 직관적인 순서로 작성할 수 있도록 let^영어과 같은 구문적 설탕을 종종 도입한다.

:let ''f'' = ''N'' in ''M''^영어

이러한 정의를 연결하여, 람다 대수 "프로그램"을 0개 이상의 함수 정의와, 해당 함수를 사용하는 람다 항 하나로 작성할 수 있으며, 이는 프로그램의 주요 본문을 구성한다.

이 let^영어의 주목할 만한 제약 사항은 이름 ''f''가 ''N''에서 정의되지 않아야 한다는 것이다. 즉, ''N''이 추상화 바인딩 ''f''의 범위를 벗어나도록 하기 위함이다. 이는 재귀 함수 정의가 let^영어으로 ''N''으로 사용될 수 없음을 의미한다. letrec^영어 구성을 사용하면 재귀 함수 정의를 작성할 수 있다.^[14]^[26]

7. 2. 재귀

람다 대수는 기본적으로 재귀를 지원하지 않는다. 람다 대수에서 모든 함수는 익명 함수이므로, 동일한 값을 정의하는 람다 항 내부에서 아직 정의되지 않은 값을 이름으로 참조할 수 없기 때문이다. 그러나 람다 표현식은 자체 인수로 자신을 수신할 수 있다.^[42]

이러한 특성을 이용하여 고정점 결합자를 사용하면 재귀 함수를 표현할 수 있다. 고정점 결합자는 주어진 람다 항(예: )에 대해, 재귀 함수를 나타내는 자기 복제 람다 표현식(예: )을 반환한다. 이때, 함수는 자체 복제가 호출될 때마다 수행되도록 미리 준비되어 있기 때문에 어떤 지점에서도 명시적으로 자신에게 전달될 필요가 없다. 따라서 원래 람다 표현식 는 호출 지점에서 자체 내에서 다시 생성되어 자기 참조를 달성한다.^[42]

대표적인 고정점 결합자로는 Y 결합자가 있다. Y 결합자는 다음과 같이 정의된다.^[42]

:

람다 대수에서 는 의 고정점이 된다. 즉, 다음 식이 성립한다.^[42]

:

:

모든 재귀적으로 정의된 함수는 재귀 호출을 추가 인수로 닫는 적절하게 정의된 함수의 고정점으로 볼 수 있다. 따라서 를 사용하면 모든 재귀적으로 정의된 함수를 람다 표현식으로 표현할 수 있다.^[42]

7. 3. 표준 용어

일부 용어는 일반적으로 통용되는 이름을 가지고 있다.^[27]^[28]^[29]

'''I''' := λ''x''.''x''
'''S''' := λ''x''.λ''y''.λ''z''.''x'' ''z'' (''y'' ''z'')
'''K''' := λ''x''.λ''y''.''x''
'''B''' := λ''x''.λ''y''.λ''z''.''x'' (''y'' ''z'')
'''C''' := λ''x''.λ''y''.λ''z''.''x'' ''z'' ''y''
'''W''' := λ''x''.λ''y''.''x'' ''y'' ''y''
'''ω''' 또는 '''Δ''' 또는 '''U''' := λ''x''.''x'' ''x''
'''Ω''' := '''ω ω'''

'''I'''는 항등 함수이다. '''SK'''와 '''BCKW'''는 임의의 람다 항을 표현할 수 있는 완전한 조합자 계산 시스템을 형성한다. '''Ω'''는 '''UU'''이며, 정규형을 갖지 않는 가장 작은 항이다. '''YI''' 또한 그러한 항이다. '''Y'''는 표준이며, '''Y'''gg('''Y'''g)가 된다. 위에 정의된 TRUE와 FALSE는 일반적으로 '''T'''와 '''F'''로 줄여서 사용한다.

7. 4. 추상화 제거

조합 논리를 사용하여 람다 추상화를 제거할 수 있다. 만약 ''N''이 추상화가 없는 람다 항이고, 조합자를 포함할 수 있다면, ''N''과 동등하지만 추상화가 없는 람다 항 ''T''(,''N'')이 존재한다. 이는 변수를 익명화하는 것으로 볼 수 있는데, ''T''(,''N'')은 ''N''에서 의 모든 발생을 제거하는 동시에, 인자 값을 ''N''이 를 포함하는 위치에 대체할 수 있도록 한다. 변환 함수 ''T''는 다음과 같이 정의할 수 있다.

: ''T''(, ) := '''I'''

: ''T''(, ''N'') := '''K''' ''N'' (단, 가 ''N''에서 자유 변수가 아닐 때)

: ''T''(, ''M'' ''N'') := '''S''' ''T''(, ''M'') ''T''(, ''N'')

어떤 경우든, ''T''(,''N'') ''P'' 형태의 항은 초기 조합자 '''I''', '''K''', 또는 '''S'''가 인자 ''P''를 가져옴으로써 축약될 수 있는데, 이는 ''N'' ''P''의 β-축약과 같다. '''I'''는 해당 인자를 반환한다. '''K'''는 인자를 버리는데, 이는 가 ''N''에서 자유롭게 발생하지 않는다면 ''N''이 하는 것과 같다. '''S'''는 인자를 응용의 두 하위 항에 모두 전달한 다음, 첫 번째 하위 항의 결과를 두 번째 하위 항의 결과에 적용한다.

조합자 '''B'''와 '''C'''는 '''S'''와 유사하지만, 인자를 응용의 하나의 하위 항에만 전달한다('''B'''는 "인자" 하위 항에, '''C'''는 "함수" 하위 항에). 그래서 하나의 하위 항에 가 발생하지 않는 경우 후속 '''K'''를 저장한다. '''B'''와 '''C'''와 비교하여, '''S''' 조합자는 실제로 인자 재정렬 및 인자 복제(두 위치에서 사용할 수 있도록)의 두 가지 기능을 병합한다. '''W''' 조합자는 후자만 수행하여 B, C, K, W 시스템을 SKI 조합자 계산법의 대안으로 제공한다.

8. 형식적 정의

람다 대수는 다음 요소들로 구성된 람다 표현식을 사용한다.^[17]

변수 ''v''₁, ''v''₂, ...
추상 기호 λ (람다)와 . (점)
괄호 ()

람다 표현식의 집합 Λ는 귀납적 정의를 사용하여 다음과 같이 정의할 수 있다.

# ''x''가 변수이면, ''x'' ∈ Λ이다.

# ''x''가 변수이고 ''M'' ∈ Λ 이면, (λ''x''.''M'') ∈ Λ이다. 이를 ''추상화''라고 한다.

# ''M'' ∈ Λ 이고 ''N'' ∈ Λ 이면, (''M'' ''N'') ∈ Λ이다. 이를 ''적용''이라고 한다.

이러한 규칙은 바커스-나우르 표기법으로도 표현할 수 있다.

```bnf

:== | |

:== λ .

:== ( )

:== v1 | v2 | ...

```

람다 대수의 언어는 변수, 상수, 람다 기호, 괄호, 온점으로 구성된다. 람다 항은 변수와 상수들로부터 시작하여 유한번의 적용 및 추상화를 하여 만들어진다.

람다 표현식 표기시 괄호 사용을 줄이기 위해 다음 규칙을 적용한다.

가장 바깥쪽 괄호는 생략한다.
적용은 왼쪽 결합 법칙을 따른다.^[18]
추상화의 본문은 가능한 한 오른쪽으로 확장된다.
일련의 추상화는 축약된다.^[20]^[18]

람다식은 '''자유 변수'''(λ에 의해 바운딩되지 않은 변수)를 포함할 수 있다. 람다 추상에 의해 묶이지 않은 변수를 '''자유 변수'''라고 한다.

추상 연산자 λ는 변수를 묶는다. 묶인 변수는 속박 변수, 그렇지 않은 변수는 자유 변수이다. 자유 변수가 없는 람다 표현식을 ''닫혀 있다''라고 하며, 조합 논리의 항과 동일한 ''결합자''라고도 한다.

8. 1. 정의

람다 표현식은 다음 요소들로 구성된다.

변수 ''v''₁, ''v''₂, ...
추상 기호 λ (람다)와 . (점)
괄호 ()

람다 표현식의 집합 Λ는 귀납적 정의를 사용하여 다음과 같이 정의할 수 있다.^[17]

# ''x''가 변수이면,

# ''x''가 변수이고 이면

# 이면

여기서 규칙 2는 ''추상화'', 규칙 3은 ''적용''이라고 불린다.

이러한 규칙은 바커스-나우르 표기법으로도 표현할 수 있다.

```bnf

:== | |

:== λ .

:== ( )

:== v1 | v2 | ...

```

람다 대수의 언어는 변수, 상수, 람다 기호, 괄호, 온점으로 구성된다. 변수와 상수는 람다 항의 기초 구성원들이며, 람다 항에 등장하는 자유 변수는 치환 연산을 통해 다른 람다 항으로 치환될 수 있다. 람다 기호는 추상화 연산을 나타내는 기호이다. 괄호와 온점은 이론적으로는 불필요하지만, 여러 가지 편의를 위해 사용된다.

람다 항은 변수와 상수들로부터 시작하여 유한번의 적용 및 추상화를 하여 만들어지는 람다 대수 기호들의 문자열이다. 즉 람다 항은 다음과 같이 정의된다.

모든 변수와 상수는 람다 항이다.
두 람다 항 $M$ , $N$ 에 대하여, 문자열 $(MN)$ 은 람다 항이다. 이를 $N$ 에 대한 $M$ 의 '''적용'''이라고 한다.
람다 항 $M$ 및 변수 $x$ 에 대하여, 문자열 $(\lambda x.M)$ 은 람다 항이다. 이를 $x$ 에 대한 $M$ 의 '''추상화'''라고 한다.

괄호 사용을 줄이기 위해 다음과 같은 표기법을 사용한다.

$M_1M_2\cdots M_n$ 은 $(\cdots((M_1M_2)M_3)\cdots M_n)$ 을 나타낸다.
$\lambda x.M_1\cdots M_n$ 은 $(\lambda x.(\cdots((M_1M_2)M_3)\cdots M_n))$ 을 나타낸다.
$\lambda x_1.\cdots\lambda x_n.M$ (또는 $\lambda x_1\cdots x_n.M$ )은 $(\lambda x_1.\cdots(\lambda x_{n-1}.(\lambda x_n.M))\cdots)$ 을 나타낸다.

8. 2. 표기법

람다 표현식의 표기를 깔끔하게 유지하기 위해 일반적으로 다음 규칙이 적용된다.

가장 바깥쪽 괄호는 생략한다: (''M'' ''N'') 대신 ''M'' ''N''.
적용은 왼쪽 결합 법칙을 따른다고 가정한다: ((''M'' ''N'') ''P'') 대신 ''M'' ''N'' ''P''로 표기할 수 있다.^[18]
모든 변수가 한 글자인 경우, 적용에서의 공백을 생략할 수 있다: ''M'' ''N'' ''P'' 대신 ''MNP''.^[19]
추상화의 본문은 가능한 한 오른쪽으로 확장된다: λ''x''.''M N''은 (λ''x''.''M'') ''N''이 아닌 λ''x''.(''M N'')을 의미한다.
일련의 추상화는 축약된다: λ''x''.λ''y''.λ''z''.''N''은 λ''xyz''.''N''으로 축약된다.^[20]^[18]

예를 들어, 어떤 수에 2를 더하는 함수 ''f''를 람다 계산의 식으로 표현하면 λ''x''. ''x'' + 2로 쓰인다. 변수 ''x''의 이름은 중요하지 않으며, λ''y''. ''y'' + 2라고 써도 같다. 함수의 적용은 좌결합이다. 즉, ''f'' ''x'' ''y'' = (''f'' ''x'') ''y''이다.

람다 계산에서는 함수의 인자는 항상 1개이다. 인자를 2개 취하는 함수는, 1개의 인자를 취하고, 1개의 인자를 취하는 함수를 반환하는 함수로 표현된다(커링). 예를 들어, 함수 ''f''(''x'', ''y'') = ''x'' − ''y''는 λ''x''. (λ''y''. ''x'' − ''y'')가 된다. 이 식은 관례로 λ''xy''. ''x'' − ''y''라고 생략해서 쓰는 경우가 많다.

람다식은 '''자유 변수'''(λ에 의해 바운딩되지 않은 변수)를 포함할 수도 있다. 예를 들어, 입력에 관계없이 항상 ''y''를 반환하는 함수를 나타내는 식 λ''x''. ''y''에서, 변수 ''y''는 자유 변수이다.

람다 추상에 의해 묶이지 않은 변수를 '''자유 변수'''(free variable)라고 한다. 식 λ*x*. (*x* *y*)에서 *y*는 자유 변수이다. 어떤 변수의 출현이 자유 출현인지 여부는, 더 정확하게는 다음과 같이 귀납적으로 정의된다.

# 람다식 *V*가 변수일 때, *V*는 자유 출현이다.

# 람다식 λ*V*. *E*에서, *E*에서 자유 출현하는 변수 중 *V* 이외의 것이 자유 출현이다. 이 때, *E* 내의 변수 *V*는 람다에 묶였다고 한다.

# 람다식 (*E* *E'*)에서, *E*에서의 자유 출현과 *E'*에서의 자유 출현의 합이 자유 출현이다.

8. 3. 자유 변수와 속박 변수

추상 연산자 λ는 변수를 묶는다. 람다 표현식 ''M''의 ''자유 변수'' 집합은 FV(''M'')으로 표시되며, 다음과 같이 정의된다.

# FV(''x'') = {''x''} (여기서 ''x''는 변수)

# FV(λ''x''.''M'') = FV(''M'') \ {''x''}

# FV(''M N'') = FV(''M'') ∪ FV(''N'')

묶인 변수는 속박 변수, 그렇지 않은 변수는 자유 변수이다. 예를 들어, 식 λ''y''.''x x y''에서 ''y''는 묶인 변수이고 ''x''는 자유 변수이다. 또한 변수는 가장 가까운 추상화에 의해 묶인다. 다음 예에서 식에 있는 ''x''의 단일 발생은 두 번째 람다에 의해 묶인다: λ''x''.''y'' (λ''x''.''z x'').

자유 변수가 없는 표현식을 ''닫혀 있다''라고 한다. 닫힌 람다 표현식은 조합 논리의 항과 동일한 ''결합자''라고도 한다.

9. 축약

람다 표현식의 의미는 표현식이 어떻게 축약될 수 있는지에 의해 정의된다.^[22]

축약에는 세 가지 종류가 있다.

'''α-변환''': 결합 변수를 변경하는 것이다. 자세한 내용은 α-변환 하위 문단에서 다룬다.
'''β-축약''': 함수를 인수에 적용하는 것이다. 자세한 내용은 β-축약 하위 문단에서 다룬다.
'''η-축약''': 외연성의 개념을 포착한다. 자세한 내용은 η-축약 하위 문단에서 다룬다.

두 표현식이 α-변환을 통해 동일한 표현식으로 변환될 수 있다면, 이들은 ''α-동치''라고 하며, β-동치와 η-동치도 유사하게 정의된다.

''리덱스''(redex)는 '축약 가능한 표현식'의 줄임말로, 축약 규칙 중 하나에 의해 축약될 수 있는 하위 항을 의미한다. 예를 들어, (λ''x''.''M'') ''N''은 ''M''에서 ''x''를 ''N''으로 치환하는 것을 표현하는 β-리덱스이다. 리덱스가 축약되는 표현식을 그 ''축약물''(reduct)이라고 하며, (λ''x''.''M'') ''N''의 축약물은 ''M''[''x'' := ''N'']이다.

만약 ''x''가 ''M''에서 자유롭게 나타나지 않는다면, λ''x''.''M x'' 역시 η-리덱스이며, 축약물은 ''M''이다.

9. 1. α-변환

'''α-변환'''(알파-변환)은 묶인 변수의 이름을 변경하는 규칙이다.^[23] 예를 들어, λ''x''.''x''를 α-변환하면 λ''y''.''y''를 얻을 수 있다. α-변환을 통해 같은 함수를 나타내는 람다식들을 '''α-동치'''라고 하며, 종종 같은 것으로 간주한다.

α-변환에는 몇 가지 규칙이 있다.

추상화를 α-변환할 때, 이름이 바뀌는 변수는 같은 추상화에 묶인 변수여야 한다. 예를 들어, λ''x''.λ''x''.''x''의 α-변환은 λ''y''.λ''x''.''x''는 될 수 있지만, λ''y''.λ''x''.''y''는 될 수 없다. 이는 프로그래밍에서 변수 그림자 가리기와 유사하다.
α-변환은 변수가 다른 추상화에 의해 캡처되는 경우에는 적용할 수 없다. 예를 들어, λ''x''.λ''y''.''x''에서 ''x''를 ''y''로 바꾸면 λ''y''.λ''y''.''y''가 되는데, 이는 원래 식과 다르다.

정적 범위를 사용하는 프로그래밍 언어에서, α-변환은 변수 이름이 포함하는 범위 내의 이름을 가리지 않도록 하여 이름 확인을 간단하게 만들 수 있다. (α-이름 바꾸기를 통해 이름 확인을 간단하게 만들기 참조)

드 브라윈 지수 표기법에서는 α-동치인 두 용어는 구문적으로 동일하다.

람다 대수에서 결합 변수의 이름은 중요하지 않다. 예를 들어, λ''x''. ''x'' 와 λ''y''. ''y''는 같은 함수를 나타낸다. 하지만, 어떤 결합 변수의 이름을 바꿀 때는 주의해야 한다. 예를 들어, λ''x''. λ''y''. ''x'' 에서 ''x''를 ''y''로 바꾸면 λ''y''. λ''y''. ''y''가 되는데, 이는 원래 식과 전혀 다르다.

변수 ''V'', ''W''와 식 ''E''에 대해, ''E'' 안의 ''V''의 모든 자유 출현을 ''W''로 치환한 것을 ''E''[''V'' := ''W''] 로 표기한다. α-변환 규칙은 다음과 같다.

: λ''V''. ''E'' →^α λ''W''. ''E''[''V'' := ''W'']

단, ''E''에 ''W''가 자유롭게 나타나지 않고, ''V''를 치환했을 때 ''E'' 안에서 ''W''가 새롭게 묶이지 않아야 한다. 이 규칙에 따라, λ''x''. (λ''x''. ''x'') ''x'' 는 λ''y''. (λ''x''. ''x'') ''y'' 로 변환할 수 있다.

9. 2. β-축약

Beta reduction^영어(베타 감소)는 함수 적용이라는 아이디어를 포착한다. 베타-감소는 치환을 통해 정의된다. (λ''x''.''M'') ''N''의 베타-감소는 ''M''[''x'' := ''N'']이다.^[42]

예를 들어, 2, 7, ×의 인코딩이 있다고 가정하면 다음과 같은 베타-감소가 가능하다. (λ''n''.''n'' × 2) 7 → 7 × 2.

베타-감소는 커리-하워드 동형사상을 통해 자연 연역에서의 '지역적 축약 가능성'과 동일한 개념으로 볼 수 있다. 예를 들어, 어떤 수에 2를 더하는 함수 ''f''를 생각해 보자. 이것은 일반적인 표기법으로는 ''f''(''x'') = ''x'' + 2라고 쓸 수 있다. 이 함수 ''f''는 람다 계산에서 람다식 λ''x''. ''x'' + 2로 쓰인다. 변수 ''x''의 이름은 중요하지 않으며, λ''y''. ''y'' + 2라고 써도 같다. 마찬가지로, 이 함수에 3을 적용한 결과 ''f''(3)은 (λ''x''. ''x'' + 2) 3으로 쓰인다. 함수의 적용은 좌결합이다. 즉, ''f'' ''x'' ''y'' = (''f'' ''x'') ''y''이다. 이번에는, 인자(함수의 입력)에 함수를 취하여 거기에 3을 적용하는 함수를 생각해 보자. 이것은 람다식으로는 λ''f''. ''f'' 3이 된다. 이 함수에, 아까 만든 2를 더하는 함수를 적용하면, (λ''f''. ''f'' 3) (λ''x''. ''x'' + 2)가 된다. 여기서,

: (λ''f''. ''f'' 3) (λ''x''. ''x'' + 2) , (λ''x''. ''x'' + 2) 3 , 3 + 2

의 3개의 표현은 모두 동치이다.

베타 축약(베타 변환)의 기본적인 아이디어는 함수의 적용이다. 베타 축약은 다음 변환이다.

: ((λ''V''. ''E'') ''E''') →^β ''E''[''V'' := ''E'']

단, ''E'''의 대입에 의해 ''E''' 중의 자유 변수가 새롭게 속박되지 않을 때에 한한다.^[42]

관계 ==는 위의 두 규칙을 포함하는 최소의 동치 관계(동치 폐포)이다.

베타 축약은 (동치 관계가 아닌) 좌변에서 우변으로의 일방적인 변환으로 볼 수도 있다. 베타 축약의 여지가 없는 람다식, 즉, ((λ''V''. ''E'') ''E''')의 형태(β-redex)를 어디에도 갖고 있지 않은 람다식을 '''정규형'''이라고 한다.

9. 3. η-축약

'''η-변환''' (에타 변환)은 확장성의 개념을 나타낸다.^[24] 이 맥락에서 두 함수가 모든 인수에 대해 동일한 결과를 제공하는 경우에만 동일하다는 것이다. η-변환은 λ''x''.''f'' ''x''와 ''f'' 사이를 ''x''가 ''f''에서 자유 변수로 나타나지 않을 때마다 변환한다.

η-변환은 커리-하워드 동형 사상을 통해 자연 연역에서의 ''국소 완전성'' 개념과 동일한 것으로 볼 수 있다.

η-변환의 기본적인 아이디어는 함수의 외연성인데, 이는 두 함수가 모든 인수에 대해 항상 같은 값을 반환할 때 서로 동치라고 간주하는 개념이다. η-변환은 다음과 같은 변환이다.

: λ''V''. ''E'' ''V'' →^η ''E''

단, ''E''에 ''V''가 자유롭게 나타나지 않을 때에 한한다.

이 동치성은 함수의 외연성이라는 개념에 의해 다음과 같이 나타난다.

만약 모든 람다식 ''a''에 대해 ''f'' ''a'' == ''g'' ''a''라면, ''a''로서 ''f''에도 ''g''에도 자유롭게 나타나지 않는 변수 ''x''를 취함으로써 ''f'' ''x'' == ''g'' ''x''이며, λ''x''. ''f'' ''x'' == λ''x''. ''g'' ''x''이다. 이 등식에 η-변환을 적용함으로써 ''f'' == ''g''가 얻어진다. 이로부터, η-변환을 인정한다면 함수의 외연성이 정당하다는 것이 증명된다.

반대로, 함수의 외연성을 인정한다고 하자. 먼저, 모든 ''y''에 대해 람다식 (λ''x''. ''f'' ''x'') ''y''는 베타 변환이 가능하며, (λ''x''. ''f'' ''x'') ''y'' == ''f'' ''y''가 된다. 이 동치 관계는 모든 ''y''에 대해 성립하므로, 함수의 외연성에 의해 λ''x''. ''f'' ''x'' == ''f''이다. 이상으로써, 함수의 외연성을 인정했을 때의 η-변환의 정당성이 증명된다.

10. 정규형과 합류성

타입이 없는 람다 대수의 경우, β-감소는 재작성 규칙으로서 강력 정규화도 아니고 약 정규화도 아니다.

그러나 α-변환까지 고려할 때(즉, 하나의 정규형을 다른 것으로 α-변환할 수 있다면 두 정규형을 동일하다고 간주), β-감소는 합류적임을 보일 수 있다.

따라서 강력 정규화 항과 약 정규화 항 모두 고유한 정규형을 갖는다. 강력 정규화 항의 경우, 어떤 감소 전략을 사용하더라도 정규형을 얻을 수 있지만, 약 정규화 항의 경우, 일부 감소 전략은 정규형을 찾지 못할 수 있다. 일반적으로 람다식 안에 β-변환할 수 있는 부분식이 여러 개 있는 경우, 어디부터 평가를 수행하는지에 따라 평가 경과는 여러 개 존재한다. 이들 여러 경과로부터 더욱 평가함으로써, 같은 람다식을 얻을 수 있는 성질을 처치-로서 정리(Church-Rosser property) 또는 합류성이라고 부른다. 또한, 어떤 람다식으로부터 한 번의 β-간약에 의해 얻어진 두 개의 람다식이, 같은 람다식으로 β-변환된다는 성질은 약 처치-로서 정리(Weak Church-Rosser property)라고 불린다. 처치-로서 정리를 갖는 체계는 약 처치-로서 정리도 갖지만, 그 역은 반드시 성립하지 않는다.

처치-로서 정리는 본고에서 다루고 있는 무형 람다 계산의 체계에서는 성립하는 것으로 알려져 있다. 그러나 그 외의 체계, 예를 들어 형을 붙여 확장된 람다 계산의 체계 등에서는 반드시 성립한다고는 할 수 없다.

11. 데이터 타입 인코딩

람다 대수 자체에는 정수나 덧셈 등이 존재하지 않지만, 산술 연산과 정수는 특정 람다식의 생략이라고 정의함으로써 인코딩할 수 있다.

자연수를 람다식으로 표현하는 방법에는 여러 가지가 있는데, 그중 가장 일반적인 것은 Church numerals|처치 수^영어라고 불리는 것으로, 다음과 같이 정의된다.

수	람다식 표현
0	λf x. x
1	λf x. f x
2	λf x. f (f x)
3	λf x. f (f (f x))

이후는 위와 동일하다. 직관적으로, 수 ''n''은 람다식에서 ''f''라는 함수를 받아서 그것을 ''n''번 적용한 것을 반환하는 함수이다. 즉, 처치 수는 1개의 인수를 받는 함수를 받아서 1개의 인수를 받는 함수를 반환하는 고차 함수이다. (처치가 제안한 원래의 람다 계산은 람다식의 인수가 적어도 한 번은 함수의 본체에 나타나야 했다. 따라서 그 체계에서는 위에 언급한 0의 정의는 불가능하다.)

위의 처치 수 정의에 따라, 후속자 (후자)를 계산하는 함수, 즉 ''n''을 받아서 ''n'' + 1을 반환하는 함수를 정의할 수 있다. 그것은 다음과 같다.

`SUCC` := λ''n'' ''f'' ''x''. ''f'' (''n'' ''f'' ''x'')

덧셈은 다음과 같이 정의할 수 있다.

`PLUS` := λ''m'' ''n'' ''f'' ''x''. ''m'' ''f'' (''n'' ''f'' ''x'')

또는 단순히 SUCC를 사용하여 다음과 같이 정의해도 좋다.

`PLUS` := λ''m'' ''n''. ''m'' `SUCC` ''n''

`PLUS`는 두 개의 자연수를 받아서 하나의 자연수를 반환하는 함수이다. 예를 들어 `PLUS` `2` `3` == `5`임을 확인할 수 있다. 곱셈은 다음과 같이 정의된다.

`MULT` := λ''m'' ''n''. ''m'' (`PLUS` ''n'') 0

이 정의는 ''m''과 ''n''의 곱셈이 0에 ''n''을 ''m''번 더하는 것과 같다는 것을 이용하여 만들어졌다. 더 짧게는 다음과 같이 정의할 수도 있다.

`MULT` := λ''m'' ''n'' ''f''. ''m'' (''n'' ''f'')

양의 정수 ''n''의 선행자 (전자)를 계산하는 함수 `PRED` ''n'' = ''n'' − 1은 간단하지 않으며, 다음과 같이 정의된다.

`PRED` := λ''n'' ''f'' ''x''. ''n'' (λ''g'' ''h''. ''h'' (''g'' ''f'')) (λ''u''. ''x'') (λ''u''. ''u'')

또는

`PRED` := λ''n''. ''n'' (λ''g'' ''k''. (''g'' `1`) (λ''u''. `PLUS` (''g'' ''k'') `1`) ''k'') (λ''v''. `0`) `0`

위의 부분식 (''g'' `1`) (λ''u''. `PLUS` (''g'' ''k'') `1`) ''k''는 ''g''(1)이 0이 될 때 ''k''로 평가되고, 그렇지 않을 때는 ''g''(''k'') + 1로 평가된다.^[42]

자연수에서 자연수로의 함수 ''F'': '''N''' → '''N'''가 계산 가능하다는 것은, 모든 자연수의 쌍 ''X'', ''Y''에 대해 ''F''(''X'') = ''Y''와 ''f'' ''x'' == ''y''가 동치가 되는 람다식 ''f''가 존재한다는 것으로 정의할 수 있다. 여기서 ''x'', ''y''는 각각 ''X'', ''Y''에 대응하는 처치 수에 의한 람다식이다. 이는 계산 가능성을 정의하는 여러 방법 중 하나이다. 자세한 내용은 처치-튜링 명제를 참고하라.

12. 타입 있는 람다 대수

'''타입 있는 람다 대수'''는 익명 함수 추상화를 나타내기 위해 람다 기호( $\lambda$ )를 사용하는 타입이 있는 형식 체계이다. 이 맥락에서 타입은 일반적으로 람다 항에 할당되는 구문적 성격의 객체이다. 타입의 정확한 성격은 고려되는 계산법에 따라 다르다(타입 있는 람다 대수의 종류 참조). 어떤 관점에서는 타입 있는 람다 대수를 타입이 없는 람다 대수의 정교화로 볼 수 있지만, 다른 관점에서는 더 기본적인 이론으로 간주할 수 있으며 '''타입이 없는 람다 대수'''는 단 하나의 타입만 있는 특수한 경우로 간주할 수도 있다.^[30]

타입 있는 람다 대수는 기초 프로그래밍 언어이며 ML, 하스켈과 같은 타입이 있는 함수형 프로그래밍 언어와 간접적으로는 타입이 있는 명령형 프로그래밍 언어의 기반이다. 타입 있는 람다 대수는 프로그래밍 언어의 타입 시스템 설계를 하는 데 중요한 역할을 한다. 여기서 타입 가능성은 일반적으로 프로그램의 바람직한 속성을 포착하는데, 예를 들어 프로그램이 메모리 접근 위반을 일으키지 않는 속성등을 들 수 있다.

타입 있는 람다 대수는 커리-하워드 동형사상을 통해 수학적 논리 및 증명 이론과 밀접하게 관련되어 있으며 범주론의 클래스인 내부 언어로 간주할 수 있다. 예를 들어, 단순 타입 람다 대수는 데카르트 닫힌 범주 (CCC)의 언어이다.

13. 축소 전략

항이 정규화되는지 여부와, 정규화가 필요한 경우 얼마나 많은 작업이 필요한지는 사용된 리덕션 전략에 크게 좌우된다.^[31]^[32]^[33]

정규 순서: 가장 왼쪽의 가장 바깥쪽 리덱스가 먼저 축약된다. 즉, 가능한 경우 인수가 축약되기 전에 인수가 추상화의 본문에 치환된다. 항에 베타 정규형이 있는 경우, 정규 순서 리덕션은 항상 해당 정규형에 도달한다.
적용 순서: 가장 왼쪽의 가장 안쪽 리덱스가 먼저 축약된다. 결과적으로 함수의 인수는 함수에 치환되기 전에 항상 축약된다. 정규 순서 리덕션과 달리 적용 순서 리덕션은 그러한 정규형이 존재하더라도 표현식의 베타 정규형을 찾지 못할 수 있다. 예를 들어, 항 (λx.y (λz.(zz) λz.(zz)))는 적용 순서에 의해 그 자체로 축약되는 반면, 정규 순서는 이를 베타 정규형 y로 축약한다.
전체 β-리덕션: 언제든지 모든 리덱스를 축약할 수 있다. 이것은 본질적으로 특정 리덕션 전략의 부재를 의미한다. 즉, 축약 가능성에 관해서는 "모든 예측이 빗나갑니다".

약한 리덕션 전략은 람다 추상화 아래에서 축약하지 않는다.

값 호출: 적용 순서와 같지만 추상화 내부에서는 리덕션이 수행되지 않는다. 이것은 C와 같은 엄격한 언어의 평가 순서와 유사하다. 함수에 대한 인수는 함수를 호출하기 전에 평가되고, 함수의 본문은 인수가 치환될 때까지 부분적으로도 평가되지 않는다.
이름 호출: 정규 순서와 같지만 추상화 내부에서는 리덕션이 수행되지 않는다. 예를 들어, λ''x''.(λ''y''.''y'')''x''는 이 전략에 따르면 정규형이지만 (λ''y''.''y'')''x'' 리덱스를 포함한다.

공유를 사용하는 전략은 "같은" 계산을 병렬로 줄인다.

최적 리덕션: 정규 순서와 같지만 동일한 레이블을 가진 계산은 동시에 축약된다.
필요 호출: 이름 호출과 같지만 (따라서 약함) 용어를 복제하는 함수 적용은 대신 인수를 명명한다. 인수는 "필요할 때" 평가될 수 있으며, 이 시점에서 이름 바인딩은 축약된 값으로 업데이트된다. 이것은 정규 순서 평가에 비해 시간을 절약할 수 있다.

14. 계산 복잡도

람다 대수의 계산 복잡도 개념은 β-축소의 비용이 구현 방식에 따라 달라질 수 있기 때문에 약간 까다롭다.^[34] 바운드 변수 ''V''가 표현식 ''E''에서 발생하는 모든 위치를 찾아야 하는데, 이는 시간 비용을 의미하거나, 자유 변수의 위치를 추적해야 하는데, 이는 공간 비용을 의미한다. ''E''에서 ''V''의 위치를 무작정 검색하는 것은 ''E''의 길이 ''n''에 대해 ''O''(''n'')이다. 디렉터 문자열은 이러한 시간 비용을 2차 공간 사용량으로 절충하는 초기 접근 방식이었다.^[35]

2014년에, 항을 축소하기 위해 정규 순서 축소에 의해 수행된 β-축소 단계의 수가 ''합리적인'' 시간 비용 모델임이 입증되었다.^[36] 즉, 축소는 단계 수에 비례하는 시간 내에 튜링 머신에서 시뮬레이션 될 수 있다. 이는 β-축소 단계마다 크기가 기하급수적으로 증가하는 람다 항이 존재하기 때문에 오랫동안 해결되지 않은 문제였다. 이 결과는 조밀하게 공유된 표현을 사용하여 이 문제를 해결한다. 람다 항을 평가하는 데 필요한 공간의 양이 축소 중인 항의 크기에 비례하지 않음을 명확히 한다. 현재 공간 복잡성의 좋은 척도가 무엇인지 알려져 있지 않다.^[37]

불합리한 모델이 반드시 비효율적이라는 의미는 아니다. 최적 축소는 중복 작업을 피하기 위해 동일한 레이블을 가진 모든 계산을 한 단계에서 축소하지만, 주어진 항을 정규형으로 축소하기 위한 병렬 β-축소 단계 수는 항의 크기에 대해 대략 선형이다. 이는 합리적인 비용 척도로 보기에는 너무 작다. 왜냐하면 모든 튜링 머신은 튜링 머신의 크기에 선형적으로 비례하는 크기로 람다 대수에 인코딩될 수 있기 때문이다. 람다 항을 축소하는 데 드는 진정한 비용은 β-축소 자체 때문이 아니라 β-축소 중에 레덱스 중복을 처리하는 데서 비롯된다.^[38] 최적 축소 구현이 정규형으로의 가장 왼쪽 외부 단계 수와 같은 합리적인 비용 모델에 따라 측정될 때 합리적인지 여부는 알려져 있지 않지만, 람다 대수의 일부 조각에 대해 최적 축소 알고리즘이 효율적이고 가장 왼쪽 외부 단계에 비해 최대 2차 오버헤드를 갖는 것으로 나타났다.^[37]

15. 람다 대수와 프로그래밍 언어

피터 란딘은 1965년에 발표한 논문에서 람다 대수가 절차적 추상화와 절차(서브 프로그램)의 적용 방식을 제공하기 때문에 많은 프로그래밍 언어가 람다 대수에 그 기초를 두고 있다고 보았다.^[39] 람다 대수를 컴퓨터에 구현하려면 함수를 일급 객체로 다루어야 하며, 이는 스택 기반 프로그래밍 언어에서는 Funarg 문제로 알려져 있다.

람다 대수와 가장 밀접한 관계를 가진 프로그래밍 언어는 함수형 프로그래밍 언어이며, 이들은 본질적으로 몇몇 상수와 데이터 타입을 사용하여 람다 대수를 구현한다. Lisp에서는 함수의 정의에 람다 표기법의 한 변형을 사용하며, 더 나아가 순수 Lisp라고 불리는 Lisp의 서브셋은 람다 대수와 진정으로 등가이다.

함수를 일급 객체로 다룰 수 있는 것은 함수형 언어뿐만이 아니다. 파스칼 등 많은 명령형 프로그래밍 언어에서는 어떤 함수를 다른 함수의 인수로 제공하는 연산이 허용된다. C나 C++에서는 함수를 가리키는 포인터나 클래스형 함수 객체를 사용하여 같은 것을 실현할 수 있다. 이러한 기능은 서브 함수가 명시적으로 쓰여진 경우에만 사용할 수 있으므로, 이 기능이 그대로 고차 함수를 지원하는 것은 아니다. 몇몇 절차적인 객체 지향 프로그래밍 언어에서는 함수를 임의의 차수로 쓸 수 있다. 스몰토크나, 더 최근의 언어에서는 에펠(에이전트)이나 C#(대리자) 등에서 제공되는 기능이 그것이다. 예를 들어, 에펠의 인라인 에이전트 기능을 사용한 다음 코드는 람다식 λ''x''. ''x'' * ''x'' (값 호출)에 상당하는 객체를 나타낸다.

'''agent''' (x: REAL): REAL '''do Result''' := x * x '''end'''

16. 병렬성과 동시성

처치-로서 성질은 람다 대수에서 평가(β-감소)가 '어떤 순서'로든, 심지어 병렬로 수행될 수 있음을 의미한다. 이는 다양한 비결정적 평가 전략이 관련되어 있음을 의미한다. 그러나 람다 대수는 병렬성을 위한 명시적인 구성을 제공하지 않는다. 미래와 같은 구성을 람다 대수에 추가할 수 있다. 통신과 동시성을 설명하기 위해 다른 프로세스 계산이 개발되었다.^[1]

17. 의미론

데나 스콧은 스콧 연속 함수를 고려하여 람다 대수를 위한 모형을 제시했다. 이 연구는 프로그래밍 언어의 지시적 의미론의 기초를 형성했다. 람다 대수에는 상당한 양의 프로그래밍 관용구가 존재하는데, 이러한 관용구들 중 다수는 원래 람다 대수를 프로그래밍 언어 의미론의 기초로 사용하여, 람다 대수를 효과적으로 저수준 프로그래밍 언어로 사용하는 맥락에서 개발되었다.

참조

_[1] nlab explicit substitution
_[2] 논문 Computability and λ-Definability 1937-12
_[3] 웹사이트 Type Theory http://plato.stanfor[...] 2006-02-08
_[4] 서적 Categorial Investigations: Logical and Linguistic Aspects of the Lambek Calculus https://books.google[...] Foris Publications
_[5] 서적 Computing Meaning https://books.google[...] Springer
_[6] 서적 Concepts in Programming Languages https://books.google[...] Cambridge University Press
_[7] 간행물 Introduction to Lambda Calculus using Racket https://www.research[...] 2023-12-05
_[8] 서적 Basic Category Theory for Computer Scientists
_[9] 논문 A set of postulates for the foundation of logic
_[10] 논문 The Inconsistency of Certain Formal Logics 1935-07
_[11] 논문 Review of Haskell B. Curry, ''The Inconsistency of Certain Formal Logics'' 1942-12
_[12] 논문 An unsolvable problem of elementary number theory
_[13] 논문 A Formulation of the Simple Theory of Types
_[14] 서적 Mathematical Methods in Linguistics https://books.google[...] Springer
_[15] 웹사이트 The Lambda Calculus http://plato.stanfor[...]
_[16] Youtube Looking Backward; Looking Forward https://www.youtube.[...] Dana Scott
_[17] 서적 The Lambda Calculus: Its Syntax and Semantics https://www.elsevier[...] North Holland
_[18] 웹사이트 Example for Rules of Associativity http://www.lambda-bo[...] Lambda-bound.com 2012-06-18
_[19] 웹사이트 The Basic Grammar of Lambda Expressions https://softoption.u[...]
_[20] 간행물 Lecture Notes on the Lambda Calculus http://www.mathstat.[...] Department of Mathematics and Statistics, University of Ottawa
_[21] 간행물 Introduction to Lambda Calculus https://ftp.science.[...] 2000-03
_[22] 논문 A Proof-Theoretic Account of Programming and the Role of Reduction Rules
_[23] 간행물 Design concepts in programming languages MIT press
_[24] 뉴스 What's the motivation for η rules? https://mail.haskell[...] Luke Palmer 2010-12-29
_[25] 간행물 Programming Languages and Lambda Calculi http://www.cs.utah.e[...]
_[26] 간행물 Cyclic lambda calculi http://ix.cs.uoregon[...] Zena M. Ariola and Stefan Blom 1997
_[27] 웹사이트 Lambda Calculus and Types https://www.cs.ox.ac[...]
_[28] 서적 Rewriting and Typed Lambda Calculi 2014
_[29] 논문 Call-by-Value Lambda Calculus as a Model of Computation in Coq https://www.ps.uni-s[...] 2019-08
_[30] 문서 Types and Programming Languages Benjamin C. Pierce
_[31] 서적 Types and Programming Languages https://books.google[...] MIT Press
_[32] 서적 The Essence of Computation 2002
_[33] 논문 The Zoo of Lambda-Calculus Reduction Strategies, and Coq https://drops.dagstu[...] Schloss Dagstuhl – Leibniz-Zentrum für Informatik 2022
_[34] 서적 Functional Programming Languages and Computer Architecture: 5th ACM Conference. Cambridge, MA, USA, August 26-30, 1991. Proceedings Springer-Verlag 1991-08-26
_[35] 논문 Director Strings Revisited: A Generic Approach to the Efficient Representation of Free Variables in Higher-order Rewriting http://www.lsv.fr/Pu[...]
_[36] 서적 Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) 2014-07-14
_[37] 저널 (In)Efficiency and Reasonable Cost Models 2018-10
_[38] arXiv About the efficient reduction of lambda terms 2017-01-16
_[39] 저널 A Correspondence between ALGOL 60 and Church's Lambda-notation
_[40] 저널 A type-theoretical alternative to ISWIM, CUCH, OWHY https://www.cs.cmu.e[...] 2022-12-01
_[41] 웹사이트 Greg Michaelson's Homepage http://www.macs.hw.a[...] Heriot-Watt University 2022-11-06
_[42] 웹사이트 チャーチ数とpred関数 https://kimiyuki.net[...] 2018-10-06
_[43] 서적 Comprehensive Mathematics for Computer Scientists 2 Springer 2005
_[44] 문서 "Type Theory" http://plato.stanfor[...] The Stanford Encyclopedia of Philosophy 2013
_[45] 서적 Categorial Investigations: Logical and Linguistic Aspects of the Lambek Calculus https://books.google[...] Foris Publications
_[46] 인용 Computing Meaning https://books.google[...] Springer
_[47] 인용 Concepts in Programming Languages https://books.google[...] Cambridge University Press
_[48] 저널 A set of postulates for the foundation of logic
_[49] 문서
_[50] 저널 The Inconsistency of Certain Formal Logics https://archive.org/[...] 1935-07
_[51] 저널 Review of Haskell B. Curry, ''The Inconsistency of Certain Formal Logics'' 1942-12
_[52] 저널 An unsolvable problem of elementary number theory https://archive.org/[...]
_[53] 저널 A Formulation of the Simple Theory of Types
_[54] 서적 Mathematical Methods in Linguistics https://books.google[...] Springer 2016-12-29
_[55] 문서 "The Lambda Calculus" http://plato.stanfor[...] The Stanford Encyclopedia of Philosophy 2013

본 사이트는 AI가 위키백과와 뉴스 기사,정부 간행물,학술 논문등을 바탕으로 정보를 가공하여 제공하는 백과사전형 서비스입니다.
모든 문서는 AI에 의해 자동 생성되며, CC BY-SA 4.0 라이선스에 따라 이용할 수 있습니다.
하지만, 위키백과나 뉴스 기사 자체에 오류, 부정확한 정보, 또는 가짜 뉴스가 포함될 수 있으며, AI는 이러한 내용을 완벽하게 걸러내지 못할 수 있습니다.
따라서 제공되는 정보에 일부 오류나 편향이 있을 수 있으므로, 중요한 정보는 반드시 다른 출처를 통해 교차 검증하시기 바랍니다.

문의하기 : help@durumis.com