Reading time: about 7 minutes (1275 words).
banner

πŸ”—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

ν•¨μˆ˜ν˜• ν”„λ‘œκ·Έλž¨μ€ μ•Œκ³ λ¦¬μ¦˜κ³Ό μž…λ ₯을 λ‚˜νƒ€λ‚΄λŠ” ν‘œν˜„μ‹ EE둜 κ΅¬μ„±λœλ‹€. 이 ν‘œν˜„μ‹ EEλŠ” μΌμ •ν•œ μž¬μž‘μ„± κ·œμΉ™μ— 따라 λŒ€μ²΄λ  수 μžˆλŠ”λ°,λ¦¬λ•μ…˜μ€ ν‘œν˜„μ‹ EE의 일뢀뢄 PP을 주어진 μž¬μž‘μ„± κ·œμΉ™μ— 따라 λ‹€λ₯Έ ν‘œν˜„μ‹ Pβ€²P'둜 λŒ€μ²΄ν•˜λŠ” 것을 μ˜λ―Έν•œλ‹€. 기호적으둜 ν‘œν˜„ν•˜λ©΄ λ‹€μŒκ³Ό κ°™λ‹€. E[P]β†’E[Pβ€²],E[P] \rightarrow E[P'], 단 Pβ†’Pβ€²P \rightarrow P'은 κ·œμΉ™μ— 따라 λŒ€μ²΄ κ°€λŠ₯ν•œ κ²½μš°μ΄λ‹€. 이 λ¦¬λ•μ…˜ 과정은 결과적으둜 더 이상 μž¬μž‘μ„±μ΄ λΆˆκ°€λŠ₯ν•œ 뢀뢄이 μ—†λŠ” ν‘œν˜„μ‹μ΄ λ‚˜μ˜¬ λ•ŒκΉŒμ§€ λ°˜λ³΅λœλ‹€. μ΄λ ‡κ²Œ 얻어진 μ΅œμ’… ν‘œν˜„μ‹μ„ μ •κ·œν˜•(normal form)이라고 ν•˜λ©°, 주어진 ν•¨μˆ˜ν˜• ν”„λ‘œκ·Έλž¨μ˜ 좜λ ₯값을 λ‚˜νƒ€λ‚Έλ‹€.

μ˜ˆμ‹œ: (7+4)β‹…(8+5β‹…3)β†’11β‹…(8+5β‹…3)β†’11β‹…(8+15)β†’11β‹…23β†’253. \begin{aligned} (7 + 4) \cdot (8 + 5 \cdot 3) &\rightarrow 11 \cdot (8 + 5 \cdot 3)\\ &\rightarrow 11 \cdot (8 + 15)\\ &\rightarrow 11 \cdot 23\\ &\rightarrow 253. \end{aligned}

μœ„μ˜ μ˜ˆμ‹œμ—μ„œ λ¦¬λ•μ…˜ κ·œμΉ™μ€ μˆ«μžλ“€μ— λŒ€ν•œ λ§μ…ˆκ³Ό κ³±μ…‰μ˜ 'ν‘œ(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)'라고 뢈리며, ν•¨μˆ˜ν˜• ν”„λ‘œκ·Έλž˜λ°μ—μ„œ 기호 데이터λ₯Ό μ‘°μž‘ν•˜κΈ° μœ„ν•œ ν•„μˆ˜μ μΈ λ„κ΅¬λ‘œ μ‚¬μš©λœλ‹€.

λ¦¬λ•μ…˜ μ‹œμŠ€ν…œμ€ 일반적으둜 Churchβˆ’RosserChurch-Rosser 속성을 λ§Œμ‘±ν•˜λŠ”λ°, μ΄λŠ” 얻어진 μ •κ·œν˜•μ΄ ν•˜μœ„ μš©μ–΄λ“€μ˜ 계산 μˆœμ„œμ— λ…λ¦½μ μ΄λΌλŠ” 것을 λ‚˜νƒ€λ‚Έλ‹€. μ‹€μ œλ‘œ 첫 번째 μ˜ˆμ‹œλŠ” λ‹€μŒκ³Ό 같이 λ¦¬λ•μ…˜ 될 수 μžˆλ‹€.

(7+4)β‹…(8+5β‹…3)β†’(7+4)β‹…(8+15)β†’11β‹…(8+15)β†’11β‹…23β†’253. \begin{aligned} (7 + 4) \cdot (8 + 5 \cdot 3) &\rightarrow (7 + 4) \cdot (8 + 15)\\ &\rightarrow 11 \cdot (8 + 15)\\ &\rightarrow 11 \cdot 23\\ &\rightarrow 253. \end{aligned}

