Vereinigungsbasierte Eliminierungsregel für Gleichheit

10

Vor ein paar Jahren bin ich auf die folgende linke Regel für Gleichheit in der sequentiellen Berechnung gestoßen:

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

Hier berechnet stθ den allgemeinsten Unifier θ für s und t und wendet dann die Substitution auf die Schlussfolgerung C und alle Hypothesen im Kontext Γ .

Das Interessante an dieser Vereinigung ist, dass sie einen Ersatz für universelle (dh skolemische) Variablen findet.

Ich kann mich jedoch nicht erinnern, wo ich das gelesen habe, und habe mich gefragt, ob mir jemand helfen könnte, einen Hinweis darauf zu finden.

Neel Krishnaswami
quelle

Antworten:

9

Ich habe dies oft den Regeln der Definitionsreflexion von Schröder-Heister zugeschrieben, obwohl die Idee darüber hinaus auf Girard und andere zurückgeht; Die Regel, nach der Sie suchen, ist eine Instanz der ersten Anzeige in Abschnitt 4. Sie benötigen jedoch auch eine Regel, die besagt, dass die Annahme der Gleichheit die Kraft eines Widerspruchs hat, wenn die Vereinigungsinstanz nicht zufriedenstellend ist.

Ein allgemeinerer Bericht wurde kürzlich in vielen Arbeiten von Dale Miller, David Baelde und der Firma verwendet (siehe zum Beispiel die kleinsten und größten Fixpunkte in der linearen Logik ). Die allgemeinere Formulierung - die auch nicht von Miller et al. Stammt - ist, dass die Regel lautet

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

Dabei ist der vollständige Satz von Unifikatoren - der Satz aller einheitlichen Substitutionen von und . Möglicherweise bevorzugen Sie auch die von mir bevorzugte äquivalente Schreibweise dieser Regel (siehe hier zum Beispiel).csu(t,s)ts

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

In jedem Fall kann in einer Begriffssprache mit entscheidbarer Vereinigung, in der die Existenz eines Vereinigers die Existenz eines allgemeinsten Vereinigers impliziert, gezeigt werden, dass eine der oben genannten Regeln den beiden folgenden Regeln entspricht:

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

(PS Frank hat dies in seinem Logikprogrammierkurs in den Vorlesungen 6, 7 und 8 besprochen , an die Sie sich möglicherweise erinnern.)

Rob Simmons
quelle
1
Vielen Dank! Ich habe mir die falschen Papiere von Schroeder-Heister angesehen.
Neel Krishnaswami
2
Ich sollte wahrscheinlich hinzufügen, dass ich im Rahmen der Typprüfung für GADTs darüber nachgedacht habe.
Neel Krishnaswami
1
Huh. Ich habe darüber im Rahmen von OMG THESIS MUST GRADUATE geschrieben, daher darf ich im Rahmen der Typprüfung für GADTs nicht darüber nachdenken ;-).
Rob Simmons