Skip to content

Lambda calculus #
Find similar titles

람다 대수(lambda calculus) #

서론 #

λ-calculus(람다 칼큘러스)는 논리학자 Alonzo Church가 개념을 정의한 수학적 모델이다. McCarthy가 람다 대수에서 영감을 받아 LISP를 만들었다.

본론 #

람다 대수는 세 가지로 표현된다.

  1. 변수
  2. x,y,z 등을 말하며 V, V1, V2 등으로 사용됩니다.
  3. 함수 적용 혹은 조합(Function applications or combinations)
  4. E1과 E2가 람다식일 경우 (E1 E2)로 표현됩니다.
  5. 추상화
  6. V가 변수이고 E가 람다 표현식일때 \(\lambda V.E \)로 추상화가 가능합니다.

BNF를 사용하여 λ-표현식을 표현하면 다음과 같이 됩니다. $$ \begin{array} \\ [\lambda-expression] ::= <variable> \\ \quad \quad \quad\quad\quad\quad\quad\quad| <\lambda-expression> <\lambda-expression>) \\ \quad\quad\quad\quad\quad\quad\quad\quad| (\lambda <variable> . <\lambda-expression> \end{array} $$ 앞의 식을 직관적으로 바꾸면 다음과 같다.[^1].[^2] $$ \begin{array} \\ E ::= V \;| ({E}_{1} \; {E}_{2}) \; | \; \lambda{V}.E \end{array} ] $$

  • 함수는 좌측으로 적용된다. $$ \begin{array} \\ {E}_{1} \; {E}_{2} \quad means \quad({E}_{1} \; {E}_{2}) \\ {E}_{1} \; {E}_{2} \; {E}_{3} \quad means \quad (({E}_{1} \; {E}_{2}) {E}_{3})\\ {E}_{1} \; {E}_{2}\; {E}_{3} \; {E}_{4} \quad means \quad ((({E}_{1} \; {E}_{2}) {E}_{3}){E}_{4})\\ \end{array} $$

  • \(lambda V. E_1 E_2 .. \) 는 \( (lambda V .(E_1 E_2 ... E_n) \)

\(\lambda V' \)는 오른쪽으로 확장이 가능하다.

  • \(\lambda V_1 ... V_n \) 는 \( (\lambda V_1 . ( ... .(\lambda V_n . E) ...)) \) $$ \begin{array} \\ \lambda{x} \,y. E \qquad means \quad (\lambda{x}.(\lambda{y}. E)) \\ \lambda{x} \,y\,z. E \qquad means \quad(\lambda{x}.(\lambda{y}(\lambda.z.E))) \\ \lambda{x} \,y\,z. E \qquad means \quad (\lambda{x}.(\lambda{y}(\lambda.z.(\lambda{w}.E)))) \\ \end{array}\\ $$ 예를 들면 다음과 같다. $$ \begin{array} \lambda{x} \; y. add \; y \; x \quad means \quad(\lambda{x}.(\lambda{y}. ((add \; y)x))) \end{array} $$

자유변수와 속박변수 #

변수 V가 있는 람다표현식 λV의 V가 속박변수(bound)이며 그렇지 않은 변수가 자유변수(free)다. \(\lambda x. y \; x )\)의 경우 y가 자유변수, 두번째 x가 속박변수다.

람다 변환 규칙 #

α-conversion(알파 변환) #

λV. E 식은 λV'. E[V'/V]로 변환됩니다. $$ λx. x\quad \overrightarrow { α } \quad λy. y \\ λx. ƒ\, x\quad \overrightarrow { α } \quad λy. ƒ y $$

다음의 예제는 (λy. add x y)[y/x]의 y가 속박변수 x로 대체될수 없다는 것을 보여준다. $$ \lambda x. \lambda y. add \; x\; y \quad \overrightarrow{\alpha} \quad \lambda y. \lambda y. add \; y \;y $$

β-conversion(베타 변환) #

베타 변환은 베타축약(β-reduction(β-redex))로도 할 수도 있다.

