Reguła eliminacji równości oparta na ujednoliceniu

Kilka lat temu natknąłem się na następującą lewą zasadę równości w rachunku różniczkowym:

$$\frac{s \doteq t \leadsto \theta \qquad \theta(\Gamma) \vdash \theta(C)} {\Gamma, s \doteq t \vdash C}$$

Tutaj, Oblicza najogólniejszym unifikatorem dla i , a następnie stosuje substition do wniosku, i wszystkich możliwości w kontekście .θ s t C $s \doteq t \leadsto \theta$$\theta$$s$$t$$C$$\Gamma$

Interesującą rzeczą w tej unifikacji jest to, że utożsamia ona zastępowanie zmiennych uniwersalnych (tj. Skolem).

Nie pamiętam jednak, gdzie to przeczytałem, i zastanawiałem się, czy ktoś mógłby mi pomóc znaleźć odniesienie do tego.

Często przypisywałem to Regułom definicyjnej refleksji Schroedera-Heistera, choć idea ta sięga dalej niż do Girarda i innych; reguła, której szukasz, jest instancją pierwszego pokazu w Sekcji 4. Jednak potrzebujesz również reguły, która mówi, że jeśli instancja zjednoczenia jest niezadowalająca, wówczas założenie równości ma moc sprzeczności.

Bardziej ogólne konto zostało ostatnio użyte w wielu pracach przez Dale'a Millera, Davida Baelde i firmę (patrz na przykład Najmniejsze i największe stałe punkty w logice liniowej ). Bardziej ogólne sformułowanie - które również nie pochodzi od Millera i in. - jest takie, że reguła jest taka

$${\{\theta \in {\sf csu}(t,s) \mid \theta\Gamma \vdash \theta{C} \}}\over{\Gamma, t \doteq s \vdash C}$$

gdzie jest kompletnym zestawem unifikatorów - zbiorem wszystkich unifikujących podstawień i . Możesz również preferować równoważny sposób pisania tej reguły, który wolę (patrz tutaj na przykład).t ${\sf csu}(t,s)$$t$$s$

$${\forall \theta. \theta{t} = \theta{s} \longrightarrow \theta\Gamma \vdash \theta{C}}\over{\Gamma, t \doteq s \vdash C}$$

W każdym razie, w języku terminów o rozstrzygającym ujednoliceniu, w którym istnienie unifikatora implikuje istnienie najbardziej ogólnego unifikatora, wykazanie, że jedna z powyższych reguł jest równoważna z posiadaniem tych dwóch reguł:

$${{{\sf no~mgu}(t,s)}\over{\Gamma, t \doteq s \vdash C}} \qquad {{{\sf mgu}(t,s) = \theta \quad \theta\Gamma \vdash \theta{C}}\over{\Gamma, t \doteq s \vdash C}}$$

(PS Frank omawiał to na swoim kursie programowania logicznego w wykładach 6, 7 i 8, z którego to miejsca pamiętasz.)