Unification of Deterministic Higher-Order Patterns (Full Version)

Sintesi Tecnica: Unificazione di Pattern di Ordine Superiore Deterministici

Enunciazione del Problema
Questo articolo affronta il problema dell'unificazione per una specifica classe di $\lambda$-termini tipati semplicemente noti come Pattern di Ordine Superiore Deterministici (DHP). Mentre l'unificazione di ordine superiore standard è indecidibile e infinitaria (potenzialmente producendo infiniti unificatori incomparabili), e l'unificazione del primo ordine è decidibile e unitaria, i DHP occupano una posizione intermedia unica. I DHP, introdotti da Yokoyama et al., sono definiti in modo tale che il loro problema di corrispondenza (matching) sia deterministico (esiste al più una sostituzione). Tuttavia, a differenza dei pattern di ordine superiore di Miller o dell'Unificazione Funzioni-Come-Costruttori (FCU) di Libal e Miller, il problema di unificazione per i DHP non è unitario; gli insiemi completi minimi di unificatori (MCSU) possono essere infiniti. La sfida principale è sviluppare una procedura di unificazione corretta e completa per questa classe che gestisca la natura potenzialmente infinitaria dello spazio delle soluzioni, mantenendo al contempo le proprietà strutturali che rendono la corrispondenza deterministica.

Metodologia
Gli autori propongono un sistema di inferenza corretto e completo per il calcolo di insiemi completi di unificatori (CSU) per i DHP. La metodologia si basa sui seguenti fondamenti tecnici:

1. Rappresentazione dei Termini: La procedura opera su $\lambda$-termini tipati semplicemente in forma normale $\beta\eta$-lunga, utilizzando una formulazione libera da $\beta\eta$ per semplificare l'applicazione delle sostituzioni ed evitare la riduzione $\beta$ esplicita durante le dimostrazioni.
2. Definizione dei DHP: Un termine è un DHP se, per ogni sottomomento della forma $x_n.y(t_m)$ dove $y$ è una variabile libera:
   • Ogni argomento $t_i$ contiene almeno una variabile vincolata da $x_n$ (garantendo la corrispondenza deterministica).
   • Gli argomenti sono "espansi" (le loro forme normali $\eta$ non sono astrazioni).
   • Gli argomenti sono distinti secondo la relazione di "sottomomento espanso" (restrizione locale), impedendo che un argomento sia un sottomomento di ordine superiore di un altro.
3. Sistema di Inferenza: La procedura di unificazione è un sistema di inferenza non deterministico che opera su coppie di DHP. Estende il quadro dell'unificazione completa di ordine superiore (Huet) ma introduce ottimizzazioni specifiche per i DHP:
   • Risoluzione Flex-Flex: A differenza dell'unificazione completa di ordine superiore che richiede legami parziali per le coppie flex-flex (coppie in cui entrambe le teste sono variabili libere), il sistema DHP risolve queste in modo "il più generale possibile". Le regole (ff=) e (ff̸=) costruiscono unificatori mantenendo solo argomenti uguali o combinando argomenti senza introdurre variabili libere, rispettivamente.
   • Proiezione e Imitazione: Il sistema utilizza regole di imitazione e proiezione ma le restringe per garantire che i termini risultanti rimangano all'interno della classe DHP. In particolare, le proiezioni nei DHP devono risultare in teste che sono simboli di funzione o variabili vincolate, non variabili libere.
   • Strategia per la Minimalità: Per garantire che l'insieme calcolato di unificatori sia minimo (ortogonale), gli autori definiscono strategie che danno priorità alle regole (rem) e (var) e calcolano nomi di variabili fresche in modo deterministico.

Contributi e Risultati Chiave

• Correttezza e Completezza: L'articolo dimostra che il sistema di inferenza è corretto (le derivazioni di successo producono unificatori validi) e completo (per ogni unificatore $\delta$, esiste una derivazione che produce un unificatore $\theta$ tale che $\theta$ è più generale di $\delta$).
• Minimalità: Gli autori dimostrano che, sotto strategie specifiche (localmente ottimali e deterministiche per le variabili fresche), il sistema di inferenza produce un Insieme Completo Minimo di Unificatori (MCSU). Questo è significativo perché, nell'unificazione di ordine superiore generale, gli insiemi minimi non sono garantiti come ortogonali o finiti.
• Spazi di Soluzione Infiniti: L'articolo fornisce esempi (ad esempio, Esempio 10 e 13) che mostrano come gli MCSU per i DHP possano essere infiniti. Di conseguenza, il sistema di inferenza non è garantito di terminare, e la decidibilità del problema di unificazione DHP rimane una questione aperta.
• Generalizzazione della FCU: Il metodo generalizza la FCU di Libal e Miller rimuovendo la "restrizione globale" (che impedisce a un argomento variabile libera di essere un sottomomento di qualsiasi argomento variabile nell'intero problema). Rimuovendo questa, il sistema gestisce un insieme strettamente più ampio di termini ma perde la proprietà unitaria della FCU.

Significato e Affermazioni
Gli autori collocano questo lavoro come un'indagine necessaria su una classe di termini in cui la corrispondenza rimane deterministica, ma l'unificazione perde la proprietà unitaria, saltando immediatamente a problemi infinitari. Il significato risiede in:

1. Sottoprogrammi Pratici: I DHP sono definiti come una classe di termini piuttosto che una restrizione dipendente dal problema (come la restrizione globale della FCU). Questo rende i DHP più facili da utilizzare come sottoprogrammi nella dimostrazione automatica di teoremi o nella programmazione logica, poiché non è necessario verificare vincoli globali per determinare se un termine è nel campo di applicazione.
2. Insight Teorico: Il lavoro chiarisce il confine tra corrispondenza deterministica e unificazione unitaria, mostrando che la transizione dall'unificazione unitaria a quella infinitaria può avvenire senza passare attraverso una fase finita.
3. Simulazione della FCU: Gli autori affermano che il loro approccio può simulare la FCU; se un problema FCU ha un unificatore più generale, il sistema di inferenza lo troverà tramite una derivazione finita e deterministica.

L'articolo conclude notando che, sebbene il sistema di inferenza sia a ramificazione finita, la sua non terminazione impedisce una prova di decidibilità. Il lavoro futuro richiederebbe rappresentazioni ingegnose di insiemi infiniti di unificatori (ad esempio, utilizzando grammatiche regolari) per gestire efficacemente gli scenari di ramificazione infinita.