1. Introduction to Lambda Calculus
Introduction

πHistory
17μΈκΈ° λΌμ΄νλμΈ λ λ€μκ³Ό κ°μ μ΄μμ μΈ μ μμ νλ€.
- κ°λ₯ν λͺ¨λ λ¬Έμ λ₯Ό κΈ°μ ν μ μλ λ²μ©μΈμ΄λ₯Ό λ§λ λ€.
- λ²μ©μΈμ΄λ‘ κΈ°μ λλ λͺ¨λ λ¬Έμ λ₯Ό ν΄κ²°νκΈ° μν κ²°μ λ°©λ²μ μ°Ύλλ€.
μνμ λ¬Έμ μ νμ νλ€λ©΄, λΌμ΄νλμΈ μ 첫 λ²μ§Έ μ μμ νλ κ²μ λ¬μ
μ΄ν μ΄λ€ ννμ μ§ν© μ΄λ‘ μ΄
μΌμ°¨ μ μ΄ λ
Όλ¦¬μ μΈμ΄λ‘ ννλ κ²μΌλ‘ μΆ©μ‘±λμλ€.
λ λ²μ§Έ μ μμ μ€μν μ² νμ λ¬Έμ κ° λμλλ°, "λ²μ©μΈμ΄λ‘ μ μλ λͺ¨λ λ¬Έμ λ₯Ό ν΄κ²°ν μ μμκΉ?"λΌλ μ§λ¬Έμ΄μλ€.
보νΈμ μΌλ‘, κ·Έλ¬ν κ²μ λΆκ°λ₯νλ€κ³ 보μ΄μ§λ§, μ΄κ²μ μ¦λͺ
νλ λ°©λ²μ λͺ
ννμ§ μμλ€. μ΄λ¬ν μ§λ¬Έμ
Entscheidungsproblem(μμ¬κ²°μ λ¬Έμ )λ‘ μλ €μ§κ² λμλ€.
1936λ , Entscheidungsproblem(μμ¬κ²°μ λ¬Έμ )λ μλ‘ μ‘° μ²μΉ(Alonzo Church)μ μ¨λ° νλ§(Alan Turing)μ΄ λ 립μ μΌλ‘ λΆμ νμ¬ ν΄κ²°νμλ€. μ΄λ₯Ό μν΄μ, μ§κ΄μ μΈ 'κ²°μ κ°λ₯(decidable)'λλ λλ±ν μλ―Έλ‘ 'κ³μ°κ°λ₯(computable)'μ νμνκ° νμνλλ°, μ²μΉμ νλ§μ λκ°μ§ λ€λ₯Έ λ°©μμΌλ‘ κ³μ° λͺ¨λΈμ λμ νμ¬ ν΄κ²°νμλ€.
- μ²μΉ(1936)λ λλ€ κ³μ°λ²(lambda calculus)λΌλ νμ 체κ³λ₯Ό λ°λͺ νκ³ , μ΄ μμ€ν μ ν΅ν΄ κ³μ° κ°λ₯ν ν¨μμ κ°λ μ μ μνλ€.
- νλ§(1936/7)μ νλ§ λ¨Έμ (Turing machines)λΌκ³ λΆλ¦¬λ κΈ°κ³λ€μ λ°λͺ νκ³ , μ΄λ¬ν κΈ°κ³λ€μ ν΅ν΄ κ³μ° κ°λ₯ν κ°λ μ μ μνλ€.
λν 1936λ
μ νλ§μ λ λͺ¨λΈμ΄ λμΌν κ°λλ₯Ό κ°μ§λ©°, λ λͺ¨λΈμ΄ κ°μ κ³μ° κ°λ₯ν ν¨μλ€μ ν΄λμ€λ₯Ό μ μνλ€λ κ²μ μ¦λͺ
νμλ€. (Turing 1937)
νμ¬μ ν° λ
Έμ΄λ§ μ»΄ν¨ν°λ€μ νλ§ λ¨Έμ μ κ°λ
μ κΈ°λ°μΌλ‘ νλ€. κ°λ
μ μΌλ‘, ν° λ
Έμ΄λ§ μ»΄ν¨ν°λ€μ λλ€ μ‘μΈμ€ λ μ§μ€ν°λ₯Ό κ°μΆ νλ§ λ¨Έμ μΌλ‘ λ³Ό μ μλ€. ν¬νΈλ(Fortran), νμ€μΉΌ(Pascal)λ±μ λͺ
λ Ήν νλ‘κ·Έλλ° μΈμ΄λ€κ³Ό λͺ¨λ μ΄μ
λΈλ¦¬μ΄ μΈμ΄λ€μ νλ§ λ¨Έμ μ΄ μνλλ λ°©μμ κΈ°λ°νμ¬ μμ±λλ€.(λͺ
λ Ήλ¬Έμ μ°μμΌλ‘μ¨ νλ§ λ¨Έμ μ΄ μ§μλλ€.)
νμ€μΌ(Haskell), λ―Έλλ€(Miranda), ML λ±κ³Ό κ°μ ν¨μν νλ‘κ·Έλλ° μΈμ΄λ€μ λλ€ κ³μ°λ²μ κΈ°λ°μΌλ‘ νλ€. 리μ€ν(Lisp)λ
μ΄λ¬ν μΈμ΄λ€μ μ΄κΈ°(λΉλ‘ ν¨μνμΈμ΄ μνκ³μ λ
Όλμ΄ μμ§λ§..) μμλΌκ³ ν μ μλ€. 리λμ
λ¨Έμ (reduction machine)μ νΉν μ΄λ¬ν ν¨μν νλ‘κ·Έλλ° μΈμ΄λ€μ μ€νμ μν΄ μ€κ³λμλ€.
리μ€νλ μμν¨μν μΈμ΄κ° μλκΈ° λλ¬Έμ, νμ€μΌκ³Ό κ°μ λͺλͺ λ€λ₯Έ ν¨μν μΈμ΄λ€κ³Ό λμ‘°μ μ΄λ€. 리μ€νλ 리λμ λ¨Έμ μμμ μ€νλμ§λ§ λμμ λͺ λ Ήν νλ‘κ·Έλλ°κ³Ό λ³μ΄(mutability)λ νμ©νλ€. μ΄λ¬ν νΉμ± λλ¬Έμ νμ€μΌκ³Ό κ°μ μμν¨μν νλ‘κ·Έλλ¨Έλ€μ΄ 리μ€νλ₯Ό μ νΈνμ§ μμΌλ©°, μμ§κΉμ§λ "리μ€νλ μ§μ€λ‘ ν¨μν μΈμ΄μΈκ°?" μ κ°μ λ Όλμ΄ μλ€. λλ λνμ λ μΈκ³΅μ§λ₯ μμ μμ 리μ€νλ₯Ό λ°°μ κ³ , μκ³ λ¦¬μ¦, λ°μ΄ν° ꡬ쑰 κ³Όμ λ₯Ό 리μ€νλ‘ κ΅¬ννμ¬ μ μΆν μ λλ‘ λ¦¬μ€νμ λΉ μ§μ μ΄ μμλ€. νΉν κ΅λ΄μ λ²μμκ° μ λ¬Έμμ€μ 1κΆλ°μ μκΈ° λλ¬Έμ, λμκ΄μμ μ€λλ μμλ€μ λΉλ € μ½μλ κΈ°μ΅μ΄μλ€. μ λͺ ν μ± μ€μ SICP(λΉλ‘ schemeμ μ¬μ©νμ§λ§ μκ΄μλ€)λ ν΄ κ·Έλ μ΄μμ΄ μ΄ μ± λ€μ 보며 리μ€νμ 맀λ ₯μ λΉ μ Έλ³΄κΈΈ λ°λλ€.
πReduction and functional programming
ν¨μν νλ‘κ·Έλ¨μ μκ³ λ¦¬μ¦κ³Ό μ λ ₯μ λνλ΄λ ννμ λ‘ κ΅¬μ±λλ€. μ΄ ννμ λ μΌμ ν μ¬μμ± κ·μΉμ λ°λΌ λ체λ μ μλλ°,리λμ μ ννμ μ μΌλΆλΆ μ μ£Όμ΄μ§ μ¬μμ± κ·μΉμ λ°λΌ λ€λ₯Έ ννμ λ‘ λ체νλ κ²μ μλ―Ένλ€. κΈ°νΈμ μΌλ‘ νννλ©΄ λ€μκ³Ό κ°λ€. λ¨ μ κ·μΉμ λ°λΌ λ체 κ°λ₯ν κ²½μ°μ΄λ€. μ΄ λ¦¬λμ κ³Όμ μ κ²°κ³Όμ μΌλ‘ λ μ΄μ μ¬μμ±μ΄ λΆκ°λ₯ν λΆλΆμ΄ μλ ννμμ΄ λμ¬ λκΉμ§ λ°λ³΅λλ€. μ΄λ κ² μ»μ΄μ§ μ΅μ’ ννμμ μ κ·ν(normal form)μ΄λΌκ³ νλ©°, μ£Όμ΄μ§ ν¨μν νλ‘κ·Έλ¨μ μΆλ ₯κ°μ λνλΈλ€.
μμ:
μμ μμμμ 리λμ
κ·μΉμ μ«μλ€μ λν λ§μ
κ³Ό κ³±μ
μ 'ν(table)'λ‘ κ΅¬μ±λλ€.
ν¨μν νλ‘κ·Έλλ°μμλ 리λμ
μ ν΅ν΄ κΈ°νΈ μ°μ°(symbolic computation)μ΄ κ°λ₯νλ€. μλ₯Ό λ€μ΄, λ€μκ³Ό κ°μ΄
first of (sort (append ('dog', 'rabbit') (sort (('mouse', 'cat')))))
-> first of (sort (append ('dog', 'rabbit') ('cat', 'mouse')))
-> first of (sort ('dog', 'rabbit', 'cat', 'mouse'))
-> first of ('cat', 'dog', 'mouse', 'rabbit')
-> 'cat'.
μ΄λ¬ν κΈ°νΈ μ°μ° κ³Όμ μ appendμ sortμ κ°μ ν¨μλ€μ΄ μΌλΆ μ¬μμ± κ·μΉμ μν΄ μ μλ μ μμμ 보μ¬μ€λ€. μ¬μμ± κ·μΉμ ν΅ν΄ μ μλ μ΄λ¬ν ν¨μλ€μ 'μ½€λΉλ€μ΄ν°(combinator)'λΌκ³ λΆλ¦¬λ©°, ν¨μν νλ‘κ·Έλλ°μμ κΈ°νΈ λ°μ΄ν°λ₯Ό μ‘°μνκΈ° μν νμμ μΈ λκ΅¬λ‘ μ¬μ©λλ€.
리λμ μμ€ν μ μΌλ°μ μΌλ‘ μμ±μ λ§μ‘±νλλ°, μ΄λ μ»μ΄μ§ μ κ·νμ΄ νμ μ©μ΄λ€μ κ³μ° μμμ λ 립μ μ΄λΌλ κ²μ λνλΈλ€. μ€μ λ‘ μ²« λ²μ§Έ μμλ λ€μκ³Ό κ°μ΄ 리λμ λ μ μλ€.
νΉμ μ¬λ¬ ννμλ€μ λμμ νκ°ν¨μΌλ‘μ¨ λ λ¨μνκ² λ¦¬λμ λ μλ μλ€.
πApplication and abstraction
κ³μ°μ 첫 λ²μ§Έ κΈ°λ³Έ μμ μ μ μ©()μ΄λ€. ννμ λλ λ λ°μ΄ν° λ₯Ό μκ³ λ¦¬μ¦μΌλ‘ κ°μ£Όνμ¬ λ°μ΄ν° λ₯Ό μ λ ₯μΌλ‘ μ μ©νλ κ²μ λνλΈλ€. μ΄λ λ κ°μ§ κ΄μ μΌλ‘ λ³Ό μ μλλ°, κ³μ° κ³Όμ λλ μ΄ κ³Όμ μ μΆλ ₯μΌλ‘ λ³Ό μ μλ€. 첫 λ²μ§Έ κ΄μ μ λ³ν(conversion)λλ λ λμ 리λμ (reduction) κ°λ μΌλ‘ ν¬μ°©λλ©°, λ λ²μ§Έ κ΄μ μ λͺ¨λΈ(μλ―Έλ‘ ) κ°λ μΌλ‘ ννλλ€. μ΄ μ΄λ‘ μ νμ μ μ νμ΄ μλ€(type-free). μ¦, κ° μκΈ° μμ μκ² μ μ©λ μ κ°μ ννμμ κ³ λ €ν μ μλ€. μ΄λ μ¬κ·λ₯Ό λͺ¨λ°©νλλ° μ μ©νλ€.
λ€λ₯Έ κΈ°λ³Έ μμ
μ μΆμν()μ΄λ€. λ§μ½ λΌλ ννμμ΄ μ μμ‘΄νλ€λ©΄, λ ν¨μ λ₯Ό λνλΈλ€.
μ μ©()κ³Ό μΆμν()λ λ€μκ³Ό κ°μ μ§κ΄μ μΈ κ³΅μμμ ν¨κ» μλνλ€.
μ¦, μ ν¨μ μ μΈμ μ μ μ©νμ¬ λ‘ κ³μ°λλ©° κ°μ μ΄ λλ€. μΌλ°μ μΌλ‘ μμ λ€μκ³Ό κ°μ΄ μ°μ΄κΈ°λ νλ€.
μ¬κΈ°μ μ μ μ λμ
νλ κ²μ λνλ΄λλ°, λλκ²λ κ° κ³μ°μ μ μΌν νμμ μΈ κ³΅λ¦¬μ΄μ§λ§, κ·Έ κ²°κ³Όλ‘ μ»μ΄μ§λ μ΄λ‘ μ κ½€ 볡μ‘νλ€.
πFree and bound variables
μΆμνλ λ³μ λ₯Ό μμμ "λ¬Άλλ€"κ³ νννλ€. μλ₯Ό λ€μ΄, μμ λ λ¬Άμ¬μλ λ³μ(bound variable)μ΄κ³ λ μμ λ³μ(free variable)λΌκ³ νλ€. μΉν μ μ μμ λ±μ₯(free occurrences)μλ§ μ μ©λλ€
λ―Έμ λΆνμμλ μ μ¬ν λ³μ λ¬Άμ κ°λ
μ΄ μλ€. μμ λ³μ λ λ¬Άμ¬μκ³ λ μμ λ³μμ΄λ€.
λͺ
λ£μ±μ μν΄, νΉμ ννμμ λ±μ₯νλ λ¬ΆμΈ λ³μλ€μ μμ λ³μλ€κ³Ό λ€λ₯΄λ€κ³ κ°μ νλ€. μ΄κ²μ λ¬ΆμΈ λ³μλ€μ μ΄λ¦μ λ³κ²½ν¨μΌλ‘μ¨ μΆ©μ‘±ν μ μλλ°, μλ₯Ό λ€μ΄, λ λ‘ λ°λ μ μλ€. μ¬μ€, μ΄λ¬ν ννμλ€μ λμΌν λ°©μμΌλ‘ μλνλ€.
κ·Έλ¦¬κ³ μ¬μ€μ μ΄λ€μ κ°μ μλλ μκ³ λ¦¬μ¦μ λνλΈλ€. λ°λΌμ λ¬ΆμΈ λ³μλ€μ μ΄λ¦λ§ λ€λ₯Έ ννμλ€μ λμΌν κ²μΌλ‘ κ°μ£Όλλ€.
πFunctions of more arguments
μ¬λ¬ μΈμλ₯Ό κ°μ§λ ν¨μλ μ μ©μ λ°λ³΅ν¨μΌλ‘μ¨ μ»μ μ μλ€. μ΄ μμ΄λμ΄λ SchΓΆnfinkel(1924)μ μν΄ μ μλμμ§λ§, H.B. Curryκ° λ 립μ μΌλ‘ λμ ν ν μ΄λΌλ μ΄λ¦μΌλ‘ λ리 μλ €μ‘λ€. μ§κ΄μ μΌλ‘ κ° λ κ°μ μΈμμ μμ‘΄νλ€λ©΄, λ€μκ³Ό κ°μ΄ μ μν μ μλ€. κ·Έλ° λ€μ,
μ΄λ κ² ν¨μΌλ‘μ¨ λ μΈμλ₯Ό κ°μ§λ ν¨μ λ₯Ό λ¨μΌ μΈμ ν¨μ λ‘ λ³νν μ μλ€. μ΄λ¬ν κΈ°λ²μ λΌκ³ λΆλ¦¬λ©°, ν¨μν νλ‘κ·Έλλ°μμ ν¨μλ€μ λ μ μ°νκ² μ‘°μνλ λ°μ μ¬μ©λλ€.
λ§μ§λ§ μμ λ°λ³΅μ μΈ μ μ©μ λν΄ μΌμͺ½μΌλ‘ κ²°ν©νλ κ²μ΄ νΈλ¦¬νλ€λ κ²μ 보μ¬μ€λ€. μ μ κ·Έλ° λ€μ λ€μκ³Ό κ°μ΄ ννλλ€. μ΄μ λ§μ°¬κ°μ§λ‘, λ°λ³΅μ μΈ μΆμνλ μ€λ₯Έμͺ½μΌλ‘ κ²°ν©νλ κ²μ μ¬μ©νλ€. κ·Έλ¬λ©΄ μμμ μ μν μ λν΄ λ€μ κ·Έλ¦¬κ³ λ λ€μκ³Ό κ°μ΄ ννλλ€. κ°μ μΈμμ λν΄ λ€μκ³Ό κ°μ΄ νννλ€. λ² λ₯Ό μ¬μ©νμ¬ μ΄ μμ λ€μκ³Ό κ°μ΄ λ²‘ν° νκΈ°λ‘ ννλλ€. λ³΄λ€ μΌλ°μ μΌλ‘ λ€μκ³Ό κ°μ΄ νννλ€.