Unificazione di ordine superiore

Question

Sto lavorando a un dimostratore di teoremi di ordine superiore, di cui l'unificazione sembra essere il sottoproblema più difficile.

Se l'algoritmo di Huet è ancora considerato all'avanguardia, qualcuno ha dei collegamenti con delle spiegazioni che sono scritte per essere comprese da un programmatore piuttosto che da un matematico?

O anche qualche esempio di dove funziona e il solito algoritmo del primo ordine no?

Answer 1

Stato dell'arte — sì, per quanto ne so tutti gli algoritmi più o meno prendere la stessa forma (seguo teoria della programmazione logica, anche se la mia esperienza è tangenziale) fornito avete bisogno dell'immagine completa di ordine superiore di Huet corrispondenza: i sottoproblemi come la corrispondenza di ordine superiore (unificazione in cui un termine è chiuso) e il calcolo del modello di Dale Miller sono decidibili.

Si noti che l'algoritmo di Huet è la migliore nel senso seguente — è come un algoritmo di semi-decisione, in quanto potrete trovare le unificatori se esistono, ma non è garantito per terminare se non lo fanno. Poiché sappiamo che l'unificazione di ordine superiore (anzi, l'unificazione del secondo ordine) è indecidibile, non si può fare di meglio.

Spiegazioni: I primi quattro capitoli della tesi di dottorato di Conal Elliott, Extensions and Applications of Higher-Order Unification dovrebbero essere conformi alla proposta. Quella parte pesa quasi 80 pagine, con una certa teoria del tipo denso, ma è ben motivata, ed è l'account più leggibile che abbia mai visto.

Esempi: l'algoritmo di Huet visualizzerà le merci per questo esempio: [X (o), Y (succ (0))]; quale di necessità renderà perplesso un algoritmo di unificazione del primo ordine.

Answer 2

Un esempio di unificazione di ordine superiore (corrispondenza del secondo ordine reale) è: f 3 == 3 + 3, dove == è modulo alpha, beta ed eta-conversion (ma non assegna alcun significato a "+"). Esistono quattro soluzioni:

\ x -> x + x 
\ x -> x + 3 
\ x -> 3 + x 
\ x -> 3 + 3 

Al contrario, primo ordine unificazione/compensazione potrebbe dare soluzione.

HOU è molto utile quando viene utilizzato con HOAS (di ordine superiore sintassi astratta), per codificare le lingue con variabili vincolanti, evitando la complessità della cattura variabile ecc

La mia prima esposizione al tema è stato il giornale "Proving e applicando le trasformazioni del programma espresse con i modelli del secondo ordine "di Gerard Huet e Bernard Lang. Come ricordo, questo documento è stato "scritto per essere compreso da un programmatore". E una volta compreso il matching del secondo ordine, HOU non è ancora molto lontano. Un risultato chiave di Huet è che il caso flessibile/flessibile (le variabili come capo di un termine e l'unico caso che non compare in corrispondenza) è sempre risolvibile.

Answer 3

Aggiungerei alla lista di lettura un capitolo nel volume 2 di il Manuale di ragionamento automatico. Questo capitolo è probabilmente più accessibile per i principianti e termina con il calcolo λΠ in cui inizia la carta Conol. Elliott .

un preprint si trova qui:

ordine superiore Unificazione e corrispondenza
Gilles Dowek, 2001
http://www.lsv.fr/~dowek/Publi/unification.ps

Conal Elliott carta è più formale e concerntrated su una variante, e anche introduce un λΠΣ-calcolo alla fine, che ha anche i sum-type oltre ai tipi di prodotto.

Bye

Answer 4

C'è anche 1993 di carta Functional Unification of Higher-Order Patterns (solo 11 pagine, di cui 4 bibliografia e il codice allegato) di Tobias Nipkow. L'abstract:

Lo sviluppo completo di un algoritmo di unificazione per le cosiddette modelli di ordine superiore, una sottoclasse di $ \ lambda $ -Termini, è presentato. Il punto di partenza è una formulazione di unificazione per trasformazione, il risultato un programma funzionale direttamente eseguibile. In una fase finale di sviluppo il risultato è adattato a $ \ lambda $ -terms nella notazione di de Bruijn. Gli algoritmi funzionano per entrambi i termini tipizzati e non tipizzati.