항을 안다 모른다의 정보를 타입에 추가하는 거임!!!

여기서 "어떤 항을 안다"의 정의는 "그 항을 logical variable (meta-variable) 없이 βη-동등하게 표현할 수 있다"임.

다음 λ-Prolog 코드를 보셈:

인터프리터가 copy_formula X Y를 증명하고자 할 때, 4가지 경우가 있을 수 있음:

1. X를 알고 Y를 알 때:

copy_formula X Y가 참인지 거짓인지를 쉽게 알 수 있음. 정상적임.

2. X를 알고 Y를 모를 때:

Y를 알 수 있음. 정상적임.

3. X를 모르고 Y를 알 때:

X를 알 수 있음. 정상적임.

4. X를 모르고 Y를 모를 때:

더 이상 알 수 있는 게 없음. 비정상적임.

여기서 4번째 경우를 아예 금지시켜버리는 거임.

그런데 이런 타입 시스템을 어떻게 설계해야할지 감이 안 옴.