Prolog: funzione mancante?

Question

Qualsiasi programmatore con una certa esperienza in Prolog conosce i vantaggi dell'uso notazione unaria per i numeri. Con l'esempio, se rappresentiamo un numero come elenco di 1" ('4' è la lista '[1,1,1,1]' e così via), possiamo definire:

unary_succ(X,[1|X]). 

le seguenti query fa cosa ci si aspetta:

?- X=[1,1],unary_succ(X,Y). 
X = [1, 1], 
Y = [1, 1, 1]. 

?- unary_succ(X,Y),X=[1,1]. 
X = [1, 1], 
Y = [1, 1, 1]. 

?- unary_succ(X,Y),Y=[1,1]. 
X = [1], 
Y = [1, 1]. 

in questo modo, l'affermazione unary_succ (X, Y) "lega" X e Y in un modo che, se dopo il fatto è indicato, una di queste variabili è destinata ad un valore, l'altro

Tuttavia, questo comportamento non è possibile se si utilizza la rappresentazione del numero interno:

?- X=2,succ(X,Y). 
X = 2, 
Y = 3. 

?- succ(X,Y),X=2. 
ERROR: succ/2: Arguments are not sufficiently instantiated 

?- succ(X,Y),Y=2. 
ERROR: succ/2: Arguments are not sufficiently instantiated 

A mio parere, sarà molto utile che dichiarazioni precedenti e simili facciano ciò che ci si aspetta. Cioè, abbiamo bisogno di collegare due variabili in un modo che, quando una di esse è legata a un valore, l'altra segue la regola precedentemente stabilita.

Le mie domande sono:

a) un modo semplice per farlo in Prolog.

b) se non possibile, qualsiasi altro linguaggio di programmazione che supporta questa funzione?

Qualsiasi commento è benvenuto.

Grazie a tutti.

* addendum I *

altro esempio è:

user_id(john,1234). 
user_id(tom,5678). 

e query:

X=john,user_id(X,Y). 
user_id(X,Y),X=john 

che attualmente vengono risolti mediante backtracking.

Answer 1

Questo argomento è noto come coroutining e deve essere risolto in modo abbastanza generale - afaik - richiede l'estensione al modello di calcolo Prolog di base. Fortunatamente, la maggior parte sono Prologs tale estensione ... Quindi, proviamo in SWISH per costruire il proprio interno 'reattivo':

my_succ(X, Y) :- when((nonvar(X);nonvar(Y)), succ(X, Y)). 

modificare non completamente sul punto, ma Jan postato su SWI-Prolog mailing list una semplice esempio di applicazione coroutining:

?- freeze(X, writeln(X)), findall(X, between(1,3,X), Xs). 
1 
2 
3 
Xs = [1, 2, 3], 
freeze(X, writeln(X)). 

Answer 2

Il problema che si descrive esiste finché le risposte di un sistema Prolog sono limitate a (sintattiche) sostituzioni risposta. Nel tuo esempio, l'obiettivo succ(X, Y) richiederebbe infinitamente molte risposte per descrivere l'intero insieme di soluzioni. Per questo motivo, viene emesso invece un instantiation_error.

Per risolvere questo problema, è necessario estendere le risposte. Quindi le risposte non includono solo sostituzioni di risposte, ma un modo più elaborato per descrivere alcuni set.

library(clpfd) vincoli di offerta su Z (e domini più prominenti).

?- use_module(library(clpfd)). 
?- Y #= X+1. 
X+1#=Y. 

Nota che tali risolutori non sono molto forti per il caso generale:

?- Y #= X+1, X #= Y+1. 
Y+1#=X, 
X+1#=Y. 

che ci si aspetta il sistema a fallire, ma produce una risposta che sostanzialmente ribadito la query. Almeno la risposta non è errata, perché afferma semplicemente: sì, c'è una soluzione fornita questa relazione vale (che non è simile alla stampa fine nei contratti di assicurazione o certificati di garanzia).

when/2 è anche conosciuto come coroutining ed è in molti casi più deboli di quello che si ottiene con clpfd. Ma in alcuni casi è più forte per alcune implementazioni di clpfd. Considerare dif/2 che può essere espressa come when(?=(X,Y), X \== Y) e

| ?- dif(X, Y), X = Y. 
no 

... mentre (in SICStus)

| ?- X #\= Y, X #= Y. 
Y #= X, 
Y #\= X, 
Y in inf..sup, 
X in inf..sup ? ; 
no 

library(clpq) offre un risolutore che è più forte in molte situazioni ma manca vincoli intero specifici come mod/2 . In molte situazioni è ancora interessante da usare, come in SICStus:

| ?- use_module(library(clpq)). 
yes 
| ?- {Y=X+1}. 
{X = -1+Y} ? 
yes 
| ?- {Y=X+1}, {X=Y+1}. 
no