# Lambda Calculus

## Definition of λ-calculus

* smallest universal programming language in the world
* 단일한 변환 규칙과 함수 정의로 구성된다.
* 1930년대에 알론조 처치에 의해 "효율적인(effective) 계산의 개념을 형식화하는 방법"으로 만들어짐
* 어떤 계산 가능한 함수든 람다 계산법에 의해 표현&계산 가능하다는 점에서 범용적이다.
* 람다 계산법은 튜링 머신으로도 표현 가능하다. -> 처치-튜링 명제
* 람다 계산법은 기호 변환의 규칙을 강조한다. 구현하는 방법에 대해선 그닥 신경쓰지 않는다. 이런 점에서 람다 계산법은 하드웨어보단 소프트웨어에 관련되어있다.
* 람다 계산법의 핵심은 "식(expression)" 이다.  &#x20;
  * "이름(name)"은 a, b, c 같은 식별자이다.&#x20;
  * "식"은 "이름"이 되거나 "함수" 가 될 수 있다.
  * "함수(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) "본문"이라고 불린다.&#x20;
* 함수는 식에 적용될 수 있다.&#x20;
  * `(λx.x)y`
  * 이 항등 함수는 변수 y에 적용된다.
  * 괄호는 애매모호함을 피하는데 도움을 준다.
  * 함수 적용은 함수 "본문"에 인수 x를 대입하여 평가된다. (이 경우에는 y를 대입한다.)
    * x에 y를 대입하여 축약하면 아래와 같이 최종 결과로 y가 나온다.
    * `(λx.x)y` → `y`&#x20;
* 표기법 `[y/x]`를 도입하여 함수 본체속 모든 x를 y로 대체함을 표현한다.&#x20;
  * `(λ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 안에서도 자유롭다.&#x20;
    * 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.&#x20;
    * x is bound in (λx.x)x.
* `(λx.xy)(λy.y)` 에서 보듯이 같은 식별자라도 한 식에서 자유로울수도 있고 속박되어 있을 수도 있다.
