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?