https://jurogrammer.tistory.com/135?category=959000 를 공부하고 정리한 글이다.

Formal definition

lambda expression의 구성요소

1. variables v1, v2...
2. the abstraction symbols λ (lambda) and . (dot);->추상화 심볼인 lambda and .(dot)
3. parentheses() : 소괄호

lambda expression의 집합(Λ)은 귀납적으로 정의됨

1. If x is a variable, then x ∈ Λ. : x가 변수라면 Λ에 속함.
2. If x is a variable and M ∈ Λ, then (λx.M) ∈ Λ. : x가 변수이고, M이 Λ에 속한다면, (λx.M)이 또한 Λ에 속함.
3. If M, N ∈ Λ, then (M N) ∈ Λ. : M과 N이 Λ에 속한다면, (M N)도 Λ에 속함.

-> 결론: 람다의 구성요소들은 람다 수식을 application 해도 람다 expression이라 할 수 있음

Notation

1. Outermost parentheses are dropped: M N instead of (M N): 가장 바깥의 소괄호는 생략한다.
2. Applications are assumed to be left associative: M N P may be written instead of ((M N) P). : application은 좌측부터 연산
3. The body of an abstraction extends as far right as possible: λx.M N means λx.(M N) and not (λx.M) N. : abstraction의 body(λx.M에서 M 해당하는 부분)은 가장 바깥까지 취급 (중요)
4. A sequence of abstractions is contracted: λx.λy.λz.N is abbreviated as λxyz.N : λx.λy.λz.N와 같은 abstraction의 나열은 λxyz.N 으로 축약됨.

Free and bound variables(자유변수와 종속변수)

• λ는 abstraction operator. body에 있는 모든 variable을 bind하다고 말할 수 있음.
• λx.M에서 λx는 binder, λx가 M옆에 붙어 variable x가 bound 됨. 다른 변수는 모두 free variable
  (ex) λy.x x y ->λy의 body는 x x y. 에 의해 y가 bound되므로 y는 bind variable. x는 free variable (종속되지 않음)
• variable은 가장 가까운 abstraction에 의해 bound 됨.
  (ex) λx.y (λx.z x). 맨 우측 x는 두번째 abstraction에 의해 bound
• free variables가 없는 expression은 closed되었다고 표현함.