beroal (beroal) wrote in category_theory,
beroal
beroal
category_theory

унификация термов

Полемика по поводу Joseph A. Goguen. “What is Unification? A Categorical View of Substitution, Equation and Solution.” (1989). Эта статья описывает унификацию в русле традиции, то есть подробно обсуждает унификацию 2 термов, то есть решение 1 уравнения. На практике приходится решать систему уравнений. Возьмём вывод типов для лямбда-исчисления. Каждый узел абстрактного синтаксического дерева программы даёт несколько уравнений, причём эти уравнения обычно имеют примитивную форму вроде τ01→τ2. В этом уравнении нечего решать. :-) Зато уравнений много. Более того, терм можно разбить на систему примитивных уравнений, например
f0(v0, f1(v1, f2(v2)))

f0(v0, v3);
v3 = f1(v1, v4);
v4 = f2(v2).
Примитивные уравнения я считаю более общей постановкой задачи, так как не знаю способа, как соединить систему примитивных уравнений в 1 уравнение термов (существует ли этот способ?). Хочу увидеть теоретический фундамент именно для системы уравнений.
Tags: substitution, unification
Subscribe
  • Post a new comment

    Error

    default userpic

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 3 comments