ν˜Ήμ€ μ—¬λŸ¬ ν‘œν˜„μ‹λ“€μ„ λ™μ‹œμ— ν‰κ°€ν•¨μœΌλ‘œμ¨ 더 λ‹¨μˆœν•˜κ²Œ λ¦¬λ•μ…˜λ  μˆ˜λ„ μžˆλ‹€.

(7+4)β‹…(8+5β‹…3)β†’11β‹…(8+15)β†’11β‹…23β†’253. \begin{aligned} (7 + 4) \cdot (8 + 5 \cdot 3) &\rightarrow 11 \cdot (8 + 15)\\ &\rightarrow 11 \cdot 23\\ &\rightarrow 253. \end{aligned}

πŸ”—Application and abstraction

Ξ»βˆ’\lambda-κ³„μ‚°μ˜ 첫 번째 κΈ°λ³Έ μž‘μ—…μ€ 적용(applicationapplication)이닀. ν‘œν˜„μ‹ Fβ‹…AF \cdot A λ˜λŠ” FAF AλŠ” 데이터 FFλ₯Ό μ•Œκ³ λ¦¬μ¦˜μœΌλ‘œ κ°„μ£Όν•˜μ—¬ 데이터 AAλ₯Ό μž…λ ₯으둜 μ μš©ν•˜λŠ” 것을 λ‚˜νƒ€λ‚Έλ‹€. μ΄λŠ” 두 가지 κ΄€μ μœΌλ‘œ λ³Ό 수 μžˆλŠ”λ°, 계산 κ³Όμ • FAF A λ˜λŠ” 이 κ³Όμ •μ˜ 좜λ ₯으둜 λ³Ό 수 μžˆλ‹€. 첫 번째 관점은 λ³€ν™˜(conversion)λ˜λŠ” 더 λ‚˜μ€ λ¦¬λ•μ…˜(reduction) κ°œλ…μœΌλ‘œ 포착되며, 두 번째 관점은 λͺ¨λΈ(의미둠) κ°œλ…μœΌλ‘œ ν‘œν˜„λœλ‹€. 이 이둠은 νƒ€μž…μ— μ œν•œμ΄ μ—†λ‹€(type-free). 즉, FFκ°€ 자기 μžμ‹ μ—κ²Œ 적용된 FFF F와 같은 ν‘œν˜„μ‹μ„ κ³ λ €ν•  수 μžˆλ‹€. μ΄λŠ” μž¬κ·€λ₯Ό λͺ¨λ°©ν•˜λŠ”데 μœ μš©ν•˜λ‹€.

λ‹€λ₯Έ κΈ°λ³Έ μž‘μ—…μ€ 좔상화(abstractionabstraction)이닀. λ§Œμ•½ M≑M[x]M \equiv M[x]λΌλŠ” ν‘œν˜„μ‹μ΄ xx에 μ˜μ‘΄ν•œλ‹€λ©΄, Ξ»x.M[x]\lambda{x}.M[x]λŠ” ν•¨μˆ˜ x↦M[x]x \mapsto M[x]λ₯Ό λ‚˜νƒ€λ‚Έλ‹€.
적용(applicationapplication)κ³Ό 좔상화(abstractionabstraction)λŠ” λ‹€μŒκ³Ό 같은 직관적인 κ³΅μ‹μ—μ„œ ν•¨κ»˜ μž‘λ™ν•œλ‹€. (Ξ»x.2β‹…x+1)3=2β‹…3+1   (=7).(\lambda{x}.2 \cdot x + 1)3 = 2 \cdot 3 + 1 \space\space\space (= 7). 즉, (Ξ»x.2β‹…x+1)3(\lambda{x}.2 \cdot x + 1)3은 ν•¨μˆ˜ x↦2β‹…x+1x \mapsto 2 \cdot x + 1에 인자 33을 μ μš©ν•˜μ—¬ 2β‹…3+12 \cdot 3 + 1둜 κ³„μ‚°λ˜λ©° 값은 77이 λœλ‹€. 일반적으둜 (Ξ»x.M[x])N=M[N](\lambda{x}.M[x])N = M[N] 식은 λ‹€μŒκ³Ό 같이 쓰이기도 ν•œλ‹€. (Ξ»x.M)N=M[x≔N],(Ξ²)(\lambda{x}.M)N = M[x \coloneqq N], \qquad (\beta) μ—¬κΈ°μ„œ [x:=N][x := N]은 xx에 NN을 λŒ€μž…ν•˜λŠ” 것을 λ‚˜νƒ€λ‚΄λŠ”λ°, λ†€λžκ²Œλ„ (Ξ²)(\beta)κ°€ Ξ»βˆ’\lambda-κ³„μ‚°μ˜ μœ μΌν•œ ν•„μˆ˜μ μΈ κ³΅λ¦¬μ΄μ§€λ§Œ, κ·Έ 결과둜 μ–»μ–΄μ§€λŠ” 이둠은 κ½€ λ³΅μž‘ν•˜λ‹€.

