Non ho mai incontrato una cosa del genere, e ho appena avuto un aspetto più dettagliato.
C'è un motivo computazionale del suono per non implementarlo di default - si deve essenzialmente generare tutte le combinazioni dell'input prima della corrispondenza del modello, oppure si deve generare il valore completo del cross-product delle clausole di corrispondenza.
Sospetto che il modo usuale per implementare questo sarebbe semplicemente scrivere entrambi i modelli (nel caso binario), cioè avere schemi per entrambi C or $X e $X or C.
A seconda dell'organizzazione di dati di base (di solito è tuple), questo abbinamento di pattern comporterebbe la riorganizzazione dell'ordine di elementi di tupla, il che sarebbe strano (in particolare in un ambiente fortemente tipizzato!). Se invece sono elenchi, allora ti trovi su un terreno ancora più oscuro.
Per inciso, ho il sospetto che l'operazione che si desidera fondamentalmente è modelli di unione disgiunta su insiemi, ad esempio:
foo (Or ({C} disjointUnion {X})) = ...
L'unico ambiente di programmazione che ho visto che si occupa di set in ogni dettaglio sarebbe Isabelle/HOL e non sono ancora sicuro che sia possibile costruire le corrispondenze di pattern su di esse.
EDIT: Sembra che la funzionalità di Isabelle function (piuttosto che fun) vi permetterà di definire modelli non-costruttore complessi, salvo poi devi dimostrare che essi siano utilizzati in modo coerente, e non è possibile utilizzare più il generatore di codice.
EDIT 2: Il modo in cui ho implementato una funzionalità simile nel corso n operatori commutativi, associativi e transitivo è stata questa:
mie condizioni erano di forma A | B | C | D, mentre le query erano di forma B | C | $X, dove $X è stato permesso di abbinare zero o più cose. Ho pre-ordinato questi usando l'ordinamento lessografico, in modo che le variabili si siano sempre verificate nell'ultima posizione.
Per prima cosa, costruisci tutte le corrispondenze a coppie, ignorando le variabili per ora e registrando quelle che corrispondono in base alle tue regole.
{ (B,B), (C,C) }
Se trattate questo come un grafo bipartito, allora si sono essenzialmente facendo un problema perfect marriage. Esistono algoritmi veloci per trovarli.
Supponendo che si trova uno, poi cogliendo tutto ciò che non appare sul lato sinistro della vostra relazione (in questo esempio, A e D), e li roba nella variabile $X, e il tuo partner è completare. Ovviamente si può fallire in qualsiasi momento, ma questo avverrà per lo più se non c'è alcuna variabile libera sul RHS, o se esiste un costruttore sul LHS che non corrisponde a nulla (impedendoti di trovare una corrispondenza perfetta).
Scusate se questo è un po 'confuso. È passato un po 'di tempo da quando ho scritto questo codice, ma spero che questo ti aiuti, anche un po'!
Per la cronaca, questo potrebbe essere non essere un buon approccio in tutti i casi. Avevo delle nozioni molto complesse di "match" su sottotermine (cioè, non un'eguaglianza semplice), e quindi set di costruzione o qualsiasi cosa non avrebbero funzionato. Forse funzionerà comunque nel tuo caso e puoi calcolare direttamente i sindacati disgiunti.
non sono sicuro sono d'accordo con la vostra fusione di Prolog pattern matching vs. ML pattern matching. La corrispondenza del modello ML è puramente sintattica, e in Prolog non credo che sia così. – Gian
Non sto dicendo che sono la stessa cosa, solo che hanno in comune il confronto degli elementi in ordine stretto. – rwallace
Ritengo che un software di dimostrazione teorico dedicato come Otter lo faccia già posizionando le formule logiche in una forma normale e trattando le clausole come strutture dati impostate, il che costa O (n log n) tempo sia per la creazione che per la verifica. In realtà, presumo che abbiano ottimizzazioni preprogrammate per le operazioni per proprietà come associatività e commutatività. –