Che tipo possono impedire la sospensione obiettivo in linguaggi logici?

Question

Dalla sezione 3.13.3 del curry tutorial:

---

operazioni che sono chiamati residuate rigida, mentre le operazioni che restringono sono chiamati flessibile. Tutte le operazioni definite sono flessibili che operazioni più primitive, come operazioni aritmetiche, sono rigidi poiché indovinare non è un'opzione ragionevole per loro. Ad esempio, il preludio definisce un'operazione di concatenazione lista come segue:

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

Dal momento che l'operazione “++” è flessibile, si può utilizzare per la ricerca di un elenco soddisfare una particolare proprietà:

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

D'altra parte, le operazioni aritmetiche predefinite come l'aggiunta “+” sono rigidi. Pertanto, una chiamata a “+” con una variabile logica come argomento flounders:

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

---

curry non sembra proteggere contro obiettivi di scrittura che verranno sospesi. Che tipo di sistemi possono rilevare in anticipo se un obiettivo verrà sospeso?

Answer 1

quello che hai descritto suona come controllo modalità, che in genere controlla quali saranno disponibili le uscite per un certo insieme di ingressi. Potresti voler controllare la lingua Mercury, che prende molto sul serio il controllo della modalità.