Концепция

Я реализую интерпретатор, который позволяет пользователю определять произвольные комбинаторы и применять их к произвольным терминам. Например, пользователь может определить церковную кодировку для пар, введя следующие определения комбинатора. :

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

Затем пользователь может ввести first (pair a b), которое постепенно уменьшается в соответствии с ранее определенными правилами:

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

Также могут быть определены другие комбинаторы, например используемые в исчислении комбинаторов SKI:

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

Комбинатор идентификаторов также может быть определен в терминах первых двух комбинаторов с помощью I → S S K K, I → S K (K K) или I = S K x. Универсальный комбинатор iota может быть определен следующим образом:

ι x → x S K

Надеюсь, эти примеры иллюстрируют то, что я пытаюсь сделать.

Реализация

Я пытаюсь реализовать это с помощью сокращения графа и система перезаписи графов. Пусть tree будет типом данных, определяемым рекурсивно

tree = leaf | (tree tree)

Это бинарное дерево, узлы которого могут быть либо листьями (конечными узлами), либо ветвями (внутренними узлами), состоящими из пары поддеревьев. Ветви представляют применение термина к другому термину, а листья представляют комбинаторы и аргументы. Пусть rule будет типом данных, определенным

rule = (tree tree)

Это соответствует правилу редукции, которое преобразует левое дерево в правое дерево (a → b). Затем список rules может быть определен как

rules = rule | (rule rules)

По сути, при оценке такого выражения, как pair a b c → c a b, интерпретатор строит дерево формы (((pair a) b) c), соответствующее левой части, дерево формы ((c a) b), соответствующее правой части, строит пару обоих деревьев, соответствующих rule ( где a,b,c каким-то образом указаны как произвольные параметры и не обязательно комбинаторы или терминальные символы), и добавляет эту пару в список rules. При редукции выражения вида first (pair a b) интерпретатор строит соответствующее дерево (first ((pair a) b)) и применяет следующие правила редукции:

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

Для этого интерпретатор должен выполнить сопоставление с образцом в дереве и его поддеревьях, перемещаясь по комбинаторам и произвольным параметрам, чтобы построить новое дерево, соответствующее правой части правила. Пример реализации древовидной структуры в C дан

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

Функция сопоставления с образцом может быть реализована как

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.
}

Однако я не уверен, как реализовать важные детали этого процесса, в том числе:

1. Сопоставление входного дерева с деревом LHS правила редукции.
2. Преобразование входного дерева в RHS-дерево правила редукции с сохранением параметров (которые могут быть листьями или ветвями) и перемещением их в соответствующие места.

Я считаю, что сопоставление с образцом на узле будет включать проверку левого дочернего и правого дочерних элементов узла и так далее, пока не будут достигнуты конечные узлы. Кто-нибудь знает программу или учебник в Интернете, в котором реализована аналогичная концепция на C, и у которой я мог бы учиться? Я вообще на правильном пути в подходе к проблеме с помощью этого метода, или есть более простой способ?