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) 에서 보듯이 같은 식별자라도 한 식에서 자유로울수도 있고 속박되어 있을 수도 있다.

PreviousThe Rust Programming Language NextSICP

Last updated 5 years ago

Was this helpful?

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) 에서 보듯이 같은 식별자라도 한 식에서 자유로울수도 있고 속박되어 있을 수도 있다.