1. Evaluation이란?

: 수학에서, 올바른 답을 얻기 위해 식(Expression)을 평가하는 방법은 중요한 이슈이다. λ Calculus에서도 마찬가지다.

2. 원칙과 전략

2-1. Evaluation Principle

: 식을 평가하기 위한 2가지 기본적인 원칙이 있는데, 각각 Eager Evaluation과 Lazy Evaluation이다.

Eager Evaluation

: 언제나 인자를 Evaluation하고, 함수를 인스턴스화(Instantiate) 한다.

Lazy Evaluation

: 인자가 필요한 시점에 Evaluation한다.

2-2. Evaluation Strategy

: 위의 기본적인 원칙에서 2개의 주요한 평가 전략(Evaluation Strategy)이 탄생하는데, 각각 Normal Order와 Applicative Order이다.

Normal Order(call by name으로도 알려져 있음)

: 언제나 맨 왼쪽의 것들부터 줄여나간다. 그리고 파라메터는 함수로 전달되기 전까지 평가하지 않는다.

Applicative Order(strict evaluation 또는 call by value로도 알려져 있음)

: 전달되었거나 대체된 파라메터를 먼저 평가한다.

 아래의 예제는, 각 Evaluation Strategy를 이해하는데에 도움이 될 것이다.

Example) 다음 식을 Normal Order, Applicative Order를 이용해서 평가(Evaluation)해보자.

(λ a.λ b.a)c((λ d.e)d)

Normal Order

: (λ a.λ b.a)c((λ d.e)d)  ->β  (λ b.a)[a＼c]c((λ d.e)d)  =  λ b.c((λ d.e)d)

->β  (c)[b＼((λ d.e)d)]  =  c

Applicative Order

: (λ a.λ b.a)c((λ d.e)d)  ->β  (λ a.λ b.a)c(e[d＼d])  =  (λ a.λ b.a)c(e)

->β  (λ b.a)[a＼c](e)  =  (λ b.c)(e)  ->β  c[b＼e]  =  c

※ 어떤 평가 전략을 쓰더라도 결과는 항상 같을까? 그렇지 않다. 위의 예와 같이, 다음 식을 평가해보자.

(λ x.a)((λ x.x x)(λ y.y y))

Normal Order

: (λ x.a)((λ x.x x)(λ y.y y))  ->β  a[x＼((λ x.x x)(λ y.y y))]  =  a

Applicative Order

: (λ x.a)((λ x.x x)(λ y.y y))  ->β  (λ x.a)(x x)[x＼(λ y. yy)]  =  (λ x.a)((λ y. yy)(λ y. yy))

->β  (λ x.a)(yy)[y＼(λ y. yy)]  =  (λ x.a)((λ y. yy)(λ y. yy)) - 무한 반복된다.

 각 평가 전략을 도입한 결과가 다르다. 따라서 어떤 평가 전략을 사용하느냐는 꽤 중요하다고 볼 수 있다. Church-Rosser 이론에 의하면, 식을 평가할 때 무한 반복되지 않고 끝날 수 있다면 Normal Order를 해당 식에 적용해도 끝날 수 있다. 그리고 똑같은 식에 두 평가 전략을 적용했을 때 모두 끝날 수 있다면, Alpha-conversion전까지 동일한 결과가 나온다.

3. Referrence

- λ Calculus tutorial

1. Reduction이란?

: λ Calculus에서 식을 줄여서 간단한 형태로 만드는 것. 식을 변형시키는 것.

2. Beta, Alpha Eta Reduction

2-1. Beta Reduction

: 아마, 가장 직관적이지 않을까 싶다. β reduction이란,  함수를 적용한 결과를 계산하는 절차를 말한다. 본질적으로, 직접 대체하는데 다음 식을 보자.

((λ (x).BODY) a)   ->β   BODY[a\x] = BODY                            ※  ->β는 β reduction을 의미한다.

식이 변하는 과정을 단계별로 보면, 

1)  ((λ (x).BODY) a)

: x는 받은 인자이며, BODY에 넘겨진다. 지금 상황은 이 함수에 a를 넘기려는 상황이다.

2) ->β   BODY[a\x] = BODY

: BODY[a\x]는, 'BODY에 있는 모든 x를 a로 대체한다'는 의미다. BODY에 x가 없다면,

아무 변화가 없으므로 그냥 BODY가 된다.

β reduction으로 식을 줄이는 예제들

1) (λ z.f z)b  ->β  (f z)[b\z] = (f b)

2) (λ z.y)c  ->β  y[c\z] = y 

3) (λ y.c)((λ z.f z) b)  ->β  (λ y.c)((f z)[b\z])

= (λ y.c)(f b)

->β  c[(f b)\y]

= c 

2-2. Alpha Reduction

: 식을 많이 줄이진 못한다. Renaming이라고 부르기도 한다. Alpha Reduction을 할때, 주의할 점이 있는데 변수의 Scope를 바꾸면 안된다는 것이다. 다음 식을 보자.

(λ (x) (+ x y))

 위의 식에서, x는 함수의 부분으로 쓰이고 있다. 이걸 'x는 Lambda식의 Scope에 Bound되었다'라고 표현하며 'y는 free'라고 표현한다. (λ (x) (+ x y))를 다음과 같이 적을수도 있다.

(λ (x) (+ x y))  ->α  (λ (z) (+ z y))

Alpha Reduction 전후는 동일하다. 그냥 변수의 이름을 바꿨을 뿐이다. Alpha Reduction을 적용할때... 변수의 Scope를 바꾸지 않도록 주의해야 하는데, 다음 식을 보자.

(λ (x) (+ x y))  ->α  (λ (y) (+ y y))

 y는 처음에 Unbound였으므로, Alpha Reduction후에 y의 의미가 바뀌었다. 이걸 Name Conflict라고 부른다. Alpha Reduction전에는 y의 Scope가 Global이었으나 Alpha Reduction후에 Local로 바뀌었다.

2-3. Eta Reduction

: Abstractions에서 쓸모없는 변수들을 제거하기 위해 쓴다. 다음 식을 보자.

((λ (x).BODY) x)  ->η  BODY

 위의 Function Abstraction에서, 함수가 쓰일때마다 인자는 그저 BODY에 전달될 뿐이다. 따라서 BODY와 동일하다. 이전의 Alpha Reduction과 비슷하게, Eta Reduction도 Name Conflict가 없어야 한다. 그래서 x는 BODY에서 free이면 Eta Reduction을 적용하면 안된다. Name Conflict를 피하기 위해, 먼저 Alpha Reduction을 하는 것도 좋다.

3. Reference

- λ Calculus tutorial

- haskell wiki

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