Newer
Older
inria-internship / proofs.org Gabriel Scherer on 31 Mar 2020 9 KB clarify lines 65-68
```* First blackboard

** Definitions

Translation to constraint trees:

[|_|]ₛ : Source Terms -> Source Constraint Trees
[|_|]ₜ : Target Terms -> Target Constraint Trees

Running a {program, constraint tree} against an input

result r ::= guard list * (Match bb | NoMatch | Absurd)
guard := bb
(same blackboxes 'bb' for source and target programs and constraint trees)

tₛ(vₛ) → r
tₜ(vₜ) → r

Cₛ(vₛ) → r
Cₜ(vₜ) → r

Equivalence of values, programs and constraint trees:

vₛ ≃ vₜ    (TODO define, this talks about the representation of source values in the target)
tₛ ≃ tₜ := (∀vₛ≃vₜ, tₛ(vₛ)=tₜ(vₜ))
Cₛ ≃ Cₜ := (∀vₛ≃vₜ, Cₛ(vₛ)=Cₜ(vₜ))

Our equivalence algorithm on constraint trees:

equiv Cₛ Cₜ → Yes | No(vₛ,vₜ)

(Yes: equivalent, No: here is a pair of inputs as counter-example)

** Statements

Theorem: Correctness of translation to constraint trees:

∀vₛ, tₛ(vₛ) = [|tₛ|]ₛ(vₛ)
∀vₜ, tₜ(vₜ) = [|tₜ|]ₜ(vₜ)

Definition: Equivalence of results modulo guard queue (r₁ ≃gs r₂):
(gs₁, mr₁) ≃gs (gs₂, mr₂)  ⇔  (gs₁, mr₁) = (gs₂ ++ gs, mr₂)

Theorem: Correctness of the equivalence of constraint trees

(equiv S Cₛ Cₜ gs = Yes)      ∧ covers(Cₜ, S) ⇒ ∀vₛ≃vₜ ∈ S, Cₛ(vₛ) ≃gs Cₜ(vₜ)
(equiv S Cₛ Cₜ gs = No(vₛ,vₜ) ∧ covers(Cₜ, S) ⇒ vₛ≃vₜ ∈ S ∧ Cₛ(vₛ) ≠gs Cₜ(vₜ)

Corollary (our main result):
(equiv FullInputSpace [|tₛ|]ₛ [|tₜ|]ₜ ∅ = Yes)  ⇔  tₛ ≃ tₜ

*** Draft of proof for equivalence between constraint trees and source/target programs

tₛ      ::= (p → bb)ⁱ  # i ∈ I
p       ::= | K(pᵢ)ⁱ, i ∈ I | (p|q) | n ∈ ℕ        # t should be T in latex
tₜ      ::= if condₜ tₜ tₜ | let x = eₜ in tₜ | switch((pₜᵢ → tₜᵢ)ⁱ tₜ? | catch(tₜ, l(yᵢ)ⁱ  → tₜ) | exit l (eₜᵢ)ⁱ
i ∈ I
condₜ   ::= eₜ bop n eₜ::=x | eₜ.n

Cₛ      ::= Leaf bb | Node(a, (Kᵢ → Cᵢ)ⁱ , C?) # i ∈ S
a       ::= Here | n.a
vₛ      ::= K(vᵢ)ⁱ | n ∈ ℕ   # i ∈ I

SMatrix mₛ := (aᵢ)ʲ, ((pᵢⱼ)ʲ → bbᵢ)ⁱ  # i ∈ I j ∈ Jᵢ # i columns, j rows, order matters
# what about size of the matrix? How to write it?

We define the constraint tree of source programs
[|tₛ|]
in terms of the constraint tree of pattern matrices
[|mₛ|]
by the following:
[|((pᵢ → bbᵢ)ⁱ|] := [| (Root), ((pᵢ → bbᵢ)ⁱ |] # i ∈ I

Naïve and incorrect correctness statement for the constraint tree of a matrix:
∀(vᵢ)ⁱ, [|(aᵢ)ⁱ, (rᵢ)ⁱ|](vᵢ)ⁱ = ((aᵢ)ⁱ, (rᵢ)ⁱ)(vᵢ)ⁱ
(this doesn't make sense because a constraint tree takes a single value as input,
not a vector (vᵢ)ⁱ)

Correctness statement for the constraint tree of a matrix:
∀v (vᵢ)ⁱ = v(aᵢ)ⁱ → [|m|](v) = m(vᵢ)ⁱ for m = ((aᵢ)ⁱ, (rᵢ)ⁱ)

# base cases
[| ∅, (∅ → bbᵢ)ⁱ |] := Leaf bbᵢ where i := min(I)
[| (aⱼ)ʲ, ∅ |] := Failure
#

[| aⱼ, rⱼ |] := (cols(mₛ)>1) := let Groups((aⱼ)ᴵ,(rᵢ)ⁱ) be (Kₖ → mₖ), m_{wildcards)
if (Kₖ)ᵏ is complete then
Node( aₘᵢₙ₍ⱼ₎, Kₖ → [| mₖ |]ᵏ)
else
Node( aₘᵢₙ₍ⱼ₎, Kₖ → [| mₖ |]ᵏ, [|m_{wildcards}|])

**** Sterms -> STrees

SMatrix mₛ := (aⱼ)ʲ, ((pᵢⱼ)ʲ → bbᵢ)ⁱ
∀(vⱼ)ʲ, mₛ(vⱼ)ʲ = [|mₛ|](vⱼ)ʲ

v(Here) = v
K(vᵢ)ⁱ(k.a) = vₖ(a) if k ∈ [0;n[

We also said that
(Leaf bb)(v) := Match bb
(Node(a, (kᵢ → cᵢ)ⁱ, c_{fallback}))(v)
let v(a) be K(vⱼ)ʲ
if k ∈ {Kᵢ}ⁱ then  C_{min{i}|k=kᵢ}(v)
else c_{fallback}(v)

**** Proof of the non-base case
let Idx(k) = [0; arity(k)[
let First(∅) = ⊥
let First((aⱼ)ʲ) = aₘᵢₙ₍ⱼ₎ ## where j ∈ J ≠ ∅

Correct(m) := ∀v, (vᵢ)ⁱ = v(aᵢ)ⁱ => m(vᵢ)ⁱ = [|m|](v)

Groups(m) = (kᵣ → mᵣ)ᵏ, m_{wild}
(vᵢ)ᴵ, v₀ = k(v'ₗ)ˡ  ## l ∈ Idx(k) ## v' child of the constructor
if k = kₖ for some k then
m(vᵢ)ⁱ = mₖ((v'ₗ)ˡ +++ (vᵢ)ⁱ)  ## where last i:= i ≠ 0
else
m(vᵢ)ⁱ = m_{wild}(vᵢ)ⁱ ## where last i:= i ≠ 0

m(vᵢ)ⁱ = First(rⱼ(vᵢ)ⁱ)ʲ for m = ((aᵢ)ⁱ, (rⱼ)ʲ)
(pᵢ)ⁱ (vᵢ)ⁱ  =  {
if p₀ = k(qₗ)ˡ, v₀ = k'(v'ₖ)ᵏ, k=Idx(k') and l=Idx(k)
if k ≠ k' then ⊥
if k = k' then ((qₗ)ˡ +++ (pᵢ)ⁱ) ((v'ₖ)ᵏ +++ (vᵢ)ⁱ) ## where i ≠ 0
if p₀ = (q₁|q₂) then
First(  (q₁pᵢⁱ) vᵢⁱ, (q₂pᵢⁱ) vᵢⁱ  ) ## where i ≠ 0
}

let Groups(m) where m = ((aᵢ)ⁱ ((pᵢⱼ)ⁱ → eⱼ)ⁱʲ) =
let (kₖ)ᵏ = headconstructor(pᵢ₀)ⁱ in
( kₖ →
((a₀.ₗ)ˡ +++ (aᵢ)ⁱ),   ## where l ∈ Idx(kₖ) and i ∈ I\{0}
(
if pₒⱼ is k(qₗ) then
(qₗ)ˡ +++ (pᵢⱼ)ⁱ  → eⱼ  ## i ≠ 0
if pₒⱼ is _ then
(_)ˡ +++ (pᵢⱼ)ⁱ   → eⱼ  ## i ≠ 0
else ⊥
)ʲ
),(
(aᵢ)ⁱ, ((pᵢⱼ)ⁱ  → eⱼ if p₀ⱼ is _ else ⊥)ʲ ## where i ≠ 0 and j ∈ J

*** Proof of equivalence checking

equiv(S, Cₛ, Cₜ) → Yes | No(vₛ, vₜ)
equiv(S, Cₛ, Cₜ) = Yes and cover(Cₜ, S) → ∀ vₛ ≊ vₜ∈S ∧ Cₛ(vₛ) = Cₜ(vₜ)
equiv(S, Cₛ, Cₜ) = No(vₛ,vₜ) and cover(Cₜ, S) → ∀ vₛ ≊ vₜ∈S ∧ Cₛ(vₛ) ≠ nCₜ(vₜ)

∀v∈a→π, C_{/a→π}(v) = C(v)
Forall(Yes) = Yes
Forall(Yes::l) = Forall(l)
Forall(No(vₛ,vₜ)::_) = No(vₛ,vₜ)
There exists and are injective:
int(k)∈ℕ (ar(k) = 0)
tag(k)∈ℕ (ar(k) > 0)
π(k) = {n|int(k) = n} x {n|tag{k} = n}

1. equiv(∅, Cₛ, Cₜ) := Yes
# below S ≠ ∅
2. equiv(S, Failure, Failure) := Yes
equiv(S, Leaf bbₛ, Leaf bbₜ) := if bbₛ = bbₜ then Yes else No(vₛ, [|vₛ|]) for vₛ ∈ S
3. equiv(S, (Leaf bbₛ|Failure) as Cₛ, Node(a, (πᵢ → Cₜᵢ)ⁱ)) :=
Forall(equiv( S∩a→π(kᵢ)), Cₛ, Cₜᵢ)ⁱ)

4. equiv(S, Node(a, (kᵢ → Cₛᵢ)ⁱ, C_{sf}), Cₜ) :=
let π' = ⋃π(kᵢ) ∀i in
Forall(equiv( S∩(a→π(kᵢ)ⁱ), Cₛᵢ, C_{t/a→π(kᵢ)})ⁱ +++ equiv(S∩(a→π(kᵢ)), Cₛ, C_{/a¬̸π'}))

Proof:
3. let Sᵢ := S∩(a→πᵢ)
either
equiv(Sᵢ, Cₛ, Cₜᵢ) = Yes ∀i
or
equiv(Sᵢ, Cₛ, Cₜᵢ) = No(vₛ, vₜ) for some minimal k∈I
# valid because:
vₛ≊vₜ∈Sₖ ∧ cₛ(vₛ) ≠ Cₜₖ(vₜ)
then  vₛ≊vₜ∈S vₛ≊vₜ ∧ Cₛ(vₛ)≠Cₜ(vₜ)
#because vₜ∈(a→πₖ) ⇒ Cₜ(vₜ) = Cₜₖ(vₜ)

4. Trimming lemma:
∀vₜ ∈ (a→π), Cₜ(vₜ) = C_{t/a→π(kᵢ)}(vₜ)
# Proof on induction on Cₜ:
a. Case where Cₜ = Leaf_{bb}:
Leaf_{bb/a→π}(v) = Leaf_{bb}(v) ## trimming leaf is leaf itself
b. # Same for failure terminal
e. # in case of unreachabe → ⊥
c. Case in which Cₜ is Node(b, (π→Cᵢ)ⁱ)_{/a→π}  then
let πᵢ' =  πᵢ if a≠b else πᵢ∩π  in
Node(b, (π→Cᵢ)ⁱ)_{/a→π} :=  Node(b, (π'ᵢ→C_{i/a→π})ⁱ)

Goal: prove that Cₜ(vₜ) = Node(b, (πᵢ'→C_{i/a→π})ⁱ)(vₜ)
# two cases:
i.  vₜ∉(b→πᵢ)ⁱ => failure = failure
ii. vₜ∈(b→πₖ) for some k =>
C_{k/a→π}(vₜ) = Node(b, (πᵢ'→C_{i/a→π})ⁱ)(vₜ) #because
#when a ≠ b then πₖ'=πₖ => vₜ∈πₖ'
#when a = b  then πₖ'=(πₖ∩π) and
vₜ∈π #because_of_hypothesis and
vₜ∈πₖ #because_of_subcase_ii
=> vₜ ∈ πₖ'
#and
Cₖ(vₜ) = C_{k/a→π}(vₜ) #by #induction #and
Cₜ(vₜ) = Cₖ(vₜ) #because vₜ∈(b→πₖ)
=> Node(b, (πᵢ'→C_{i/a→π})ⁱ)(vₜ) = Cₜ(vₜ)

Covering lemma:
∀a,π covers(Cₜ,S) => covers(C_{t/a→π}, (S∩a→π))
Uᵢπⁱ ≈ Uᵢπ'∩(a→π) ≈ (Uᵢπ')∩(a→π) # TODO swap π and π'

4. ∀S, Cₜ covers S → {
- equiv(S, Cₛ, Cₜ) = Yes => ∀vₛ≊vₜ∈S, Cₛ(vₛ) = Cₜ(vₜ)
- equiv(S, Cₛ, Cₜ) = No(vₛ, vₜ) => vₛ≊vₜ∈S ∧ Cₛ(vₛ) ≠ Cₜ(vₜ)
# Case analysis of Forall
e. in case of unreachable Cₛ(vₛ) = Absurd(Unreachable) ≠ Cₜ(vₜ) always # no unreachable in Cₜ
a. Forall(...) = Yes
Consider vₛ(a) = K(v'ⱼ)
# Case analysis k∈(kᵢ)ⁱ or k∉(kᵢ)ⁱ
i. k=kₖ for some k then Cₛ(vₛ) = Cₛᵢ(vₛ)
# Ind. hyp.:
Cₛᵢ(vₛ) = C_{t/a→πᵢ}(vₜ)
# and we know that, for the trimming lemma
Cₜ(vₜ) = C_{t/a→πᵢ}(vₜ)

b. Forall(...) = No(vₛ, vₜ)
for a minimum k, equiv(Sₖ, Cₛₖ, C_{t/a→πₖ} = No(vₛ, vₜ)
then Cₛₖ(vₛ) ≠ C_{t/a→πₖ}(vₜ)  and C_{t/a→πₖ}(vₜ) = Cₜ(vt)
=> (Cₛₖ(vₛ) = Cₛ(vₛ)) ≠ Cₜ(vₜ) # Same for fallback?
```