Я часто связывал это с Правилами рефлексии определений Шредера-Хейстера, хотя эта идея восходит к Жирару и другим; Правило, которое вы ищете, является экземпляром первого отображения в Разделе 4. Однако вам также необходимо правило, которое говорит, что если экземпляр объединения неудовлетворителен, то предположение о равенстве имеет силу противоречия.
Более общий отчет использовался в последнее время во многих работах Дейла Миллера, Дэвида Баэлда и компании (см., Например, Наименьшие и наибольшие фиксированные точки в линейной логике ). Более общая формулировка - которая также не происходит от Миллера и др. - это то, что правило
{θ∈csu(t,s)∣θΓ⊢θC}Γ,t≐s⊢C
где - полный набор унификаторов - набор всех объединяющих подстановок и . Вы также можете предпочесть эквивалентный способ написания этого правила, которое я предпочитаю (см. Здесь, например).t scsu(t,s)ts
∀θ.θt=θs⟶θΓ⊢θCΓ,t≐s⊢C
В любом случае, в языке терминов с разрешимым объединением, где наличие объединителя подразумевает существование наиболее общего объединителя, можно показать, что наличие любого из этих правил выше эквивалентно наличию этих двух правил:
no mgu(t,s)Γ,t≐s⊢Cmgu(t,s)=θθΓ⊢θCΓ,t≐s⊢C
(PS Франк обсуждал это в своем курсе по логическому программированию в лекциях 6, 7 и 8, где, возможно, вы и помните.)