02. Lambda Calculus의 Syntax

1. Abstraction과 Application, Variable

: λ Calculus의 기본 아이디어는, 단일 식(Εxpression)에서 함수는 정의되고 다른 함수로 적용될 수 있다는 것이다. 각 람다 식은, 람다 식에서 람다 식으로 매핑(Mapping)하는 함수이다. 3가지 기본 타입의 식이 있는데, Function Abstraction과 Function Application, Variable이 그것이며, 각각은 중첩될 수 있다. 다음은 각각에 대한 정의이다.

Variable

: variable x는 람다 식이다.

Abstraction

: x가 variable이고, U가 람다 식이면, abstraction U는 람다 식이다.

Application

: U와 V가 람다 식이면, application U V는 람다 식이다.

2. Context Free Grammar로 나타낸 Syntax

: 위에서 이야기한 정의를 바탕으로, Context Free Grammar를 이용해서 Syntax를 표현해보면 다음과 같다.

<var> ::= a | b | ... | z

<arg> ::= <var>

| (λ <var>.<expr>)

| (<func><arg>)

<func> ::= <var>

| (λ <var>.<expr>)

| <func><arg>

<expr> ::= <var>

| <func><arg>                Application, Function Application

| λ <var>.<expr>            Abstraction, Function Abstraction

※ Application, Abstraction의 차이는?

: Application에서 <func>는 함수, <arg>는 전달할 인자로 생각하면 된다. Abstraction은 익명함수(Anonymous Function)로 생각하면 된다(<var>와 <expr>사이의 .은 함수 몸통과 인자를 분리하기 위한 표시다).

2-1. Application

: Function Application의 형태는 <func><arg>인데 <func>는 함수, <var>는 함수에 전달될 인자로 보면 된다. Application의 간단한 예는 f(x)이다. 괄호나 빈칸은 무시할 수 있으므로, f(x)랑 f x랑 f   x랑 동등하다고 볼 수 있다.

Example) 아래의 식 중에서 올바른 Function Application은?

1) f(x) - 올바른 Function Application

2) f x - 올바른 Function Application

3) x.y - 이것은 Function Abstraction임

4) (f x - 문법상 올바르지 않음

※ application은 left-associative다. x y z는 (x y) z와 동등하나 x (y z)와 동등하진 않다. 따라서 x y z의 의미는 'x는 y에 적용되고, 그 결과가 z에 적용된다'이다. x (y z)의 의미는 'y가 z에 적용된 결과에 x를 적용한다'이다.

2-2. Abstraction

: Function Abstraction의 형태는 λ <var>.<expr>이다. Abstraction은 함수를 위한 간단한 표현이며, 간단한 예는 λ x.y이다

Example) 아래의 식 중에서 올바른 Function Abstraction은?

1) y x - λ랑 마침표(.)이 없음

2) λ g(x) - 문법상 올바르지 않음

3) λ x.y - 올바른 Function Abstraction

4) λ x.(y x) - 올바른 Function Abstraction

※ Abstraction은 가능한한 오른쪽을 향한다. λ x.x y z는 λ x.(x y z)와는 동등하지만, (λ x.x) y z와 동등하지 않다.

3. Reference

- λ Calculus tutorial

- Untyped Lambda Calculus

- A Tutorial Introduction to the Lambda Calculus