Order of clauses matters to much; equations should hold definitionally whenever possible.

[UlfNorell]

From andreas....@gmail.com on April 18, 2011 13:59:25

(See attached file.)

In a definition of parallel substitution for strongly typed terms I wrote:

subst : ∀ {m} {vt : VarTrm m} (tau : RenSub vt) → Tm → Tm subst {vt = Var} tau (var x) = var (tau x) -- lookup in renaming subst {vt = Trm} tau (var x) = tau x -- lookup in substitution subst {vt = vt } tau (abs t) = abs (subst (lift tau) t) subst {vt = vt } tau (app t u) = app (subst tau t) (subst tau u)

However, the last two equations did not hold definitionally, since Agda splits first on vt and then on the Tm argument. This makes the subsequent proof fail.

Everything works fine if I put the last two clauses first, then Agda first splits on the Tm argument and then, only in case var, on vt.

For anyone but the expert this behavior is confusing (see messages on the Agda list).

Can we change Agda to enforce that equations hold definitionally? The exception would of course be partially redundant clauses such as default cases, they can not hold definitionally. But it should be visible in the syntax that a clause is not a definitional equality, to get WYSIWYG. One way is to require permission by the user to split a variable that is not an implicit or underscore.

For instance,

max zero n = n max m zero = m max (suc m) (suc n) = suc (max m n)

could be rejected by Agda since no case tree has this behavior, definitionally. One would have to give a strictness annotation to either n or m in the first two equations:

max zero !n = n max m zero = m max (suc m) (suc n) = suc (max m n)

This variant would enforce to first split on n and only in the successor case split on m, to preserve reduction behavior for the second equation.

It is then clear to the user that the first equation does not always hold but rather is only an abbreviation for

max zero (suc n) = suc n

Comments?

Attachment: ParallelSubstitution.agda

Original issue: http://code.google.com/p/agda/issues/detail?id=408

[UlfNorell]

From nils.anders.danielsson on April 22, 2011 04:05:09

This proposal is rather vague. For instance, what happens if a clause contains several exclamation marks?

I agree that Agda's notation can be hard to understand. Epigram's notation is easy to understand, but has the disadvantage that it is verbose, and this can make it harder to get an overview over large definitions. Your suggestion to use Agda's current notation in simple cases and something more explicit in other cases seems like a good compromise.

Cc: -nils.anders.danielsson

[UlfNorell]

From andreas....@gmail.com on April 22, 2011 12:22:29

I agree that the proposal is a bit vague. An exclamation mark before a variable is just a permission to split, it does not have to be executed. Basically, I want some visual evidence in the source code that reduction behavior of clauses is not guaranteed.

[UlfNorell]

From ulf.nor...@gmail.com on September 03, 2011 00:55:55

Labels: Priority-Medium

[UlfNorell]

From andreas....@gmail.com on October 04, 2012 01:34:40

Here is an example from Ulf where split order matters: The classic lookup function for vectors can be defined with two different argument orders, leading to a different set of covering clauses:

-- splitting on the Fin does not require the absurd clause lookup : {A : Set}{n : ℕ} → Fin n → Vec A n → A lookup zero (a ∷ as) = a lookup (suc i) (a ∷ as) = lookup i as

-- splitting on the Vec does require an absurd clause !! : {A : Set}{n : ℕ} → Vec A n → Fin n → A [] !! () (a ∷ as) !! zero = a (a ∷ as) !! (suc i) = as !! i

Some idea how to improve the split heuristics:

Try to predict whether splitting on an argument will lead to a cover.

In lookup, splitting on Vec does not lead to a cover

• because split type Vec A n is free (all constructors possible)
• clauses cover only constructor ∷

In lookup, splitting on Fin may lead to a cover

• because all constructors are covered

==> prioritize Fin over Vec

Status: Accepted

[UlfNorell]

From andreas....@gmail.com on October 13, 2012 13:44:47

The stuff of comment 4 is implemented. On AIM XVI we also discussed a modification of the split strategy that would make the following pass:

max : Nat → Nat → Nat max (suc n) (suc m) = suc (max n m) max 0 (suc m) = suc m max n 0 = n

testmax3 : {n : Nat} → max n 0 ≡ n testmax3 = refl

It would refer splitting on arugments that have all-constructor matches. Thus it would prefer splitting on the second argument (suc, suc, 0) over the first argument (suc, 0, variable n). However, there are example where this does not lead to success. Here is a shortened example taken from Data.AVL:

data ∼ : ℕ → ℕ → Set where pr : ∀ {n} → suc n ∼ n eq : ∀ {n} → n ∼ n

max : ∀ {m n} → m ∼ n → ℕ max (pr {n}) = suc n max (eq {n}) = n

data Tree : ℕ → Set where node : ∀ {hˡ hʳ} (bal : hˡ ∼ hʳ) → Tree (max bal)

test : ∀ {hˡ hʳ} → Tree hˡ → hˡ ∼ hʳ → Set test (node pr) pr = ℕ test (node eq) pr = ℕ test x eq = ℕ

Splitting first on the second argument makes a split on the first argument impossible, because it leads to the unification problem:

max bal = suc h^r

Agda gives up on this. Splitting on the first argument succeeds, since the problem

max bal = h^l

can be solved by an instantiation of flexible variable h^l.

Well, I have changed the coverage...clause-compilation pipeline such that we can implement new split strategies easily. However, I am afraid that without backtracking we cannot improve over the as-is.

Cc: nils.anders.danielsson
Labels: Coverage

[UlfNorell]

From ulf.nor...@gmail.com on October 14, 2012 22:41:41

I think the new strategy is still an improvement. With the old strategy the test example works purely by chance. Swap the order of the argument and it fails. With the new strategy it least we can tell people to use case splits and they'll be fine. Don't use case splits and you're on your own.

[UlfNorell]

From andreas....@gmail.com on November 11, 2013 16:37:53

We should revisit this issue before the release:

1. Should we turn on the new split strategy (currently off)?
2. I still think that catch-all patterns need to stick out syntactically so that it is suggested that the associated equation will not hold definitionally.

Labels: Milestone-2.3.4