Attuazione del calcolo combinatore

Question

Concetto

Io sono l'attuazione di un interprete che consente all'utente di definire arbitraria combinators e li applica ai termini arbitrari. Ad esempio, un utente può definire il Church encoding for pairs inserendo le seguenti definizioni combinator:

pair a b c → c a b 
true a b → a 
first a → a true 

L'utente può quindi introdurre first (pair a b), che si riduce passo-passo secondo le norme precedentemente definite:

first (pair a b) 
→ pair a b true 
→ true a b 
→ a 

Altri combinatori possono essere definiti, come ad esempio quelli utilizzati nel SKI combinator calculus:

S x y z → x z (y z) 
K x y → x 
I x → x 

il Combi identità nator potrebbe anche essere definito in termini dei primi due combinatori per I → S S K K o I → S K (K K) o-. L'universale iota combinator potrebbe allora essere definito da:

ι x → x S K 

Questi esempi si spera di illustrare quello che sto cercando di fare.

Attuazione

sto cercando di implementare questo utilizzando graph reduction e un sistema di graph rewriting. Lasciare tree essere un tipo di dati definito ricorsivamente

tree = leaf | (tree tree) 

Questo è un albero binario, in cui i nodi possono essere sia foglie (nodi terminali) o rami (nodi interni) costituiti da una coppia di sottostrutture. I rami rappresentano l'applicazione di un termine a un altro termine, mentre le foglie rappresentano i combinatori e gli argomenti. Lasciare rule essere un tipo di dati definito da

rule = (tree tree) 

Questo corrisponde ad una regola di riduzione che trasforma struttura a sinistra nella struttura di destra (a → b). L'elenco dei rules può quindi essere definito da

rules = rule | (rule rules) 

Effettivamente, quando si valuta un'espressione come pair a b c → c a b, l'interprete costruisce un albero di forma (((pair a) b) c) corrispondente al lato sinistro, un albero della forma ((c a) b) corrispondente al sul lato destro, costruisce una coppia di entrambi gli alberi corrispondenti a rule (dove a,b,c sono in qualche modo specificati come parametri arbitrari e non necessariamente combinatori o simboli di terminale) e aggiunge questa coppia all'elenco rules. Quando si riduce l'espressione della forma first (pair a b), l'interprete costruisce l'albero corrispondente (first ((pair a) b)) e applica le regole di riduzione come segue:

(first ((pair a) b)) 
→ (((pair a) b) true) 
→ ((true a) b) 
→ a 

Per fare questo, l'interprete deve eseguire pattern matching sull'albero ei suoi sottoalberi, "in movimento attorno "ai combinatori e ai parametri arbitrari per costruire un nuovo albero corrispondente al lato destro della regola.Un esempio di implementazione della struttura ad albero in C è dato da

struct tree_t { 
    bool is_leaf; 
    union { 
     char* symbol; 
     struct { 
      tree_t* left; 
      tree_t* right; 
     }; 
    }; 
}; 

Una funzione pattern matching potrebbe essere implementato come

bool matches(tree_t* pattern, tree_t* replacement) { 
    if (pattern -> is_leaf && replacement -> is_leaf) 
     //do stuff, return a boolean 
    else if (pattern -> is_leaf && replacement -> is_branch) 
     //do stuff, return a boolean 
    else if (pattern -> is_branch && replacement -> is_leaf) 
     //do stuff, return a boolean 
    else if (pattern -> is_branch && replacement -> is_branch) 
     return matches(pattern -> left, replacement -> left) && matches(pattern -> right, replacement -> right); 
     //The above tests for equality recursively by testing for equality in each subtree. 
} 

Tuttavia, non sono sicuro di come implementare importanti dettagli di questo processo, compresi :

1. Corrispondenza di un albero di input con l'albero LHS di una regola di riduzione.
2. Trasformare l'albero di input nell'albero RHS della regola di riduzione, preservando i parametri (che possono essere foglie o rami) e "spostandoli" intorno alle loro posizioni appropriate.

Credo che la corrispondenza di modelli su un nodo implichi l'esame del figlio sinistro e del figlio destro del nodo e così via, fino a quando non si raggiungono i nodi terminali. Qualcuno sa di un programma o tutorial online che ha implementato un concetto simile in C e che potrei imparare da? Sono anche sulla strada giusta per affrontare il problema attraverso questo metodo, o c'è un modo più semplice?

Answer 1

È necessario prenderlo in due passaggi separati. Un modello di corrispondenza corrisponde a un modello rispetto a un albero e crea un dizionario che associa le variabili nel modello ai valori dell'albero.

Quindi si passa quel dizionario a una funzione separata che riempie la sostituzione, sostituendo le variabili con i relativi valori dal dizionario.

L'approccio di corrispondenza del modello descritto in SICP funzionerà correttamente in C, anche se potrebbe essere più semplice utilizzare una struttura di dati mutabile per il dizionario. Vedi https://mitpress.mit.edu/sicp/full-text/sicp/book/node99.html