\( (\lambda V. E_1) E2) \) 같은 식에 적용되면 \( E_1 [E_2 / V] \)로 변환된다. 베타변환은 프로그래밍 언어에서 함수 실행을 평가하는것처럼 보여진다. $$ (λx. ƒ\, x)\, E \quad \overrightarrow { β } \quad ƒ \, E \\ (λx. (λy. add\, x\, y))\, \underline {3} \quad \overrightarrow { β } \quad λy. add\, \underline{3} \, y \\ (λy. add\, \underline{3} \, y) \,\underline{4} \, \overrightarrow { β } \, add \, \underline{3} \, \underline{4} $$ 아래의 예제는 (square y)의 y가 자유변수이기 때문에 \( (\lambda y. add x \; y)[(square \; y)/ x] \) 치환은 유효하지 않다는 것을 보여주고 있다. $$ (\lambda x.(\lambda y. add \; x \; y)) (square\; y) \quad \overrightarrow{\beta} \quad \lambda y. add (square\; y) y $$

η-conversion(에타 변환) #

두 함수가 같은 인수를 받고 같은 결과를 준다면 같은 함수다. $$ λx. add\, x\quad\overrightarrow { η } \quad add \\ λy. add\, x \, y \quad \overrightarrow { η } \quad add \,x $$ add xx가 자유변수일 경우 에타변환이 되지 않는다. $$ \lambda x . add x \; x \quad \overrightarrow{\eta} \quad add \;x $$

치환 #

E[E'/V]로 정의된 식이 E안의 각 자유변수 VE'로 치환됩니다.

알파변환과 베타변환에선 치환과 관련하여 명시하고 있다. $$ (λV. E1) \, E2\quad \overrightarrow { β }\quad E1[E2/V] \\ (\lambda V. E1) \, E2\, \rightarrow \, E1[E2/V] \quad and \quad \lambda V.E \rightarrow \lambda V'. E[V'/V] $$ E[E'/V]E에 대해 재귀적으로 정의됩니다.

Equality of lambda-expressions #

람다식의 세가지 변환을 하여도 똑같다는 것을 나타낸다. $$ \begin{array} \\ 1.\; E \equiv E_1 \\ 2. \; E' \equiv E_n \\ 3. \; for\;each\; i\; either \\ \quad (a) \; E_i \;\overrightarrow{α} \; E_{i+1} \; or \;E_i \;\overrightarrow{β} \; E_{i+1}\; or \; E_i \; \overrightarrow{η} \; E_{i+1} \;or \\ \quad (a) \; E_{i+1} \;\overrightarrow{α} \; E_{i} \; or \;E_{i+1} \;\overrightarrow{β} \; E_{i}\; or \; E_{i+1} \; \overrightarrow{η} \; E_{i} \;or \\ \end{array} $$ 동치의 정의는 다음을 따른다. $$ \begin{array} \\ (i) \;For \; any \; E ; it \; is \; the \; case \; that\; E = E\; (equality \; is\; reflexive) \\ (ii) \; If\; E = E', then \; E'= E \; (equality \; is \; symmertric) \\ (iii)\; If \; E=E' \; and \; E'=E'', then \; E=E'' (equality \; is \; transitive) \\ \end{array} $$ 중요한 점은 알파와 베타변환에서 가장 중요한 치환까지 유효하다는 것을 다음 예제에서 보여주고 있다. $$ \lambda x. \lambda y.\; x = \lambda y. \lambda y. y $$ 이는 다음과 같은 변환을 만족한다. $$ \begin{array} \\ (\lambda x.(\lambda y\; .x)) \underline{1} \underline{2} \quad\overrightarrow{ β} \quad (\lambda{y}. \underline1)\underline2 \quad \overrightarrow{ β} \quad \underline{1} \\ (\lambda x.(\lambda y\; .y)) \underline{1} \underline{2} \quad\overrightarrow{ β} \quad (\lambda{y}. y)\underline2 \quad \; \overrightarrow{ β} \quad \underline{2} \\ \end{array} $$

[^1]: V는 Varirable, E1,E2는 aplication(combinations), λV.E는 Abstraction를 뜻합니다.

[^2]: It took about 40 years for logicians (Dana Scoot, in fact[^3]) to make it rigorous in a useful way.

[^3]: Scott, D.S 'Models for various type free calculi'

Reference #

  • Programming Language Theory its Implemetation by Michael J. C. Gordon(1988)
0.0.1_20140628_0