[PLT/프로그래밍언어론] 11. Functional Programming(2)

 

11. functional(2)

#PLT

λ Calculus

λ-term(term) (λ-Term)

• 다항식 x² - 2x + 5을 고려해 봅시다.
• x = 2일 때 다항식의 값은 얼마일까요?
• 상황을 표현하기 위해 λ-Term을 사용할 수 있습니다.
• 기호 λ는 변수 x를 expression에 바인딩합니다.
• 정의 (Definition)
  • 모든 변수는 λ-term입니다.
  • Application Terms: M과 N이 λ-term이라면, (MN)은 λ-term입니다.
  • Abstraction Terms: M이 λ-term이고, x가 변수라면, (λx[M])은 λ-term입니다.
• Convention: 왼쪽으로 결합
  • M1M2M3...Mn ➞ ((M1M2)M3)...Mn
• 함수형 패러다임에서의 Redex를 기억하세요 - ((fn x => M) arg)

자유 변수와 바운드 변수 (Free and Bound Variables)

---

자유 변수 (Free Variable):

• 특정 함수 정의(λx)에 의해 바인딩되지 않은 변수.
• 예를 들어, x가 함수의 매개변수로 선언되지 않았지만 사용되는 경우, x는 자유 변수이다.

묶인 변수 (Bound Variable):

• 함수 정의(λx)에 의해 바인딩된 변수.
• 예를 들어, λx.x에서 x는 묶인 변수입니다.

---

---

1. 자유 변수 계산 규칙 (FV)

• 변수 x가 단독으로 등장하면, 그 자체로 자유 변수:
  • 𝐹𝑉(𝑥) = {𝑥}
• 두 표현식 𝑀, 𝑁이 결합된 경우, 두 식의 자유 변수의 합집합:
  • 𝐹𝑉(𝑀𝑁) = 𝐹𝑉(𝑀) ∪ 𝐹𝑉(𝑁)
• 함수 정의 λx.M에서 x는 묶인 변수로 간주되므로 자유 변수 집합에서 제외:
  • 𝐹𝑉(λ𝑥[𝑀]) = 𝐹𝑉(𝑀) − {𝑥}

2. 묶인 변수 계산 규칙 (BV)

• 단독 변수 x는 묶인 변수가 아님:
  • 𝐵𝑉(𝑥) = ∅
• 두 표현식 𝑀, 𝑁의 묶인 변수는 두 식의 묶인 변수의 합집합:
  • 𝐵𝑉(𝑀𝑁) = 𝐵𝑉(𝑀) ∪ 𝐵𝑉(𝑁)
• 함수 정의 λx.M에서는 x가 새로 묶인 변수로 추가됨:
  • 𝐵𝑉(λ𝑥[𝑀]) = 𝐵𝑉(𝑀) ∪ {𝑥}

예시

1. 자유 변수와 묶인 변수 구분 예
식: 𝜆𝑥.(𝑥 𝑦)

• 함수 𝜆𝑥는 변수 𝑥를 묶습니다.
  • 𝑥는 묶인 변수입니다.
• 변수 𝑦는 함수의 매개변수로 선언되지 않았으므로 자유 변수입니다.

⠀결론:

• 𝐹𝑉(𝜆𝑥.(𝑥 𝑦)) = {𝑦}
• 𝐵𝑉(𝜆𝑥.(𝑥 𝑦)) = {𝑥}

⠀2. 자유 변수와 묶인 변수 구분 예
식: 𝜆𝑥.((𝜆𝑦.(𝑥 𝑦)) 𝑧)

• 첫 번째 함수 𝜆𝑥는 𝑥를 묶습니다.
• 내부 함수 𝜆𝑦는 𝑦를 묶습니다.
• 𝑧는 어떤 함수에도 묶이지 않으므로 자유 변수입니다.

3.
FV(M) = x + y
FV(N) = x + z 면
FV(MN) = x + y + z

여기서 𝜆𝑥[m] 으로 바운딩하면
BV(𝜆𝑥[m]) = {x}이고,
FV(𝜆𝑥[m]) = {y}이다.

𝜆𝑥[m]을 함수로 표현하자면 다음과 같다.

def f(x):
	x + y

x는 actual parameter의 값을 사용하므로 BV이고, y는 함수 외부의 값을 사용하므로 FV이다.

⠀결론:

• 𝐹𝑉(𝜆𝑥.((𝜆𝑦.(𝑥 𝑦)) 𝑧)) = {𝑧}
• 𝐵𝑉(𝜆𝑥.((𝜆𝑦.(𝑥 𝑦)) 𝑧)) = {𝑥, 𝑦}

