어떻게 DIF/2 제약 조건을 포함하는 교환 법칙의 타당성을 검증하는데?

Question

dif/2 제약 조건에는 많은 과장이 있는데, 특히 (\ =)/2 및 (\ ==)/2의 일부 비 선언성에 대한 구조입니다. 이 비 선언성은 종종 비 단조로 특징 지어지며 비 공존 성의 예가 제시됩니다.

하지만 dif/2가 포함 된 테스트 사례가 교환 가능한지 여부를 테스트하는 방법은 무엇입니까?

가 나는 교환 법칙 시험을하고, 나는 모두 이 같은 결과를 제공 변형 것을 조사 할 : 그래서 일반적으로 당신이 할 수있는

?- A, B. 
-- versus -- 
?- B, A. 

을 여기에 내가 무엇을 원하는 메타 설명이다 이 교환 법칙을 확인 귀결 경우 (==)/2 내장 술어, 단순성을 확인합니다. 이 술어는 인스턴스화 된 변수를 따르므로

그러나 제약 조건을 생성하는 사례를 테스트하는 경우 call_with_residue/2 이 충분하지 않으면 제약 조건이 동일해야합니다.

Welcome to SWI-Prolog (Multi-threaded, 64 bits, Version 7.3.23) 
Copyright (c) 1990-2015 University of Amsterdam, VU Amsterdam 

?- dif(f(X,X),f(a(U,g(T)),a(g(Z),U))), X=a(g(Z),U). 
X = a(g(Z), U), 
dif(f(a(g(Z), U), U, Z, U, T), f(a(U, g(T)), g(Z), T, g(Z), Z)). 

?- X=a(g(Z),U), dif(f(X,X),f(a(U,g(T)),a(g(Z),U))). 
X = a(g(Z), U), 
dif(f(U, T), f(g(Z), Z)). 

모든 아이디어를 어떻게 진행 : 다음의 예와 같이 어느 , 까다로운 일이 될 수 있습니까?

면책 조항은 그 함정 :
나는 당신이 사양에 비해 좋고 나쁜 조건을 분리 할 수있는 좋은 시험 방법으로 교환 법칙 테스트를 보증하지 않습니다. 일반적으로 좋은 조건과 나쁜 조건 모두 commutativity에 문제가 없을 수 있습니다.

dif/2 제약 조건의 동일성에 대한 방법을 확인하기위한 수단으로 commutativity testing을 사용하고 있습니다. 이 평등은 검증 포인트로서보다 전통적인 테스트 케이스에서 사용될 수 있습니다.

Answer 1

몇 가지가 있습니다. 이 경우 가장 쉬운 방법은 단순히 수집 된 잔여 제약을 다시 게시하는 것입니다. 이 예에서

, 우리가 얻을 :

 
?- X = a(g(Z), U), 
    dif(f(a(g(Z), U), U, Z, U, T), f(a(U, g(T)), g(Z), T, g(Z), Z)). 
X = a(g(Z), U), 
dif(f(U, T), f(g(Z), Z)). 

목표는 훨씬 간단합니다!

copy_term/3 및 call_residue_vars/2으로 잔여 목표를 수집 할 수 있습니다.