논리 언어에서 목표 정지를 방지 할 수있는 시스템 유형은 무엇입니까? <a href="http://www-ps.informatik.uni-kiel.de/currywiki/documentation/tutorial" rel="nofollow">curry tutorial</a> 섹션 3.13.3에서

Question

:

---

좁히는 연산이 플렉시블 호출되는 반면, 경질이라고 residuate 작업. 모든 정의 된 연산은 유연하지만 산술 연산과 같은 대부분의 기본 연산은 추측이 합리적인 옵션이 아니므로 엄격합니다.

Prelude> x ++ [3,4] =:= [1,2,3,4]  where x free 
Free variables in goal: x 
Result: success 
Bindings: 
x=[1,2] ? 

: 작업 "++"우리는 특정 속성을 만족하는 목록을 검색하는 데 사용할 수 있습니다, 유연 이후

infixr 5 ++ 
... 
(++)    :: [a] -> [a] -> [a] 
[]  ++ ys = ys 
(x:xs) ++ ys  = x : xs ++ ys 

: 예를 들어, 다음과 같이 전주곡이 목록의 연결 작업을 정의

한편, 덧셈 "+"와 같은 사전 정의 된 산술 연산은 고정적입니다. 따라서, 호출은 "+"논리 변수와 인수는 넙치하기 :

Prelude> x + 2 =:= 4 where x free 
Free variables in goal: x 
*** Goal suspended! 

---

카레가 정지됩니다 쓰기 목표를 방지하기 위해 표시되지 않습니다. 어떤 유형의 시스템이 목표가 일시 중지 될 것인지 미리 탐지 할 수 있습니까?

Answer 1

설명 된 내용은 일반적으로 특정 입력 집합에 사용할 수있는 출력을 확인하는 모드 확인과 비슷합니다. 당신은 모드 검사를 아주 심각하게 받아들이는 언어 인 머큐리를 검사하고 싶어 할 것입니다.