ricerca e query esistenziali senza problemi

Question

Esiste un modo estensibile ed efficiente per scrivere istruzioni esistenziali in Haskell senza implementare un linguaggio di programmazione logica incorporato? Spesso quando sono algoritmi di attuazione, voglio esprimere esistenzialmente quantificati dichiarazioni del primo ordine come

∃x.∃y.x,y ∈ xs ∧ x ≠ y ∧ p x y 

dove ∈ è sovraccarico sulle liste. Se sono di fretta, potrei scrivere codice perspicua che assomiglia

find p []  = False 
find p (x:xs) = any (\y -> x /= y && (p x y || p y x)) xs || find p xs 

o

find p xs = or [ x /= y && (p x y || p y x) | x <- xs, y <- xs] 

Ma questo approccio non generalizzare bene alle domande restituzione di valori o predicati o funzioni di più arietà . Ad esempio, anche una semplice istruzione come

∃x.∃y.x,y,z ∈ xs ∧ x ≠ y ≠ z ∧ f x y z = g x y z 

richiede la scrittura di un'altra procedura di ricerca. E questo significa una quantità considerevole di codice boilerplate. Naturalmente, linguaggi come Curry o Prolog che implementano restringimento o un motore risoluzione consentono al programmatore di scrivere dichiarazioni come:

find(p,xs,z) = x ∈ xs & y ∈ xs & x =/= y & f x y =:= g x y =:= z 

di abusare la notazione considerevolmente, che svolge sia una ricerca e restituisce un valore. Questo problema si verifica spesso quando si implementano algoritmi specificati in modo formale, ed è spesso risolto da combinazioni di funzioni come fmap, foldr e mapAccum, ma la ricorsione per lo più esplicita. Esiste un modo più generale ed efficiente, o solo generale ed espressivo, di scrivere codice come questo in Haskell?

Answer 1

C'è una trasformazione standard che permette di convertire

∃x ∈ xs : P 

a

exists (\x -> P) xs 

Se è necessario produrre un testimone è possibile utilizzare al posto di findexists.

La vera seccatura di fare questo tipo di astrazione in Haskell al contrario di un linguaggio logico è che davvero necessario passare il "universo" set xs come parametro. Credo che questo sia ciò che porta nella "confusione" a cui ti riferisci nel tuo titolo.

Ovviamente è possibile, se preferisci, riempire il set universale (attraverso il quale stai cercando) in una monade. Quindi è possibile definire le proprie versioni di exists o find per lavorare con lo stato monadico. Per renderlo efficiente, puoi provare a Control.Monad.Logic, ma potrebbe comportare la rottura della tua testa contro i documenti di Oleg.

In ogni caso, la codifica classica è quella di sostituire tutti i costrutti vincolanti, compresi i quantificatori esistenziali e universali, con lambda e procedere con le chiamate di funzione appropriate. La mia esperienza è che questa codifica funziona anche per query nidificate complesse con molta struttura, ma che sembra sempre goffo.

Answer 2

Forse non capisco qualcosa, ma cosa c'è di sbagliato nella comprensione delle liste? Il tuo secondo esempio diventa:

[(x,y,z) | x <- xs, y <- xs, z <- xs 
, x /= y && y /= z && x /= z 
, (p1 x y z) == (p2 x y z)] 

Ciò consente di restituire valori; per verificare se la formula è soddisfatta, basta usare null (non valuterà più del necessario a causa della pigrizia).