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

1. Intro

1-1. Introduction

: Lambda Calculus(= λ Calculus)는 가장 작은, 범용 프로그래밍 언어이다(Universal Progamming Language). λ Calculus는 계산가능한 함수(Computable Function)를 정의하기 위한 수학적인 시스템으로, Alonzo Church에 의해 1936년에 탄생했다. 원래의 시스템은, Stephen Kleene와 J. B. Rogger가 Kleene-Rosser 역설을 발견한 다음, 논리적으로 일치하지 않는 것으로 나타났다. 그 후 1936년에 Church가 계산(Computation)과 관련된 부분만 따로 발표했는데, 이것이 오늘 날 Untyped λ Calculus라고 불리고 있다. 1940년에는, 계산적으로는 약하지만 논리적으로는 일관된 Simply Typed λ Calculus를 소개했다. 

 1960년대까지, λ Calculus는 형식주의에 불과했었다. Richard Montague와 다른 언어학자들의 자연어 의미에서의 응용 덕분에, λ Calculus은 언어학과 컴퓨터 과학에서 입지를 굳힐 수 있게 되었었다.

 λ Calculus는 함수형 언어(Functional Language)이며, 다른 함수형 언어처럼 수학적인 함수의 이론에 기반을 둔다.  λ Calculus는 모든 계산을 함수의 관점에서 표현할 수 있다.  λ Calculus가 가진 특성은 AI(Artificial Intelligence), Proof System, Logic Programming 분야에서 사용하기 편하다. 그리고 함수와 데이터를 균등하게 다루며, 표기방법도 간단해서 Side effect도 적다. 그래서,  λ Calculus는 순수 함수형 언어의 모델로 사용된다.

※ 1950년대 개발된 LISP는 함수형 프로그래밍 언어이며 λ Calculus를 코어로 두고 있다. 

1-2. Untyped λ Calculus

: Kleene-Rosser의 역설이 발표된 이후, Church는 아주 코어한 로직만 남기고 다른 로직을 좀 제거했는데, 이것을 Untyped λ Calculus(또는 Pure  λ Calculus)라고 부른다. 오늘날, 우리에게 λ Calculus로 알려져 있는 것이다.

1-3. Typed λ Calculus

: λ 심볼을, 익명 함수 추상화(Anonymous Function Abstraction)를 표시하기 위해 쓰는 타입화된 형식주의. Simply Typed λ Calculus은 Typed λ Calculus의 종류중 하나이며, 오직 하나의 타입 생성자를 갖고 기본 타입과 함수 타입만 갖고 있다.

2. Reference

- Wikipedia Lambda Calculus

- λ Calculus tutorial

- Untyped Lambda Calculus

- A Tutorial Introduction to the Lambda Calculus