• λ는 변수 x를 바인딩하므로 x는 free variable이 아닙니다.
• 프로그래밍 언어에서 free variable는 함수 내에서 사용되지만 함수의 local이 아니거나 전역(non-local)인 변수입니다.

22. 치환 (Substitutions)

M[x := N]을 사용하여 M 내의 자유 변수 x (free occurrence of x)를 N으로 치환함을 나타낼 수 있습니다. M안에 등장하는 자유 변수 x를 N으로 치환한다 ~

람다 대수에서 치환은 다음과 같이 나타냅니다:

• 표기법: 𝑀[𝑥 := 𝑁]
  • ( 𝑀 ): 치환 대상이 되는 람다 표현식.
  • ( 𝑥 ): ( 𝑀 )에서 대체할 자유 변수.
  • ( 𝑁 ): ( 𝑥 )를 대체할 표현식.

치환은 ( 𝑀 ) 안의 자유 변수 ( 𝑥 )를 ( 𝑁 )으로 바꿉니다. 단, ( 𝑥 )가 묶인 변수(bound variable)일 경우는 영향을 받지 않습니다.

람다 대수에서 정의된 치환 규칙은 다음과 같습니다:

1. 변수 치환

( 𝑥[𝑥 := 𝑀] ≡ 𝑀 )

• 자유 변수 ( 𝑥 )는 ( 𝑀 )으로 치환됩니다.

예시: ( 𝑥[𝑥 := 𝑦] )

• 결과: ( 𝑦 )

2. 다른 변수 치환

𝑦[𝑥 := 𝑀] ≡ 𝑦

• ( 𝑦 )가 ( 𝑥 )와 다른 변수라면, 치환은 발생하지 않습니다.

예시: 𝑧[𝑥 := 𝑦]

• ( 𝑧 )는 ( 𝑥 )와 상관없기 때문에 변경되지 않음.
• 결과: ( 𝑧 )

3. 함수 호출 내 치환

• (𝐴𝐵)[𝑥 := 𝑀] ≡ (𝐴[𝑥 := 𝑀])(𝐵[𝑥 := 𝑀])
  • ( 𝐴 )와 ( 𝐵 )는 각각 독립적으로 ( 𝑥 )를 ( 𝑀 )으로 치환합니다.

예시: (𝑥𝑦)[𝑥 := 𝑧]

• ( 𝑥 )는 ( 𝑧 )로 치환되고, ( 𝑦 )는 그대로 유지됩니다.
• 결과: (𝑧𝑦)

4. 람다 추상화 내 치환 (묶인 변수는 영향 없음)

• (λ𝑥.𝐴)[𝑥 := 𝑀] ≡ λ𝑥.𝐴
  • ( 𝑥 )가 ( λ𝑥 )에 의해 이미 묶여 있으므로 치환이 발생하지 않습니다.

예시: (λ𝑥.𝑥𝑦)[𝑥 := 𝑧]

• ( 𝑥 )는 ( λ𝑥 )에 의해 묶여 있으므로 치환되지 않습니다.
• 결과: ( λ𝑥.𝑥𝑦 )

5. 다른 변수의 람다 추상화 내 치환

• (λ𝑦.𝐴)[𝑥 := 𝑀] ≡ λ𝑦.(𝐴[𝑥 := 𝑀]) 단, ( 𝑦 ≠ 𝑥 )
  • ( 𝑦 )가 ( 𝑥 )와 다르면, ( 𝐴 ) 안에서 자유 변수 ( 𝑥 )만 ( 𝑀 )으로 치환합니다.

예시: (λ𝑦.𝑥𝑦)[𝑥 := 𝑧]

• ( 𝑥 )는 자유 변수로 치환되고, ( 𝑦 )는 그대로 유지됩니다.
• 결과: ( λ𝑦.𝑧𝑦 )

3. 중요한 개념: 자유 변수와 묶인 변수

치환의 정확한 동작을 이해하려면 자유 변수(Free Variable)와 묶인 변수(Bound Variable)의 개념을 알아야 합니다:

• 자유 변수: 함수 내부에서 바인딩되지 않은 변수.
  • 치환의 대상.
• 묶인 변수: 함수 내부에서 바인딩된 변수.
  • 치환되지 않음.

4. 치환의 예제

1. 단순 치환

( 𝑥[𝑥 := 𝑦] )

• 자유 변수 ( 𝑥 )를 ( 𝑦 )로 치환.
• 결과: ( 𝑦 )

---

2. 람다 추상화 내 치환

( (λ𝑥.𝑥𝑦)[𝑥 := 𝑧] )

• ( 𝑥 )는 ( λ𝑥 )에 의해 묶여 있으므로 치환되지 않음.
• 결과: ( λ𝑥.𝑥𝑦 )

---

3. 함수 호출 내 치환

