<div dir="ltr">Hi Andrea,<br><br>Unfortunately, the --new-without-K flag doesn't solve the incompatibility between the termination checker and univalence (<a href="http://code.google.com/p/agda/issues/detail?id=1023">http://code.google.com/p/agda/issues/detail?id=1023</a>). 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<br>
<br><div style="margin-left:40px">noo : (X : Set) -> (WOne <-> X) -> X -> Zero<br>noo .WOne Refl (wrap f) = noo FOne iso f<br></div><br>is structurally recursive on the third argument, but this argument has type X which is not a datatype. <br>
<br>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. <br>
<br>Best,<br>Jesper<div class="gmail_extra"><br><br><div class="gmail_quote">On Mon, Mar 10, 2014 at 4:36 PM, Andrea Vezzosi <span dir="ltr"><<a href="mailto:sanzhiyan@gmail.com" target="_blank">sanzhiyan@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div>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"><div><div>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>
</div></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div><div><div><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></div></div>_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">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>
<br>_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">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></div>