Lambda Calculus

Raul Rojas, "A Tutorial Introduction to the Lambda Calculus", Freie Universität Berlin, 2015.

Definition of λ-calculus

• smallest universal programming language in the world

• 단일한 변환 규칙과 함수 정의로 구성된다.

• 1930년대에 알론조 처치에 의해 "효율적인(effective) 계산의 개념을 형식화하는 방법"으로 만들어짐

• 어떤 계산 가능한 함수든 람다 계산법에 의해 표현&계산 가능하다는 점에서 범용적이다.

• 람다 계산법은 튜링 머신으로도 표현 가능하다. -> 처치-튜링 명제

• 람다 계산법은 기호 변환의 규칙을 강조한다. 구현하는 방법에 대해선 그닥 신경쓰지 않는다. 이런 점에서 람다 계산법은 하드웨어보단 소프트웨어에 관련되어있다.

• 람다 계산법의 핵심은 "식(expression)" 이다.

  • "이름(name)"은 a, b, c 같은 식별자이다.

  • "식"은 "이름"이 되거나 "함수" 가 될 수 있다.

  • "함수(function)"은 그리스 문자 "λ"를 함수의 인자를 표현하기 위해 사용한다.

    • 함수의 "본문(body)"는 인자가 어떻게 재정렬(rearrange) 될지를 정의한다.

  • 예를 들어 항등 함수는 (λx.x) 와 같이 표현된다.

    • λx 는 함수의 인자가 x라는 것을 표현한다. 이 인자는 변경되지 않고 반환된다.

• 함수는 다른 함수에 의해 적용될 수 있다.

  • 예를 들어 함수 B에 적용된 A는 AB로 작성될 것이다. (대문자는 함수를 표현하기 위해 사용된다.)

  • 람다 계산법은 함수에 집중한다.

    • 상수와 진릿값도 기호 변환을 위해 서로 작용할 수 있는(act on one another) 함수로 표현된다.

  • 람다 계산법에는 타입이 없다.

    • 어떤 함수든 서로 작용할 수 있다.

    • 프로그래머는 연산을 합리적으로 유지할 책임이 있다.

• "식"은 다음과 같이 재귀적으로 표현된다.

    <expression> := <name> | <function> | <application> 
    <function> := λ<name>.<expression>
    <application> := <expression> <expression>

• 식은 가독성을 위하여 괄호로 둘러쌓일 수 있다.

  • "E"와 (E)"는 같은 의미이다.

• "점" 은 람다 계산법에서 사용되는 유일한 "키워드"이다.

• 괄호로 둘러쌓인 난잡한 표현을 피하기 위해 왼쪽에서부터 함수를 적용시키는 컨벤션을 도입한다.

  • E1E2E3...En 는 (... (E1E2)E3 ...En)과 동일하다.

• 좋은 함수는 괄호안에 포함되거나 포함되지 않아도 같은 의미를 지닌다.

  • λx.x ≡ (λx.x)

  • A ≡ B에서 동등함을 표현하는 기호로 ≡ 를 사용해 A는 B와 동등하다는 것을 표현한다.

  • 위에서 설명한 대로 λ 오른쪽의 "이름"은 함수 인자의 식별자이다. 점 오른쪽은(여기서는 단일한 x) "본문"이라고 불린다.

• 함수는 식에 적용될 수 있다.

  • (λx.x)y

  • 이 항등 함수는 변수 y에 적용된다.

  • 괄호는 애매모호함을 피하는데 도움을 준다.

  • 함수 적용은 함수 "본문"에 인수 x를 대입하여 평가된다. (이 경우에는 y를 대입한다.)

    • x에 y를 대입하여 축약하면 아래와 같이 최종 결과로 y가 나온다.

    • (λx.x)y → y

• 표기법 [y/x]를 도입하여 함수 본체속 모든 x를 y로 대체함을 표현한다.

  • (λx.x)y → [y/x]x → y

  • 함수 인자의 이름은 자체로써는 아무런 의미도 가지지 않는다. 그저 placeholder일 뿐이다.

    • (λz.z) ≡ (λy.y) ≡ (λt.t) ≡ (λu.u) 이 모든 함수들은 모두 같다.

    • (λx.x)y 은 (λ∇.∇)y와 같은 의미다.

  • 이런 알파벳 치환은 "α-reduction" 이라고도 불린다.

Free and bound variables

• 우리는 알파벳을 심볼로 사용하기 때문에 동일한 알파벳을 반복해서 사용하는 것에 주의해야 함.

• 람다 계산법에서 모든 이름은 지역에 묶인다.

  • 함수 λx.x의 x는 함수 인자로 나타난 이름이기 때문에 "묶였다" 라고 말한다

  • 인자로 들어오지 않는 이름들은 "자유 변수" 라고 불린다.

• (λx.x)(λy.yx)

  • 첫번째 함수의 x는 λ에 묶인다.

  • 두번째 함수의 y도 λ에 묶인다.

    • 하지만 두번째 함수의 x는 자유 변수다.

  • 두번째 함수의 x는 첫번째 함수의 x와 완전히 별개

  • (λx.x)(λy.yx) -> (λy.yx)x -> (λ. x)

    • 축약해보면 x가 남는걸 볼 수 있음.

• 형식적으로 다음의 케이스에서 <name> 은 식 안에서 자유롭다.

  • <name> 은 <name> 안에서 자유롭다

    • a is free in a

  • <name>은 식별자 <name> != <name1> 라면 λ<name1>.<exp> 안에서 자유롭다. + <exp> 안에서도 자유롭다.

    • y is free in λx.y

  • <name> 은 적어도 한 람다 함수에서 자유로우면 전체 E1E2 안에서도 자유롭다.

    • x is free in (λx.x)x

• 다음의 케이스에서 <name>은 속박된다.

  • <name> is bound in λ <name1 >. <exp> if the identifier <name>=<name1> or if <name> is bound in <exp>.

    • x is bound in (λy.(λx.x)).

  • <name> is bound in E1E2 if <name> is bound in E1 or if it is bound in E2.

    • x is bound in (λx.x)x.

• (λx.xy)(λy.y) 에서 보듯이 같은 식별자라도 한 식에서 자유로울수도 있고 속박되어 있을 수도 있다.