Prolog Language
단조 로움

단조로운 술어에 대한 추론

단조 술어는 선언적 추론을 적용하여 디버깅 할 수 있습니다.

순수 Prolog에서 프로그래밍 실수는 다음 현상 중 하나 또는 모두를 초래할 수 있습니다.

1. 술어는 실패 해야하는 경우에 잘못 성공합니다 .
2. 술어가 성공 해야하는 경우에 잘못 실패합니다 .
3. 술어는 예기치 않게 유한 한 답 세트 만 생성해야하는 위치에서 반복 됩니다.

예를 들어 선언적 추론을 통해 case (2)를 디버깅 할 수있는 방법을 생각해보십시오. 우리는 술어의 절의 목표를 체계적으로 제거 하고 여전히 쿼리 가 실패하는지 확인할 수 있습니다. 단조로운 코드에서 목표를 제거하면 결과 프로그램을 더 일반적으로 만들 수 있습니다. 따라서 우리는 목표 중 어느 것이 예상치 못한 실패로 이어지는지를 봄으로써 오류를 찾아 낼 수 있습니다.

단조로운 술어의 예

단조 술어의 예는 다음과 같습니다.

• 와 통합 (=)/2 또는 unify_with_occurs_check/2
• dif/2 , 용어의 불일치 표현
• 단조로운 실행 모드를 사용하여 (#=)/2 및 (#>)/2 와 같은 CLP (FD) 제약 조건 .

단조로운 목표만을 사용하는 프롤로그 술어 자체가 단조롭다.

단조로운 술어는 선언적 추론을 허용합니다.

1. 쿼리에 제약 조건 (즉, 목표)을 추가하면 솔루션 세트를 줄이거 나 늘릴 수 없습니다.
2. 같은 조건의 목표를 제거에서 가장 솔루션 세트를 줄일 수 없다, 확장 할 수 있습니다.

비 단조 술어

다음은 단조롭지 않은 술어의 예입니다.

• var/1 , integer/1 등과 같은 메타 논리적 인 술어
• (@<)/2 와 (@>=)/2 와 같은 용어 비교 술어
• !/0 , (\+)/1 및 단조 로움을 깰 수있는 다른 구문을 사용하는 술어
• findall/3 과 setof/3 과 같은 모든 솔루션 술어 .

이러한 술어가 사용되면 목표를 추가 하면 더 많은 솔루션이 생길 수 있습니다. 이는 제약 조건 추가가 솔루션을 줄이거 나 확장하지 않을 수 있다는 논리에서 알려진 중요한 선언적 속성에 상반됩니다.

결과적으로 선언적 디버깅 및 기타 추론에 의존하는 다른 속성도 손상됩니다. 예를 들어, 비 단조적인 술어는 1 차 논리에서 알려진 결합의 교환 가능성 의 기본 개념을 깬다. 다음 예는 이것을 설명합니다.

?- var(X), X = a.
X = a.

?- X = a, var(X).
false.

모든-솔루션은 같은 술어 findall/3 도 휴식 단순성 : 추가 조항은 이전에 보유했던 목표의 실패로 이어질 수 있습니다. 이것은 또한 1 차 논리에서 알 수 있듯이 사실을 추가하는 것이 증가 할 수 있고 결과의 집합을 결코 줄일 수 없는 montonicity에 반하는 것입니다.

non-monotonic 구조에 대한 모노톤 대안

다음은 프로그램에 순수하지 않은 단조로운 구문 대신 단조로운 술어를 사용하는 방법의 예입니다.

• dif/2 는 (\=)/2 와 같이 non-monotonic 구조 대신 사용하기위한 것 입니다.
• 산술 제한 조건 (CLP (FD), CLP (Q) 및 기타)은 수정 된 산술 술어 대신 사용하기위한 것 입니다
• !/0 은 거의 항상 단조롭지 않은 프로그램으로 이어지고 완전히 피해야 합니다.
• 이 시점에서 올바른 결정을 내릴 수없는 경우 인스턴스화 오류가 발생할 수 있습니다.

단조와 효율성의 결합

효율성을 위해서 실제 Prolog 프로그램에서 비 단조적인 구조의 사용을 받아 들여야 만한다고 주장하는 경우가 있습니다.

이것에 대한 증거는 없습니다. 최근의 연구에 따르면 Prolog의 순수한 단조로운 하위 집합은 대부분의 실제 프로그램을 표현하기에 충분할뿐만 아니라 실제로는 효율적으로 사용할 수 있습니다. 최근에 발견 if_/3 관점을 권장하는 구조는 if_/3 : 단조 로움과 선택 점의 감소를 결합합니다. dif / 2 색인 생성을 참조하십시오.

예를 들어, 다음 형식의 코드 :

pred(L, Ls) :-
    condition(L),
    then(Ls).
pred(L, Ls) :-
    \+ condition(L),
    else(Ls).

if_/3 을 다음과 같이 쓸 수 있습니다 :

pred(L, Ls) :-
    if_(condition(L),
        then(Ls),
        else(Ls)).

단조와 결정론을 결합 합니다.