단순화된 λ-계산

람다 대수는 함수형 언어의 이론적 핵심으로, λ-식을 계산(평가)하는 것을 바탕으로 한다.

λ-식은 다음 세 형태 중 하나이다.

1. 하나의 상수. 예를 들어 t.
2. 함수 정의 Lv.E. 여기서 글자 L은 λ를 나타내고, v는 몸체 E 안에 나타날 수 있는 변수(예: x)이며, E는 다시 하나의 λ-식이다.
3. 함수를 인수에 적용한 적용 (f)x. 함수 f와 인수 x는 모두 λ-식이다.

식 E 안에서 변수 v가 나타난 위치가 E의 어떤 부분식 Lv.…의 몸체 안에 있으면 그 위치는 묶임(bound) 상태이다. 묶이지 않은 위치는 자유(unbound) 상태이다.

λ-식을 계산하면 또 다른 λ-식이 나오며, 규칙은 다음과 같다.

1. 상수는 자기 자신으로 계산된다.
2. 함수 정의는 자기 자신으로 계산된다.
3. 적용 (f)x를 계산할 때는 먼저 함수 f를 계산한다.
   • f가 함수 정의 Lv.E로 계산되면, 인수 x는 계산하지 않는다. 대신 몸체 E 안에서 자유롭게 나타난 모든 v를 x로 치환한 뒤, 그렇게 얻은 몸체를 계산한 결과가 이 적용의 값이 된다.
   • 그렇지 않으면 인수 x를 계산하고, 적용은 (f')x'로 계산된다. 여기서 f', x'는 각각 계산된 함수와 인수이다.

변수와 상수는 한 글자의 소문자(a–z)이다. 어떤 계산은 끝나지 않으므로, 프로그램은 한 식당 최대 1000번의 함수 적용(치환)만 수행해야 한다. 계산 도중 현재 λ-식의 길이는 10000자를 넘지 않는다.

아래는 계산 과정을 보여 주는 예시이다(; 뒤의 글은 주석이다).

1.
  (Lx.x)y                        ; x <- y
  y

2.
  ((Lx.Ly.(x)y)Lz.z)Lq.q         ; x <- Lz.z
  (Ly.(Lz.z)y)Lq.q               ; y <- Lq.q
  (Lz.z)Lq.q                     ; z <- Lq.q
  Lq.q

λ 옆에 묶인 변수의 유효 범위는 그 λ-식의 몸체뿐이며, 같은 이름이 다른 곳에 나타날 수도 있다. 예를 들어:

3.
  ((Lx.x)(Ly.y)Lx.x)x
  ((Ly.y)Lx.x)x
  (Lx.x)x
  x

몸체에는 자유 변수, 즉 상수가 들어 있을 수 있다.

4.
  (((Lx.Ly.q)Lz.t)r)u      ; x <- Lz.t
  ((Ly.q)r)u               ; y <- r
  (q)u

이 계산은 실제 람다 대수보다 단순화되어 있다. 치환 후에는 인수 안에서 원래 자유였던 위치가 묶이게 될 수도 있다. 실제 람다 대수는 변수 이름을 바꿔 이를 방지하지만, 이 문제에서는 그런 처리를 하지 않아도 된다.

5.
  ((Ly.Lx.y)x)w            ; y <- x
  (Lx.x)w
  w

여러 식을 읽어 각각의 계산 결과를 출력하는 프로그램을 작성하라.

입력은 한 줄에 하나씩 주어지는 λ-식들의 집합이다. 마지막 줄은 항상 한 글자 상수 z이다. 모든 식은 올바른 형식이라고 가정해도 된다.

각 입력 식에 대해, 입력과 같은 순서로(마지막 줄 포함) 계산 결과를 한 줄에 하나씩 출력한다. 어떤 식을 계산하는 데 함수 적용이 1000번을 초과해야 한다면, 그 줄에는 unterminated라는 한 단어만 출력한다.