[Agda] A correctness proof for pattern matching without K

[Jesper Cockx]

Hi Andrea,

Unfortunately, the --new-without-K flag doesn't solve the incompatibility
between the termination checker and univalence (
http://code.google.com/p/agda/issues/detail?id=1023). In my opinion, this
bug is a problem with the termination checker and not with --without-K (or
--new-without-K) itself. The problem is that you cannot do structural
recursion on a type that is not a datatype, for example the definition in
the bug report

noo : (X : Set) -> (WOne <-> X) -> X -> Zero
noo .WOne Refl (wrap f) = noo FOne iso f

is structurally recursive on the third argument, but this argument has type
X which is not a datatype.

This would be easy to fix if Agda had a concept of "the type on which we do
structural recursion", but for the better or the worse, Agda's termination
checker is much more complicated than that. So hopefully someone with more
knowledge of it can find a fix.

Best,
Jesper


On Mon, Mar 10, 2014 at 4:36 PM, Andrea Vezzosi <sanzhiyan at gmail.com> wrote:

> 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
>>
>>
>
> _______________________________________________
> 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/730773c4/attachment-0001.html