-
[프언] #17. Lambda Calculus2023-2학기/프로그래밍언어 2023. 12. 13. 18:37
프로그래밍 언어를 디자인할 때, 모든 Expression이 꼭 필요한 것은 아닙니다. 무슨 뜻이냐?
위 Expression은 필수적으로 존재할 필요가 없습니다. 왜냐? 아래 Expression으로 대체 가능하거든요.
이렇게 다른 문법으로 대체 가능한 Syntax를 Syntactic Sugar라고 합니다. 그리고 이 Sugar를 전부 없애 만들어낸 무가당 프로그래밍 언어를 Lambda Calculus라고 합니다.
Lambda Calculus
Lambda Calculus에는 단 3개의 Expression이 존재합니다. Variable, Abstraction, Application이 그것입니다.
Variable의 경우는 딱히 설명할 게 없겠죠. Abstraction과 Application은 프로시져의 정의와 호출과 비슷하게 작동합니다. 예를 들어, $\lambda x.x+1$ 은 x를 받아 x+1을 출력하는 프로시져로 생각할 수 있고, $\lambda x.x+1 10$을 계산하면 11이 됩니다.
Lambda Calculus의 Semantics를 아래와 같이 표현할 수 있습니다.
$\lambda x$ 내부에 존재하는 변수들을 보고 저희는 Bound, 그 외의 변수들은 Free라고 표현합니다. 예를 들어, $\lambda y.\left( x\; y \right)$에서 y는 Bound Variable, x는 Free Variable입니다. 그리고 Free Variable이 없는 Expression을 Closed Expression이라고 합니다.
계산 순서
이렇게 생긴 Expression을 계산하고 싶다고 합시다. (id는 Identity의 줄임말으로 x를 넣으면 x를 반환하는 Abstraction입니다.) 그럼 어떤 id 먼저 계산해야 할까요? 총 3가지 선택지가 있습니다.
첫 번째 줄처럼 왼쪽에 있는 Abstraction 먼저 계산하는 방식을 Normal Order 혹은 Call-by-Name 이라고 합니다. 이 두 방법의 차이는 각 Argument를 언제 계산하는지에 있습니다. Call-by-Name 방식에서 Argument는 그 Argument가 실제로 필요할 때 계산되며, Normal Order의 경우는 그렇지 않습니다.
반면 각 Argument를 그때그때 계산한 뒤 함수를 적용하는 방식을 Call-by-Value라고 합니다.
Church Numeral & Church Boolean
다음으로는 이제 저희가 이때까지 만든 프로그래밍 언어를 Lambda Calculus로 변환하는 과정에 대해 알아보도록 하겠습니다. 그전에, 편의를 위해 아래와 같은 Church Numeral을 정의하겠습니다.
Church Numeral은 기초적인 함수들을 숫자의 형태로 나타내는 것에 의의가 있습니다. 예를 들어 encode(0)는 2개의 인자를 받아 두번째 인자를 리턴하는 함수입니다. encode(1)은 함수와 변수 하나를 받아 변수에 함수를 적용한 값을 리턴합니다. encode(2)는 함수를 두 번 적용한 값을 리턴하고요.
주어진 f, x, $e_1$, $e_2$에 대해 위가 성립합니다. 함수를 $e_1+e_2$번 적용시키기 위해 먼저 $e_2$번 f를 적용시킨 뒤에 $e_1$번 적용시키는 거죠. 여기에서 착안하여 + 기호를 아래와 같이 정의할 수 있습니다.
비슷한 방법으로, 곱하기 기호는 아래와 같이 정의할 수 있습니다.
아래는 위에 실제 값을 적용시킨 예시입니다.
(밑줄은 encode 함수가 적용되어 있다는 것을 간략하게 나타낸 것입니다. 즉, encode(1) = 1)
Integer와 마찬가지로, Boolean도 Church Boolean이라는 형식으로 나타낼 수 있습니다.
encode(true)는 2개의 인수를 받아 첫번째 인수를 리턴, encode(false)는 2개의 인수를 받아 두 번째 인수를 리턴하는 함수로서 작용합니다. 이를 이용해서 if then else 구문을 아래와 같이 바꿀 수 있습니다.
if문, and, or, not 아래와 같이 변형됩니다.
지금까지 저희 언어를 Lambda Calculus로 변환하는 과정을 정리하면 아래와 같습니다.
Y-combinator
Y-combinator는 재귀 프로시져를 변환하기 위해 만들어진 방법입니다.
예를 들어, 팩토리얼을 계산하는 letrec 함수를 변환하는 과정은 아래와 같습니다.
감사합니다.
이 글은 컴퓨터공학과 학부생이 개인 공부 목적으로 작성한 글이므로, 부정확하거나 틀린 내용이 있을 수 있으니 참고용으로만 봐주시면 좋겠습니다. 레퍼런스 및 글에 대한 기본적인 정보는 이 글을 참고해 주세요.
'2023-2학기 > 프로그래밍언어' 카테고리의 다른 글
[프언] #19. Continuations (0) 2023.12.13 [프언] #18. Algebraic Data Type (0) 2023.12.13 [프언] #16. Procedure Overloading and Parametric Polymorphism (0) 2023.12.13 [프언] #15. Subtype Polymorphism (0) 2023.12.13 [프언] #14. Let-Polymorphic Type System (0) 2023.12.10