Ho una domanda interessante, ma non sono sicuro esattamente come frase che ...Come trovare l'ordine di elaborazione ottimale?
consideri il lambda calcolo. Per una determinata espressione lambda, ci sono diversi possibili ordini di riduzione. Ma alcuni di questi non terminano, mentre altri lo fanno.
Nel lambda calcolo, risulta che v'è un particolare ordine di riduzione che è garantita per terminare sempre con una soluzione irriducibile se esiste effettivamente. Si chiama Normal Order.
Ho scritto un semplice risolutore logico. Ma il problema è che l'ordine in cui elabora i vincoli sembra avere un enorme effetto sul fatto che trovi qualche soluzione o meno. Fondamentalmente, mi chiedo se esiste qualcosa come un normale ordine per il mio linguaggio di programmazione logica. (O wether è impossibile per una semplice macchina per risolvere questo problema in modo deterministico.)
Quindi questo è quello che sto cercando. Presumibilmente, la risposta dipende in modo critico da cosa sia esattamente il "semplice risolutore logico". Quindi cercherò di brevemente descriverlo.
Il mio programma è strettamente basata sul sistema di combinatori nel capitolo 9 di Il divertimento di programmazione (Jeremy Gibbons & Oege de Moor). La lingua ha la seguente struttura:
L'input della risolutore è un singolo predicato. I predicati possono coinvolgere variabili. L'uscita dal risolutore è zero o più soluzioni. Una soluzione è un insieme di assegnazioni di variabili che rendono il predicato diventato vero.
Le variabili contengono espressioni. Un'espressione è un numero intero, un nome di variabile o una tupla di sottoespressioni.
C'è un predicato di uguaglianza, che confronta le espressioni (non predicati) per l'uguaglianza. È soddisfatto se la sostituzione di ogni variabile (vincolata) con il suo valore rende identiche le due espressioni. (In particolare, ogni variabile è uguale a se stessa, vincolata o meno). Questo predicato viene risolto utilizzando l'unificazione.
Ci sono anche operatori per AND e OR, che opera in modo ovvio. Non c'è un operatore NOT.
C'è un operatore "esiste", che crea essenzialmente variabili locali.
La funzione per definire i predicati denominati consente il ciclo ricorsivo.
Una delle "cose interessanti" sulla programmazione logica è che una volta che si scrive un predicato di nome, funziona in genere fowards e indietro (e talvolta anche lateralmente). Esempio canonico: un predicato per concatinare due liste può anche essere usato per dividere una lista in tutte le possibili coppie.
Ma a volte l'esecuzione di un predicato all'indietro comporta una ricerca infinita, a meno che non si riorganizzi l'ordine dei termini. (Ad esempio, scambiare l'LHS e l'RHS di un AND o di un OR). Mi chiedo se ci sia un modo automatico per rilevare l'ordine migliore per eseguire i predicati, per assicurare la pronta interruzione in tutti i casi in cui la soluzione è esatta finito.
Qualche suggerimento?
Probabilmente aiuterà se si posta un paio di esempi di programmi nella tua lingua, e mostrare come le diverse strategie di riduzione portano a risultati diversi. –
@ n.m. Buona idea. Proverò a dare un esempio minimale ... – MathematicalOrchid
Vedi anche [Aritmetica presburger] (http://en.wikipedia.org/wiki/Presburger_arithmetic) nel caso in cui non l'avessi visto prima - la validità è decidibile e consente e, o, non, per sempre e induzione (anche se forse l'induzione non è potente come la ricorsione che descrivi). –