( (𝑥𝑦)[𝑥 := 𝑧] )

• ( 𝑥 )는 ( 𝑧 )로 치환되고, ( 𝑦 )는 그대로 유지.
• 결과: ( (𝑧 𝑦) )

---

4. 묶인 변수를 가진 함수 치환

( (λ𝑦.𝑥(λ𝑥.𝑥𝑦))[𝑥 := 𝑧] )

1. ( λ𝑦 ) 내부에서 자유 변수 ( 𝑥 )를 ( 𝑧 )로 치환.
2. 내부의 ( λ𝑥 )에서 ( 𝑥 )는 묶인 변수이므로 치환되지 않음.

결과:
( λ𝑦.𝑧(λ𝑥.𝑥𝑦) )

모든 항 A, B, M 및 모든 변수 x와 y에 대해, 다음이 성립한다.

23. 표기법 (Notations)

• MN: 함수 M을 argument N에 application 한 것.
• PQR: (PQ)R, 왼쪽으로 결합하는 관습.
• (λx[M]): x를 본문 항 M에 바인딩하는 λ-term.
  • λx[M], λx.M, λxM도 사용 가능.
• M[x := A]: M 내부의 모든 자유 변수 x를 λ-term A로 치환하여 얻은 λ-term.
  • [A/x]M, M[x/A], {A/x}M, 등. 같은 의미이다.
• M≡N: λ-term M과 N이 동일함(구문적 동일성). M과 N은 동일한 길이와 동일한 시퀀스의 대응하는 기호를 가집니다.

ex)

24. Reduction (Reductions)

• α-Reduction: Renaming of a variable
• β-Reduction: Subsitution 적용.
• 𝛿-Reduction: primitive function 적용.
• 𝜂-Reduction: Simplification.
  • 에타

25. 𝛿 - Reduction (𝛿 - conversion)

• 또는 𝛿 - Reduction, 𝛿 - rule은 primitive function을 적용하는 것입니다.
• Constant function는 이미 알고 있는 기본적인 수학 규칙으로, λ-calculus를 augment(첨가)합니다.

델타9로 바로 써도 된다.

26. β-Reduction (β-reduction)

• β-Reduction은 또한 β-Conversion, β- rule이라고도 합니다.
• 기본적으로 바운드 변수를 λ로 치환하는 것입니다.

27. α-Reduction (α-conversion)

• 기본적으로 α-Reduction(또는 α- rule)은 변수의 이름을 바꾸는 것입니다.
• 이는 variable capture를 avoid하기 위해 사용할 수 있습니다 - different variables with the same symbol

x가 bound variable로 두 번 등장했다. 첫 번째 베타 리덕션에서 x가 사라져버린다 문제가 발생함.
알파 conversion을 쓰면 안쪽 x를 y로 바꿔줌.

28. 𝜂-Reduction (𝜂-reduction)

• 𝜂-rule 또는 𝜂-Reduction은 항(term)을 simplification하는 것입니다.
• term이 λx[Mx] 형태이면, x가 M에서 자유 변수가 아닌 경우 이를 M으로 단순화할 수 있습니다.
  • x가 M안에서 자유 변수로 나타나면 M이 x값을 의존하기 때문에 M으로 단순화할 수 없다.

여기서 보면 M = λy.y+1이고, x가 M안에 자유 변수로 존재하지 않는다. 그래서 λx.(λy.y+1)x를 λy.y+1로 단순화 할 수 있더라 ~

보통 에타 리덕션을 쓰는 얘들을 보면 이렇게 값을 전달하는 역할을 하는 경우가 많다.
η-Reduction의 목적을 정리해보자면

1. 표현 단순화:
   • 함수의 입력이 단순히 전달되기만 하는 경우, 해당 입력을 제거해 코드(람다 식)를 단순화할 수 있습니다.
2. 동일한 의미 유지:
   • λx[mx]와 M은 동일하게 동작하므로, η-Reduction은 식의 동작에 영향을 주지 않습니다.
3. 최적화:
   • η-Reduction은 함수 호출 시 불필요한 계산을 제거하여 최적화를 가능하게 합니다.

29. 𝛽 - Normal Form

• λ-term M의 𝛽 - redex는 (λx[P])Q 형태의 M의 하위 항입니다.
  • 𝛽-redex는 β-reduction의 후보입니다.
• term이 β-normal from에 있으면, 더 이상 β-redex가 없습니다.
  • 이는 항에 더 이상의 Reduction이 불가능함을 의미합니다.

30. Reducibility

