알고 있는지에 대한 정보를 추가하면 어떨까요?

"항을 안다"를 그 항을 논리 변수 없이 βη-동등하게 표현할 수 있다고 정의합시다.

다음 λ-Prolog 코드를 보면요:

?- copy_formula X Y를 응답하는 데 다음 4가지 경우가 있습니다:

1. X를 알고 Y를 아는 경우:

copy_fomula X Y가 참인지 그렇지 않은지는 결정적입니다.

2. X를 알고 Y를 모르는 경우:

Y가 무엇인지 알 수 있습니다.

3. X를 모르고 Y를 아는 경우:

X가 무엇인지 알 수 있습니다.

4. X를 모르고 Y를 모르는 경우:

X도 Y도 알 수 없습니다.

여기서 4번째 경우를 피하기 위해 타입 정보에 알고 있는지에 대한 정보를 추가하고자 하는데,

어떻게 타입시스템을 설계해야될지 모르겠네요.