Prolog Language
단조 로움
수색…
단조로운 술어에 대한 추론
단조 술어는 선언적 추론을 적용하여 디버깅 할 수 있습니다.
순수 Prolog에서 프로그래밍 실수는 다음 현상 중 하나 또는 모두를 초래할 수 있습니다.
- 술어는 실패 해야하는 경우에 잘못 성공합니다 .
- 술어가 성공 해야하는 경우에 잘못 실패합니다 .
- 술어는 예기치 않게 유한 한 답 세트 만 생성해야하는 위치에서 반복 됩니다.
예를 들어 선언적 추론을 통해 case (2)를 디버깅 할 수있는 방법을 생각해보십시오. 우리는 술어의 절의 목표를 체계적으로 제거 하고 여전히 쿼리 가 실패하는지 확인할 수 있습니다. 단조로운 코드에서 목표를 제거하면 결과 프로그램을 더 일반적으로 만들 수 있습니다. 따라서 우리는 목표 중 어느 것이 예상치 못한 실패로 이어지는지를 봄으로써 오류를 찾아 낼 수 있습니다.
단조로운 술어의 예
단조 술어의 예는 다음과 같습니다.
- 와 통합
(=)/2
또는unify_with_occurs_check/2
-
dif/2
, 용어의 불일치 표현 - 단조로운 실행 모드를 사용하여
(#=)/2
및(#>)/2
와 같은 CLP (FD) 제약 조건 .
단조로운 목표만을 사용하는 프롤로그 술어 자체가 단조롭다.
단조로운 술어는 선언적 추론을 허용합니다.
- 쿼리에 제약 조건 (즉, 목표)을 추가하면 솔루션 세트를 줄이거 나 늘릴 수 없습니다.
- 같은 조건의 목표를 제거에서 가장 솔루션 세트를 줄일 수 없다, 확장 할 수 있습니다.
비 단조 술어
다음은 단조롭지 않은 술어의 예입니다.
-
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)).
단조와 결정론을 결합 합니다.