Реализация комбинаторного исчисления

Question

концепция

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

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, Универсальный комбинатор йоты может быть определен следующим образом:

ι 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, и из которой я мог бы поучиться? Я даже на правильном пути в подходе к проблеме с помощью этого метода, или есть более простой способ?

Answer 1

Вы должны сделать это в два отдельных шага. Сопоставление шаблонов сопоставляет шаблон с деревом и создает переменные словаря, отображающие в шаблоне значения в дереве.

Затем вы передаете этот словарь отдельной функции, которая выполняет замену, заменяя переменные их значениями из словаря.

Подход сопоставления с шаблоном, описанный в SICP, будет отлично работать в C, хотя вам может оказаться проще использовать изменяемую структуру данных для словаря. См. https://mitpress.mit.edu/sicp/full-text/sicp/book/node99.html