viewimage.php?id=2ab4c42ef0d0&no=24b0d769e1d32ca73fee87fa11d02831c3cad598d6c02bb0ff75d5f6af262f5aca81f423984168e38a57a7cd931a45b72d125151e1775cd6099478116be2d4dc497a5339e2286b67928b6cf65f8a153793459df2d1bb35d546e6f6

짤은 직관주의 1계 논리인데 알 필요는 없어.
내가 설명하고자 하는 건 기다란 선의 의미야:
선 위에 있는 모든 식들을 유도할 수 있을 때,
선 밑에 있는 식을 유도할 수 있다.
참 간단하지?
선 하나하나는 논리형 프로그래밍에서의 Rule이야.
인터프리터에게 식을 주면
인터프리터는 Rule을 이용하여
주어진 식을 유도할 수 있는지를 알려줘.
이게 논리형 프로그래밍의 전부야.

나만의 언어에서 기다란 선은 "/"로 치환되었어.
즉, Rule의 형태는 a_1, ..., a_n / b의 꼴이고,
여기서 a_1, ..., a_n, b는 Formula야.
Formula가 뭐냐면 식에 대한 자료형으로,
Predicate의 Term과의 결합이야.
이 두 개념이 뭔지는 다음 코드를 보고 나면 말해줄게.
/ Father( "A", "B" ).
/ Father( "B", "C" ).
/ Father( "C", "D" ).
Father( x, y ) / Family( x, y ).
/ Family( x, x ).
Family( x, y ) / Family( y, x ).
Family( x, y ), Family( y, z ) / Family( x, z ).
Predicate Father의 해석은 "왼쪽 Term과 오른쪽 Term의 관계가 부자관계인가?"이고,
Predicate Family의 해석은 "왼쪽 Term과 오른쪽 Term이 같은 가문인가?"이야.
감이 잡히지?

더 자세히 설명할게, 기다려줘.
나만의 언어는 타입이 있는 언어야.
타입은 생성자의 집합에 대응되고,
값은 생성자들의 결합인데 문자열에 대응된다.
자연수를 타입으로 정의해보자.
Nat
{
zero() → "z".
succ(Nat) → "s" 1.
}
0항 생성자 zero()와 1항 생성자 succ()으로
타입 Nat을 정의해봤어.
예를 들어, succ(succ(zero()))는 Nat의 값이며,
문자열 "ssz"에 대응된다.
Term은 값과 변수의 결합이야.
예를 들어 n : Nat에 대하여 succ(n) : Nat은 항이야.
이제 1번째 항과 2번째 항의 합이 3번째 항이 되도록
Predicate Plus를 정의해볼게.
/ Plus( x, zero(), x ).
Plus( x, y, z ) / Plus( x, succ( y ), succ( z ) ).
만약 인터프리터에게 Plus( "sz", "z", "sz" )라고 물으면 yes라 답하고, Plus( "sz", x, "ssz" )라고 물으면 x = "sz"라고 답하고, Plus( "sz", y, "z" )라고 물으면 그런 y는 존재하지 않는다고 답해.

문제는 내가 이것을 효율적으로 구현하는 법을 모른다는 거야. 너희들의 도움이 필요해.

- 희망의 등불