인터프리터는 명제가 참인지 거짓인지 답한다.

변수가 있는 식에 대해서도 답하면 좋겠다.

그러려면 해를 모조리 구하거나 변수를 묶어야 한다.

해를 모조리 구하게 하는 방법은 내 실력 밖이다.

그러므로 변수를 묶어 인터프리터와 대화하게 하자.

어떻게 할까? 변수를 정의할 때, 형식문법과 비슷하게,

재귀적으로 변수가 가질 수 있는 값의 집합을 정의하게 하자.

타입 Nat이 "Nat ::= zero( ), succ( Nat )."로 정의되었을 때,

자유 변수 a, b를 다음과 같이 정의하자.

  1. a : Nat. -- 자유 변수 a를 Nat 타입으로 선언함.
  2. b : Nat. -- 자유 변수 b를 Nat 타입으로 선언함.
  3. a ::= zero( ), succ( b ).
  4. b ::= succ( a ).
그러면 a는 임의의 짝수만을 값으로 가질 수 있고,
b는 임의의 홀수만을 값으로 가질 수 있다.

다음과 같은 코드가 있을 때,

"Even( a )?"라고 물으면 "yes"라고 대답하게끔 하고 싶다.

  1. Even( Nat ). -- 첫 번째 항의 타입이 Nat인 1항 술어 Even 선언.
  2. / Even( zero( ) ).
  3. Even( x ) / Even( succ( succ( x ) ) ).
그러려면 귀납법을 어떻게 확장해야 될까?

더 일반적인 상황까지 커버할 수 있어야 한다.