• λ-term A와 B에 대해, A가 B로 β-Reduction된다면 (A →_βB), 이는 A ≡ B이거나 A에서 B로의 유한한 β-Reduction 시퀀스가 존재함을 의미합니다.
• N이 β-정규 형식이고 M →β N인 항 N이 존재하면 term M은 β-normal form을 가진다(has a β-normal form)
  • 이는 M을 β-Reduction하여 더 이상 Reduction 할 수 없는 β-normal form으로 만들 수 있음을 의미합니다.

31. 처치-로저 정리 (Church-Rosser Theorem)

• 만약 P →𝛽 Q 그리고 P →𝛽 R이라면, Q →𝛽 S 그리고 R →𝛽 S인 항 S가 존재합니다.
• 이는 동치성 정리 (Confluence Theorem) 또는 다이아몬드 속성 (Diamond Property)라고도 불립니다.
• 이는 β-normal form의 유일성을 간단히 나타냅니다.
• S가 존재하더라도, 항상 β-Reduction을 통해 S를 얻을 수 있다는 보장은 없습니다.
  • evaluation 중 diiversions(분기)가 발생할 수 있음을 보았습니다.

𝛽*는 0개 이상의 β-Reduction을 의미합니다.

32. Reduction 전략 (Reduction Strategy)

• Reduction 전략은 Reduction할 redex를 선택하는 전략을 나타냅니다.
• β-Reduction 전략이 정규화 (Normalizing) 되려면, Normal form N을 가지는 모든 λ-term M에 대해 이 전략을 사용하면 M을 N으로 Reduction할 수 있어야 합니다.
• Rightmost Strategy: 항상 가장 오른쪽의(rightmost) β-redex를 선택하며, 정규화되지 않습니다.
• Leftmost Strategy: 항상 가장 왼쪽의(leftmost) β-redex를 선택하며, 정규화됩니다.

33. 표준화 정리 (Standardization Theorem)

• λ-term M이 normal form N을 가지면, M을 N으로 Reduction하기 위해 가장 왼쪽(leftmost)의 outermost redex를 Reduction할 수 있습니다.
• Normal-order Evaluation: redex R이 argument A보다 먼저 평가됩니다.
  • argumentA 자체가 redex일 수 있으며, 이는 outermost redex R에 포함됩니다.

1. outermost redex
2. leftmost redex (λy.gey)t 먼저
3. get (λz.in)n 적용

재귀 함수 (Recursive Function)

• 익명 함수 (Anonymous Function): λ-calculus에서 함수는 이름이 없습니다.
• 이름이 있는 함수 (Function with name):
  

  f(x) = 2x + 1
  

• λ-calculus:
  

  λx.2x+1
  

• 함수에 이름이 없다면, 재귀적으로 함수를 호출할 수 있을까요?

예제: 팩토리얼 (Example: Factorial)

• 팩토리얼 함수 정의:

fact(n) = n * fact(n-1), if n >= 1
fact(0) = 1

• λ-calculus에서:

• 여기서 fact는 자유 변수로, 현재는 알 수 없는 상태입니다. 조건 표현식(if, then, else)이 추가된 λ-calculus입니다.
• 여기서 자유 변수 fact를 바인딩하고 λ-term을 만들기 위해 무언가가 필요합니다.

36. Y-조합자 (Y-combinator)

• 알 수 없는 함수 fact를 위한 변수 f를 사용해 봅시다.
  

  F = λf.λn.if n = 0 then 1 else n*f(n - 1)
  

• 이제 재귀 호출을 형성하기 위해 g라는 항을 찾아야 합니다, 즉 g ->b F(g)이어야 합니다.
• 이제 Y를 고려해 봅시다, YM = M(YM)을 만족합니다
  • YM : Y가 term M에 적용된다면 M(YM)이어야 한다. 즉, 다시 YM이 적용된다.
  
  

  Y = λf[(λx[f(x x)]) (λx[f(x x)])]
  

  보면 x와 f가 모두 bounding variable이다.
• Y는 Curry's paradoxical combinator, 간단히 Y-combinator, or a fixpoint operator라고 불립니다.

37. Y-조합자 (Y-combinator)

38. 팩토리얼 (Factorial)

• Y-조합자를 사용하여 λ-term으로 된 팩토리얼 함수는 YF입니다.

Y combinator 특징에 따라 YF는 F(YF)가 된다.
YF를 파라미터로 사용하는 것이므로, F = ~~~식에다가 YF를 써주면, 바운드 변수 f 대신 YF가 들어간다.
2 != 0 이므로 else 있는데에 가서 2-1 델타 conversion해주고, 다시 YF 대신 F(YF)를 써준다.
2*(F(YF)1)에서 파라미터가 1이므로 이번에는 1을 써준다. 또 else가 들어가서 델타 변환하고 YF대신 FYF 넣어서 최종적으로는 0=0이되어 2 * 1 * 1 = 2가 된다.