Основанное на унификации правило исключения для равенства

10

Несколько лет назад я наткнулся на следующее левое правило равенства в последовательном исчислении:

stθθ(Γ)θ(C)Γ,stC

Здесь stθ вычисляет наиболее общий объединитель θ для s и t , а затем применяет подстановку к заключению C и всем гипотезам в контексте Γ .

Интересная вещь об этом объединении - то, что оно уравнивает, находит замену универсальным (то есть, сколем) переменным.

Тем не менее, я не могу вспомнить, где я читал это, и мне было интересно, если кто-нибудь может помочь мне найти ссылку на это.

Нил Кришнасвами
источник

Ответы:

9

Я часто связывал это с Правилами рефлексии определений Шредера-Хейстера, хотя эта идея восходит к Жирару и другим; Правило, которое вы ищете, является экземпляром первого отображения в Разделе 4. Однако вам также необходимо правило, которое говорит, что если экземпляр объединения неудовлетворителен, то предположение о равенстве имеет силу противоречия.

Более общий отчет использовался в последнее время во многих работах Дейла Миллера, Дэвида Баэлда и компании (см., Например, Наименьшие и наибольшие фиксированные точки в линейной логике ). Более общая формулировка - которая также не происходит от Миллера и др. - это то, что правило

{θcsu(t,s)θΓθC}Γ,tsC

где - полный набор унификаторов - набор всех объединяющих подстановок и . Вы также можете предпочесть эквивалентный способ написания этого правила, которое я предпочитаю (см. Здесь, например).t scsu(t,s)ts

θ.θt=θsθΓθCΓ,tsC

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

no mgu(t,s)Γ,tsCmgu(t,s)=θθΓθCΓ,tsC

(PS Франк обсуждал это в своем курсе по логическому программированию в лекциях 6, 7 и 8, где, возможно, вы и помните.)

Роб Симмонс
источник
1
Спасибо! Я искал не те бумаги Шредера-Хейстера.
Нил Кришнасвами
2
Я, вероятно, должен добавить, что я думал об этом в контексте проверки типов для GADT.
Нил Кришнасвами
1
Да. Я писал об этом в контексте OMG ЭТОТ ДОЛЖЕН ВЫПУСКАТЬ, поэтому я не имею права думать об этом в контексте проверки типов для GADT ;-).
Роб Симмонс