UniTO/tesi/drafts/partial-decomposition-proof.org

Auxiliary operations:

index family of a constructor Idx(K) := [0; arity(K)[

head of an ordered family (we write x for any object here, value, pattern etc.) head((xᵢ)^{i ∈ I}) = x_min(I)

tail of an ordered family tail((xᵢ)^{i ∈ I}) := (xᵢ)^{i ≠ min(I)}

head constructor of a value or pattern constr(K(xᵢ)ⁱ) = K constr(_) = ⊥ constr(x) = ⊥

first non-⊥ element of an ordered family First((xᵢ)ⁱ) := ⊥ if ∀i, xᵢ = ⊥ First((xᵢ)ⁱ) := x_min{i | xᵢ ≠ ⊥} if ∃i, xᵢ ≠ ⊥

Definition of running a pattern row against a (same-size) value vector (pᵢ)ⁱ(vᵢ)ⁱ ∅ (∅) := [] (_, tail(pᵢ)ⁱ) (vᵢ) := tail(pᵢ)ⁱ(tail(vᵢ)ⁱ) (x, tail(pᵢ)ⁱ) (vᵢ) := σ[x↦v₀] if tail(pᵢ)ⁱ(tail(vᵢ)ⁱ) = σ (K(qⱼ)ʲ, tail(pᵢ)ⁱ) (K(v'ⱼ)ʲ,tail(vⱼ)ʲ) := ((qⱼ)ʲ + tail(pᵢ)ⁱ)((v'ⱼ)ʲ + tail(vᵢ)ⁱ) (K(qⱼ)ʲ, tail(pᵢ)ⁱ) (K'(v'ₗ)ˡ,tail(vⱼ)ʲ) := ⊥ if K ≠ K' (q₁|q₂, tail(pᵢ)ⁱ) (vᵢ)ⁱ := First((q₁,tail(pᵢ)ⁱ)(vᵢ)ⁱ, (q₂,tail(pᵢ)ⁱ)(vᵢ)ⁱ)

Definition of group decomposition: let constrs((pᵢ)^{i ∈ I}) = { K | K = constr(pᵢ), i ∈ I } let Groups(m) where m = ((aᵢ)ⁱ ((pᵢⱼ)ⁱ → eⱼ)ⁱʲ) = let (Kₖ)ᵏ = constrs(pᵢ₀)ⁱ in ( Kₖ → ((a₀.ₗ)ˡ + tail(aᵢ)ⁱ) ( if pₒⱼ is Kₖ(qₗ) then (qₗ)ˡ + tail(pᵢⱼ)ⁱ → eⱼ if pₒⱼ is _ then (_)ˡ + tail(pᵢⱼ)ⁱ → eⱼ else ⊥ )ʲ ), ( tail(aᵢ)ⁱ, (tail(pᵢⱼ)ⁱ → eⱼ if p₀ⱼ is _ else ⊥)ʲ )

Groups(m) is an auxiliary function that decomposes a matrix m into submatrices, according to the head constructor of their first pattern. Groups(m) returns one submatrix m_r for each head constructor K that occurs on the first row of m, plus one "wildcard submatrix" m_wild that matches on all values that do not start with one of those head constructors.

Intuitively, m is equivalent to its decomposition in the following sense: if the first pattern of an input vector (v_i)^i starts with one of the head constructors Kₖ, then running (v_i)^i against m is the same as running it against the submatrix m_Kₖ; otherwise (its head constructor is none of the Kₖ) it is equivalent to running it against the wildcard submatrix.

We formalize this intuition as follows:

Lemma (Groups): Let $m$ be a matrix with $Groups(m) = (kᵣ → mᵣ)ᵏ, m_{wild}$. For any value vector $(vᵢ)ᴵ$ such that $v₀ = K(v'ₗ)ˡ$ for some constructor K, we have: \[ if K = Kₖ for some k then m(vᵢ)ⁱ = mₖ((v'ₗ)ˡ +++ (vᵢ)^{i∈I\{0}}) otherwise m(vᵢ)ⁱ = m_{wild}(vᵢ)^{i∈I\{0}} \]

Proof:

Let $m$ be a matrix ((aᵢ)ⁱ, ((pᵢⱼ)ⁱ → eⱼ)ʲ) with $Groups(m) = (Kₖ → mₖ)ᵏ, m_{wild}$.

Below we are going to assume that m is a simplified matrix:

the first row does not with an or-pattern or a variable

I think it would be simpler to not consider them at all in the formalization. If we do want them, the discrepancy can be fixed later by defining a simplification step that explodes head-or-patterns and binds variable, and showing that it preserves the matrix semantics.

Let (vᵢ)ⁱ be an input matrix with v₀ = Kᵥ(v'ₗ)ˡ for some constructor Kᵥ.

We have to show that:

• if Kₖ = Kᵥ for some Kₖ ∈ constrs(p₀ⱼ)ʲ, then m(vᵢ)ⁱ = mₖ((v'ₗ)ˡ + tail(vᵢ)ⁱ)
• otherwise m(vᵢ)ⁱ = m_wild(tail(vᵢ)ⁱ)

Let us call (rₖⱼ) the j-th row of the submatrix mₖ, and rⱼ_wild the j-th row of the wildcard submatrix m_wild.

Our goal contains same-behavior equalities between matrices, for a fixed input vector (vᵢ)ⁱ. It suffices to show same-behavior equalities between each row of the matrices for this input vector. We show that for any j,

• if Kₖ = Kᵥ for some Kₖ ∈ constrs(p₀ⱼ)ʲ, then (pᵢⱼ)ⁱ(vᵢ)ⁱ = rₖⱼ((v'ₗ)ˡ + tail(vᵢ)ⁱ
• otherwise (pᵢⱼ)ⁱ(vᵢ)ⁱ = rⱼ_wild tail(vᵢ)ⁱ

In the first case (Kᵥ is Kₖ for some Kₖ ∈ constrs(p₀ⱼ)ʲ), we have to prove that

(pᵢⱼ)ⁱ(vᵢ)ⁱ = rₖⱼ((v'ₗ)ˡ + tail(vᵢ)ⁱ

By definition of mₖ we know that rₖⱼ is equal to

if pₒⱼ is Kₖ(qₗ) then (qₗ)ˡ + tail(pᵢⱼ)ⁱ → eⱼ if pₒⱼ is _ then (_)ˡ + tail(pᵢⱼ)ⁱ → eⱼ else ⊥

By definition of (pᵢ)ⁱ(vᵢ)ⁱ we know that (pᵢⱼ)ⁱ(vᵢ) is equal to

(K(qⱼ)ʲ, tail(pᵢⱼ)ⁱ) (K(v'ₗ)ˡ,tail(vᵢ)ⁱ) := ((qⱼ)ʲ + tail(pᵢⱼ)ⁱ)((v'ₗ)ˡ + tail(vᵢ)ⁱ) (_, tail(pᵢⱼ)ⁱ) (vᵢ) := tail(pᵢⱼ)ⁱ(tail(vᵢ)ⁱ) (K(qⱼ)ʲ, tail(pᵢⱼ)ⁱ) (K'(v'ₗ)ˡ,tail(vⱼ)ʲ) := ⊥ if K ≠ K'

We prove this first case by a second case analysis on p₀ⱼ.

TODO

In the second case (Kᵥ is distinct from Kₖ for all Kₖ ∈ constrs(pₒⱼ)ʲ), we have to prove that

(pᵢⱼ)ⁱ(vᵢ)ⁱ = rⱼ_wild tail(vᵢ)ⁱ

TODO