πŸ”—Free and bound variables

좔상화(abstraction)(abstraction)λŠ” λ³€μˆ˜ xxλ₯Ό MM μ•ˆμ—μ„œ "λ¬ΆλŠ”λ‹€(bind)(bind)"κ³  ν‘œν˜„ν•œλ‹€. 예λ₯Ό λ“€μ–΄, Ξ»x.yx\lambda{x}.yxμ—μ„œ xxλŠ” λ¬Άμ—¬μžˆλŠ” λ³€μˆ˜(bound variable)이고 yyλŠ” 자유 λ³€μˆ˜(free variable)라고 ν•œλ‹€. μΉ˜ν™˜ [x:=N][x := N]은 xx의 자유 λ“±μž₯(free occurrences)μ—λ§Œ μ μš©λœλ‹€ yx(Ξ»x.x)[x:=N]≑yN(Ξ»x.x)yx(\lambda{x}.x)[x := N] \equiv yN(\lambda{x}.x)

λ―Έμ λΆ„ν•™μ—μ„œλ„ μœ μ‚¬ν•œ λ³€μˆ˜ 묢음 κ°œλ…μ΄ μžˆλ‹€. ∫abf(x,y)dx\int_{a}^bf(x,y)dxμ—μ„œ λ³€μˆ˜ xxλŠ” λ¬Άμ—¬μžˆκ³  yyλŠ” 자유 λ³€μˆ˜μ΄λ‹€.
λͺ…λ£Œμ„±μ„ μœ„ν•΄, νŠΉμ • ν‘œν˜„μ‹μ— λ“±μž₯ν•˜λŠ” 묢인 λ³€μˆ˜λ“€μ€ 자유 λ³€μˆ˜λ“€κ³Ό λ‹€λ₯΄λ‹€κ³  κ°€μ •ν•œλ‹€. 이것은 묢인 λ³€μˆ˜λ“€μ˜ 이름을 λ³€κ²½ν•¨μœΌλ‘œμ¨ μΆ©μ‘±ν•  수 μžˆλŠ”λ°, 예λ₯Ό λ“€μ–΄, Ξ»x.x\lambda{x}.xλŠ” Ξ»y.y\lambda{y}.y둜 λ°”λ€” 수 μžˆλ‹€. 사싀, μ΄λŸ¬ν•œ ν‘œν˜„μ‹λ“€μ€ λ™μΌν•œ λ°©μ‹μœΌλ‘œ μž‘λ™ν•œλ‹€. (Ξ»x.x)a=a=(Ξ»y.y)a(\lambda{x}.x)a = a = (\lambda{y}.y)a 그리고 사싀상 이듀은 같은 μ˜λ„λœ μ•Œκ³ λ¦¬μ¦˜μ„ λ‚˜νƒ€λ‚Έλ‹€. λ”°λΌμ„œ 묢인 λ³€μˆ˜λ“€μ˜ μ΄λ¦„λ§Œ λ‹€λ₯Έ ν‘œν˜„μ‹λ“€μ€ λ™μΌν•œ κ²ƒμœΌλ‘œ κ°„μ£Όλœλ‹€.

πŸ”—Functions of more arguments

μ—¬λŸ¬ 인자λ₯Ό κ°€μ§€λŠ” ν•¨μˆ˜λŠ” μ μš©μ„ λ°˜λ³΅ν•¨μœΌλ‘œμ¨ 얻을 수 μžˆλ‹€. 이 μ•„μ΄λ””μ–΄λŠ” SchΓΆnfinkel(1924)에 μ˜ν•΄ μ œμ•ˆλ˜μ—ˆμ§€λ§Œ, H.B. Curryκ°€ λ…λ¦½μ μœΌλ‘œ λ„μž…ν•œ ν›„ curryingcurryingμ΄λΌλŠ” μ΄λ¦„μœΌλ‘œ 널리 μ•Œλ €μ‘Œλ‹€. μ§κ΄€μ μœΌλ‘œ f(x,y)f(x, y)κ°€ 두 개의 μΈμžμ— μ˜μ‘΄ν•œλ‹€λ©΄, λ‹€μŒκ³Ό 같이 μ •μ˜ν•  수 μžˆλ‹€. Fx=Ξ»y.f(x,y),F_x = \lambda{y}.f(x,y), F=Ξ»x.Fx.F = \lambda{x}.F_x. 그런 λ‹€μŒ, (Fx)y=Fxy=f(x,y).(ρ)(Fx)y = F_xy = f(x, y). \qquad (\rho)

