<div dir="ltr">Hi,<div><br></div><div>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?</div><div><br></div><div>Cheers,</div>
<div>Andrea</div><div><br></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Mon, Mar 10, 2014 at 3:28 PM, Jesper Cockx <span dir="ltr"><<a href="mailto:Jesper@sikanda.be" target="_blank">Jesper@sikanda.be</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><div><div>Dear all,<br><br></div><div>Some people might be interested that I finished the correctness proof for pattern matching without K. It proves the following:<br>
<br></div><div style="margin-left:40px">
Let us restrict the unification algorithm used during case splitting in two ways:<br></div><div style="margin-left:40px">- It is not allowed to delete equations of the form "x = x".<br></div><div style="margin-left:40px">
-
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 <i>self-unifiable</i>, i.e. unification of ixs with itself should succeed (while still following these two restrictions).<br></div><div><div style="margin-left:40px">
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 (<i>without</i> using the K axiom).<br></div><br></div><div>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 <a href="http://people.cs.kuleuven.be/%7Ejesper.cockx/Without-K/" target="_blank">here</a>.
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.<br></div><div><br></div><div>Here are some examples that are rejected by the current --without-K flag, but are accepted by --new-without-K:<br></div><div style="margin-left:40px"><br>{-# OPTIONS --new-without-K #-} <br>
</div><div style="margin-left:40px">module Counterexamples where<br></div><div style="margin-left:40px"><br>open import Data.Nat<br>open import Relation.Binary.PropositionalEquality<br><br>≤-self : (m : ℕ) → m ≤ m → ⊤<br>
≤-self .zero (lz .zero) = tt<br>≤-self .(suc m) (ls m .m p) = tt<br><br>sum-right : (k l m : ℕ) → k ≡ (l + m) → ⊤<br>sum-right .(l + m) l m refl = tt<br><br></div>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:<br>
</div><div><div style="margin-left:40px"><br>open import Data.List<br><br>head-≡ : {A : Set} {x y : A} {xs ys : List A} → <br> x ∷ xs ≡ y ∷ ys → x ≡ y<br>head-≡ refl = refl</div><br>
In fact, we place no restrictions on the parameters at all. On the
other hand, injectivity of indexed data still poses a problem:<br></div><br><div style="margin-left:40px">open import Data.Fin using (Fin) renaming (zero to fz; suc to fs)<br><br>drop-fs : ∀ {n} (x y : Fin n) → fs x ≡ fs y → x ≡ y<br>
drop-fs x .x refl = refl<br>-- Error: Cannot eliminate reflexive equation n = n of type ℕ because K has been disabled.<br>-- when checking that the pattern refl has type fs x ≡ fs y<br></div><br></div>
<div>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 href="https://lists.chalmers.se/pipermail/agda/2014/006367.html" target="_blank">a previous mail</a>,
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
(<a href="http://www.cse.chalmers.se/~nad/repos/equality/" target="_blank">http://www.cse.chalmers.se/~nad/repos/equality/</a>) 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.<br><br></div>
All questions, remarks, and suggestions are very welcome.<br>
<div><br></div>
<div>Best regards,<br></div>
Jesper Cockx</div>
<br>_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div>