저번에 이어서 문제를 내겠습니다. 저번 내용:
http://m.dcinside.com/board/math/693

이제 문제의 프로그래밍 언어에 진짜 함수를 추가하자.
그러나 공리의 꼴로만 함수를 정의할 수 있다.
예를 들어 타입 변수 "t"에 대하여, 코드
"PowerSet( Set t ) : Set (Set t)."
는 멱집합 함수를 선언하고, 코드
"In( z, y ), In( y, PowerSet( x ) ) / In( z, x )."
는 멱집합 함수를 정의한다.
이때 2항 술어 In( t, Set t )에 대하여 식 In( x, s )의 해석은 x가 s의 원소일 때면 그리고 그럴 때에만 참이다.

명제논리에 관한 다음 코드를 보자.

viewimage.php?id=20bcc42e&no=24b0d769e1d32ca73cee86fa11d0283191de25edc716dfae8790c63e5d68dc4703094b82276c59b96fa7233385e2bd154c4889eb652200e4225f2f444ef56af3b9ff443574d55ff8d92aa561d4a40c1f142f0a14fc71b4e0db0ad33425645e

함수 Comma( Set t, t ) : Set t에 대하여,
Comma( h, a )의 해석은 집합 h와 집합 { a }의 합집합이 되도록 코딩되었다.
이때 이렇게 해석할 수 있는 알고리듬이 존재하여,
인터프리터가 코드 "/ Proves( Comma( h, a ), a )."와
멱집합함수를 정의하는 코드에 대하여 잘 작동하게 하는가?

임의의 x, y가 주어졌을 때 식 Proves( x, y )이
식 Proves( Comma( h, a ), a )과 패턴 매칭 되게 하는,
즉 x = Comma( h, a ), y = a를 만족하는,
h와 a 중 지금까지 구하지 않는 해가 존재하는지와 무엇인지를 인터프리터가 유한 단계 안에 알아내게 해야한다.

아니면 멱집합 코드와 명제논리 코드에 대하여 인터프리터가 잘 작동하게 하는 알고리듬을 찾아주세요.

- 희망의 등불