μ΄λ ‡κ²Œ ν•¨μœΌλ‘œμ¨ 두 인자λ₯Ό κ°€μ§€λŠ” ν•¨μˆ˜ f(x,y)f(x, y)λ₯Ό 단일 인자 ν•¨μˆ˜ FF둜 λ³€ν™˜ν•  수 μžˆλ‹€. μ΄λŸ¬ν•œ 기법은 curryingcurrying라고 뢈리며, ν•¨μˆ˜ν˜• ν”„λ‘œκ·Έλž˜λ°μ—μ„œ ν•¨μˆ˜λ“€μ„ 더 μœ μ—°ν•˜κ²Œ μ‘°μž‘ν•˜λŠ” 데에 μ‚¬μš©λœλ‹€.

λ§ˆμ§€λ§‰ 식은 반볡적인 μ μš©μ— λŒ€ν•΄ μ™Όμͺ½μœΌλ‘œ κ²°ν•©(association)(association)ν•˜λŠ” 것이 νŽΈλ¦¬ν•˜λ‹€λŠ” 것을 보여쀀닀. FM1β‹…β‹…β‹…Mn denotes (β‹…β‹…((FM1)M2)β‹…β‹…β‹…Mn).FM_1 Β·Β·Β· M_n \space denotes \space (Β·Β·((FM_1)M_2)Β·Β·Β·M_n). 식 (ρ)(\rho)은 그런 λ‹€μŒ λ‹€μŒκ³Ό 같이 ν‘œν˜„λœλ‹€. Fxy=f(x,y)F{xy} = f(x, y) 이와 λ§ˆμ°¬κ°€μ§€λ‘œ, 반볡적인 μΆ”μƒν™”λŠ” 였λ₯Έμͺ½μœΌλ‘œ κ²°ν•©ν•˜λŠ” 것을 μ‚¬μš©ν•œλ‹€. Ξ»x1β‹…β‹…β‹…xn.f(x1,....,xn) denotes Ξ»x1.(Ξ»x2.(β‹…β‹…β‹…(Ξ»xn.f(x1,....xn))β‹…β‹…)).\lambda{x_1} Β·Β·Β· x_n.f(x_1, ...., x_n) \space denotes \space \lambda{x_1}.(\lambda{x_2}.(Β·Β·Β·(\lambda{x_n}.f(x_1,....x_n))Β·Β·)). 그러면 μœ„μ—μ„œ μ •μ˜ν•œ FF에 λŒ€ν•΄ λ‹€μŒ F=Ξ»xy.f(x,y)F = \lambda{xy}.f(x, y) 그리고 (ρ)(\rho)λŠ” λ‹€μŒκ³Ό 같이 ν‘œν˜„λœλ‹€. (Ξ»xy.f(x,y))xy=f(x,y).(\lambda{xy}.f(x, y))xy = f(x, y). nn개의 μΈμžμ— λŒ€ν•΄ λ‹€μŒκ³Ό 같이 ν‘œν˜„ν•œλ‹€. (Ξ»x1β‹…β‹…β‹…xn.f(x1,β‹…β‹…β‹…,xn))x1β‹…β‹…β‹…xn=f(x1,....,xn)(\lambda{x_1}Β·Β·Β·x_n.f(x_1,Β·Β·Β·,x_n))x_1Β·Β·Β·x_n = f(x_1,....,x_n) nn번 (Ξ²)(\beta)λ₯Ό μ‚¬μš©ν•˜μ—¬ 이 식은 λ‹€μŒκ³Ό 같이 벑터 ν‘œκΈ°λ‘œ ν‘œν˜„λœλ‹€. (Ξ»xβƒ—.f[xβƒ—])xβƒ—=f[xβƒ—];(\lambda{\vec{x}}.f[{\vec{x}}])\vec{x} = f[\vec{x}]; 보닀 일반적으둜 λ‹€μŒκ³Ό 같이 ν‘œν˜„ν•œλ‹€. (Ξ»xβƒ—.f[xβƒ—])Nβƒ—=f[Nβƒ—];(\lambda{\vec{x}}.f[{\vec{x}}])\vec{N} = f[\vec{N}];