[Agda] A correctness proof for pattern matching without K

[Andrea Vezzosi]

Hi,

This is very interesting, have you tested the flag on those examples that
use univalence to trick the termination checker into accepting non-total
functions?

Cheers,
Andrea



On Mon, Mar 10, 2014 at 3:28 PM, Jesper Cockx <Jesper at sikanda.be> wrote:

> Dear all,
>
> Some people might be interested that I finished the correctness proof for
> pattern matching without K. It proves the following:
>
> Let us restrict the unification algorithm used during case splitting in
> two ways:
> - It is not allowed to delete equations of the form "x = x".
> - When applying injectivity on an equation "c us = c vs" of type "D pars
> ixs", the datatype indices ixs (but not the parameters pars) should be
> *self-unifiable*, i.e. unification of ixs with itself should succeed
> (while still following these two restrictions).
> Let f be a function defined by dependent pattern matching (i.e. it has a
> valid case tree and is structurally recursive), where all case splits
> follow the restrictions above. Then we can translate f to a definition
> using only eliminators (*without* using the K axiom).
>
> The motivation for these two restrictions, as well as the proof, can be
> found in our submission to ICFP '14 called "Pattern matching without K",
> available here <http://people.cs.kuleuven.be/%7Ejesper.cockx/Without-K/>.
> The same page also contains a link to the updated implementation of my
> --new-without-K flag, which enforces the two restrictions to the
> unification algorithm above.
>
> Here are some examples that are rejected by the current --without-K flag,
> but are accepted by --new-without-K:
>
> {-# OPTIONS --new-without-K #-}
> module Counterexamples where
>
> open import Data.Nat
> open import Relation.Binary.PropositionalEquality
>
> ≤-self : (m : ℕ) → m ≤ m → ⊤
> ≤-self .zero (lz .zero) = tt
> ≤-self .(suc m) (ls m .m p) = tt
>
> sum-right : (k l m : ℕ) → k ≡ (l + m) → ⊤
> sum-right .(l + m) l m refl = tt
>
> Compared to the regular --without-K, it now also handles parameters much
> better. For example, the following is rejected by --without-K but accepted
> by --new-without-K:
>
> open import Data.List
>
> head-≡ : {A : Set} {x y : A} {xs ys : List A} →
>         x ∷ xs ≡ y ∷ ys → x ≡ y
> head-≡ refl = refl
>
> In fact, we place no restrictions on the parameters at all. On the other
> hand, injectivity of indexed data still poses a problem:
>
> open import Data.Fin using (Fin) renaming (zero to fz; suc to fs)
>
> drop-fs : ∀ {n} (x y : Fin n) → fs x ≡ fs y → x ≡ y
> drop-fs x .x refl = refl
> -- Error: Cannot eliminate reflexive equation n = n of type ℕ because K
> has been disabled.
> -- when checking that the pattern refl has type fs x ≡ fs y
>
> Be aware that this definition is rejected by the regular --without-K flag
> as well. However, this kind of problem occurs somewhat more often than
> before because of the second restriction to the unification algorithm. This
> restriction is a necessary evil to solve the bug discussed in a previous
> mail <https://lists.chalmers.se/pipermail/agda/2014/006367.html>, but
> I'll be the first to agree that it seems overly restrictive.  In practice,
> I don't usually run into this problem, but YMMV. I have tested my
> implementation on Nils' --without-K library (
> http://www.cse.chalmers.se/~nad/repos/equality/) without encountering any
> problems. The easiest way to solve this problem, seems to add (manual or
> automatic) detection of types that satisfy K on their own (i.e. homotopy
> sets), for example ℕ. I'll probably be working on this in the future, but
> in my opinion the implementation is already very usable right now.
>
> All questions, remarks, and suggestions are very welcome.
>
> Best regards,
> Jesper Cockx
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140310/6cfbc4f3/attachment.html