Programmextraktion aus Beweisen
co I
⊆
co G
Till Überrück-Fries
30. November 2015
Till Überrück-Fries
Programmextraktion aus Beweisen
Erinnerung 1: Gray-Code
Wir betrachten die beiden Algebren G und H mit den Trägern
∗
|G| = {1, 1}∗ ∪ {1, 1}∗ ⊥11 und |H| =
∗
∗
{1, 1}+ ∪ {1, 1}+ ⊥11 ∪ ⊥1 .Sie sind rekursiv definiert durch:
G = (|G|, {LRa : G → G | a ∈ PSD} ∪ {U : H → G, nilG : G}),
H = (|H|, {Fina : G → H | a ∈ PSD} ∪ {D : H → H, nilH : H}).
Dabei ist die Bedeutung der Konstruktoren gegeben durch:
x −1
x
,
fU (x ) = ,
2
2
x +1
x
fFina = a
,
fD (x ) = .
2
2
Die Bedeutung eines Ausdrucks p = [c1 , c2 , . . .] des Typs G ist
dann gegeben durch
fLRa (x ) = −a
FG (p) =
∞
\
fc1 (fc2 (. . . fcn (I) . . .)).
n=1
Till Überrück-Fries
Programmextraktion aus Beweisen
Erinnerung 2:
co
G und
co
H
Wir konstruieren uns jetzt die Prädikate co G und co H für G und H. co G (x ) bedeutet dann ’x besitzt eine
Pre-Gray-Code-Darstellung’.
Dazu betrachten wir die folgenden Operatoren:
r
Γ(X , Y ) := {y | ∃x ∈X ∃a (y = −a
r
∆(X , Y ) := {y | ∃x ∈X ∃a (y = a
x −1
2
x +1
2
x
r
) ∨ ∃x ∈Y (y =
r
) ∨ ∃x ∈Y (y =
x
2
)}
2
)}
Das Größter-Fixpunkt-Axiom liefert uns ( co G , co H ). Es gilt das (verstärkte) Koinduktionsaxiom:
co
(X , Y ) ⊆ (Γ( G ∪ X ,
co
co
H ∪ Y ), ∆( G ∪ X ,
co
H ∪ Y ))
co
→ (X , Y ) ⊆ ( G ,
co
H)
Die co G -Klausel und die inverse co G -Klausel lauten:
nc co
r
∀x ( G (x ) → ∃x 0 ∈ co G ∃a (x = −a
nc
r
0
∀x (∃x 0 ∈ co G ∃a (x = −a
x −1
2
Till Überrück-Fries
x0 − 1
2
r
r
) ∨ ∃x 0 ∈ co H (x =
) ∨ ∃x 0 ∈ co H (x =
x
0
2
)→
co
x0
2
))
G (x ))
Programmextraktion aus Beweisen
Realisierbarkeit 1
Γr (Z , W ) := {(p, x ) | ∃(p 0 ,x 0 )∈Z ∃a (x = −a
x0 − 1
) ∧ p = LRa (p 0 ))∨u
2
x0
∧ p = U(q 0 ))},
2
x0 + 1
) ∧ q = Fina (p 0 ))∨u
∆r (Z , W ) := {(q, x ) | ∃(p 0 ,x 0 )∈Z ∃a (x = a
2
x0
∧ q = D(q 0 ))}.
∃(q0 ,x 0 )∈W (x =
2
∃(q0 ,x 0 )∈W (x =
Das Größter-Fixpunkt-Axiom von TCF liefert uns
(( coG )r , ( coH )r ) := ν(Z ,W ) (Γr (Z , W ), ∆r (Z , W ))
als den größter Fixpunkt von (Γr , ∆r ).
Till Überrück-Fries
Programmextraktion aus Beweisen
Realisierbarkeit 2
(( coG )r , ( coH )r ) erfüllt das (verstärkte) simultane
Koinduktionsaxiom:
(Z , W ) ⊆ (Γr (( coG )r ∪ Z , ( coH )r ∪ W ), ∆r (( coG )r ∪ Z , ( coH )r ∪ W ))
→ (Z , W ) ⊆ (( coG )r , ( coH )r )
Es bleibt zu zeigen, dass coG korrekt ist, d.h. der Zeuge von
co G (x ) ist genau die Pre-Gray-Code-Darstellung von x .
Proposition
Für x ∈ I und kototale Ideale p in G und q in H gilt
( coG )r (p, x ) ↔ x = FG (p),
( coH )r (q, x ) ↔ x = FH (q).
Kein Beweis.
Till Überrück-Fries
Programmextraktion aus Beweisen
co
I⊆
co
G
Wir wollen zeigen, dass jedes x , das eine Signed-Digit-Darstellung
besitzt auch eine Pre-Gray-Code-Darstellung besitzt. Also
Proposition
(CoIToCoG)
co
∀nc
x ( I (x ) →
co
G (x )).
Stattdessen zeigen wir die folgende stärkere Aussage:
Lemma
(CoIToCoGAux)
co
∀nc
x (∃a I (ax ) →
co
G x ),
co
∀nc
x (∃a I (ax )
co
H x ).
Till Überrück-Fries
→
Programmextraktion aus Beweisen
Beweis
Setze P := {x | ∃a (ax ∈ coI )}. Wir zeigen per Koinduktionsaxiom
(P, P) ⊆ ( coG , coH ). Also (i) P ⊆ Γ( coG ∪ P, coH ∪ P) und (ii)
P ⊆ Γ( coG ∪ P, coH ∪ P). (i): Sei x1 ∈ P. Dann nach inverser
co G -Klausel z.z.:
(∗) ∃rx ∈ coG ∪P ∃a (x1 = −a
x
x −1
∨ ∃rx ∈ coH ∪P (x1 = )
2
2
Da x1 ∈ P gibt es ein a1 , so dass coI (a1 x1 ). Die
x 0 +d
r
(∀nc
x ∈ co I ∃x 0 ∈ co I ∃d (x = 2 ) liefert uns
∃rx ∈ coI ∃d (a1 x1 =
Also haben wir x2 ∈
co I
x +d
).
2
und d, so dass a1 x1 =
Till Überrück-Fries
co I -Klausel
x2 +d
2 .
Programmextraktion aus Beweisen
Beweis Forts.
Fall d = −1: Mit x := x2 und a := −a1 gilt dann die linke Seite
von (∗), da x2 ∈ P und
x1 = a1 a1 x1 = a1
x2 − 1
x −1
x2 + d
= a1
= −a
.
2
2
2
Fall d = 1: Mit x := −x2 und a := a1 gilt dann die linke Seite von
(∗), da −x2 ∈ P und
x1 = a1 a1 x1 = a1
x2 + 1
−x2 − 1
x −1
x2 + d
= a1
= −a1
= −a
.
2
2
2
2
Fall d = 0: Mit x := a1 x2 gilt dann die rechte Seite von (∗), da
a1 x2 ∈ P und
x1 = a1 a1 x1 = a1
x2 + d
a1 x2
x
=
= .
2
2
2
Der Beweis von (ii) funktioniert genauso.
Till Überrück-Fries
Programmextraktion aus Beweisen
Minlog-Beweis
λ-Ausdrücke
Siehe gray.scm Zeilen 1893 - 2070.
Nach Z. 1900: (proof-to-expr)
Baum des λ-Ausdrucks
(lambda (xˆ)
(lambda (ExHyp7062)
((((Gfp xˆ) ExHyp7062) ((u7063 xˆ) ExHyp7062))
((u7064 xˆ) ExHyp7062))))
λ xˆ
λ ExHyp
•
•
•
•
•
Gfp
•
ExHyp
xˆ
u7063
•
ExHyp
•
u7064
ExHyp
xˆ
xˆ
Die Formeln u# sind die noch offenen Lücken des
Baumes.
Till Überrück-Fries
Programmextraktion aus Beweisen
Simultane Korekursion
Die simultanen Korekursionsoperatoren für G, H haben den Typ
co
RG
(G,H),(σ,τ )
: σ → δG → δH → G
co
(G,H),(σ,τ )
RH
: τ → δG → δH → H
mit den Schritttypen
δG := σ → PSD × (G + σ) + (H + τ ),
δH := τ → PSD × (G + σ) + (H + τ ).
Sie genügen den folgenden Konversionsregeln:
(
co
0
R G NMM 7→
(
co
R H N 0 MM 0 7→
LRπ1 (u) ([id, λy ( coR G yMM 0 )]π2 (u))
U([id, λz ( coR H zMM 0 )]v )
( coR
yMM 0 )]π
Finπ1 (u) ([id, λy
G
D([id, λz ( coR H zMM 0 )]v )
Till Überrück-Fries
2 (u))
Programmextraktion aus Beweisen
für MN=inl(u)
für MN=inr(v )
für M 0 N 0 =inl(u)
für M 0 N 0 =inr(v )
Extrahierter Term
Z. 2023:
(ppc neterm-CoIToCoGAux)
[bv]
(CoRec psd@@iv=>ag psd@@iv=>ah)bv
([bv0]
[case (left Des right bv0)
(Lft -> InL(inv left bv0@InR(PRht@right Des right bv0)))
(Rht -> InL(left bv0@InR(PLft@right Des right bv0)))
(Mid -> InR(InR(left bv0@right Des right bv0)))])
([bv0]
[case (left Des right bv0)
(Lft -> InL(inv left bv0@InR(PLft@right Des right bv0)))
(Rht -> InL(left bv0@InR(PRht@right Des right bv0)))
(Mid -> InR(InR(left bv0@right Des right bv0)))])
Dies lässt sich schreiben als
inl(−b, inr(1, v 0 ))
inl(b, inr(−1, v 0 ))
0
inr(inr(b, v ))
für d = −1,
für d = 1,
für d = 0,
inl(−b, inr(−1, v 0 ))
inl(b, inr(1, v 0 ))
inr(inr(b, v 0 ))
für d = −1,
für d = 1,
für d = 0.
Nochmal die Konversionsregel:
co
co
0
n
LRπ (u) ([id, λy ( co R G yMM 0 )]π2 (u))
1
U([id, λz ( co R H zMM 0 )]v )
0
n
Finπ (u) ([id, λy ( co R G yMM 0 )]π2 (u))
1
D([id, λz ( co R H zMM 0 )]v )
R G NMM 7→
0
R H N MM 7→
Till Überrück-Fries
Programmextraktion aus Beweisen
für MN=inl(u)
für MN=inr(v )
für M 0 N 0 =inl(u)
für M 0 N 0 =inr(v )
Impliziter Algorithmus
Dies liefert uns den impliziten Algorithmus: g : τ → G und
h : τ → H mit τ := PSD × I sind gegeben durch
g(b, C−1 (v )) = LR−b (g(1, v )), h(b, C−1 (v )) = Fin−b (g(−1, v )),
g(b, C1 (v ))) = LRb (g(−1, v )), h(b, C1 (v )) = Finb (g(1, v )),
g(b, C0 (v ))) = U(h(b, v )),
h(b, C0 (v )) = D(h(b, v )).
Till Überrück-Fries
Programmextraktion aus Beweisen
© Copyright 2024 ExpyDoc
