문제는 이걸 설명하는 법을 모르겠다는 것입니다.
빨리 슈도코드를 작성해서 형님들의 공격을 받고 싶습니다.
대충 설명하자면,
귀납법을 시도하고 실패하면 패턴 매칭을 시도해보고 또 실패하면 오답으로 둡니다. 목표가 더 이상 없으면 정답으로 둡니다. 귀납법 적용에 성공하면, 변수 = 변수 꼴의 제약이 붙고, 패턴 매칭에 성공하면 변수 → 항 꼴의 제약이 붙습니다. 제약 조건의 트리가 응답입니다.
다음 코드를 봅시다.
1 / Even( 'z' ).
2 Even( x ) / Even( 'ss' x ).
질의 "Even( a )?"에 대한 응답은 다음과 같이 얻어집니다.
처음에는 가정의 집합과 제약 조건의 집합은 공집합이고 목표들의 큐는 질의로 초기화됩니다.
여기서 하나를 꺼내보면:
Even(a)인데,
귀납법을 시도하면 실패하고
패턴매칭을 해보면:
1) #1: a → 'z'.
2) #2: a → 'ss' Nat1.
위와 같은 제약 조건이 각각 추가되면서 패턴매칭에 성공합니다.
이때 Even( a )는 가설이 됩니다.
가지 1)은 더 이상 목표가 없으니 정답이고,
가지 2)의 목표는 Even( Nat1 )입니다.
여기서 Nat1 = a이면 귀납법 적용에 성공하므로,
제약 조건 Nat1 = a를 가진 자식 노드가 생성되고,
그 노드는 정답입니다.
따라서 정답트리는
☞ a → 'z'.
☞ a → 'ss' Nat1.
☞☞ Nat1 = a.
정답트리는 트리구조를 가진 형식문법입니다.

- 희망의 등불