Unfolding and Rewriting [Re: [Agda] Bounties for Agda features]

[Andreas Abel]

On 08.05.12 9:10 PM, Daniel Peebles wrote:
> That could be a good start, but ultimately it'd be nice to have
> better user-specified control over it, somehow.

Ok, do you have an idea how that should look like?  Coq, e.g., has the
"unfold" tactic (or was it "expand", cannot remember).

In Agda, an "unfold" has no significance and would leave no trace in the
file, it would be a temporary change of the proof state, maybe.

> In the categories library there are pretty much no constructors or
> pattern matching anywhere but many definitions expand to more
> complicated definitions that will often

But would that not be prevented by my proposal?  If no pattern matching
fires, expansion does not bring progress, so it does not happen...

> obscure the proofs (and probably increase memory usage). We currently
>  selectively throw things behind abstract barriers, along with proofs
>  that the abstract terms are equal to their definitions, but that's
> really tedious and far from ideal.

:-(

> One of the more annoying constructor-y situations I've come across is
>  when I use the standard library map function on a term xs (that I
> have not pattern matched on) whose length is (suc ...). Then I end up
> with the replicate in the definition of map producing an extra
> element like f ∷ replicate f ⊛ xs which can be really confusing in a
> larger term.

Certainly, you would not want such partial unfoldings, exposing the
concrete definition of map.

It would be nice if the implementation of a function could be hidden
behind a more abstract reduction interface, like

   map f []        --> []
   map f (x :: xs) --> f x :: map f xs

even if that is not the definition of map.

In general, the state of rewrite rules in Agda is unsatisfactory.  They
cannot be part of an interface, you can only specify them as
propositional equations.  However, these do not fire during reduction,
which makes abstract program development tedious, if not unfeasible.

With rewrite rules as a primitive, we could also have very handy
simplification rules like

   x + 0 --> x

There is tons of literature on rewriting in type theory which we have
not made use of.  Of course, care is called for, since rewriting easily 
destroys termination and confluence.

Cheers,
Andreas


> On Mon, May 7, 2012 at 3:33 PM, Andreas Abel <andreas.abel at ifi.lmu.de
>  <mailto:andreas.abel at ifi.lmu.de>> wrote:
>
> On 07.05.12 7:06 PM, Daniel Peebles wrote:
>
> *Come up with a neat solution to control depth of evaluation
> locally*
>
>
> See http://code.google.com/p/agda/__issues/detail?id=433
> <http://code.google.com/p/agda/issues/detail?id=433>
>
> I see this mostly as an ease-of-use feature, but it might also help
> performance. Basically, often you really don't want terms to
> normalize fully in your goals or context. Some of my proofs have
> goals whose normal forms are thousands (literally) of lines long, so
> the goal output becomes effectively unusable.
>
> Most of the time, I want to work at a higher level of abstraction
> than individual recursively defined functions, and I've already
> proved simple lemmas about them. In those cases, I don't want simple
> definitions to normalize past a certain point, and want to prove
> things about the higher-level expressions.
>
> For example, when I'm writing simple proofs about the algebraic
> properties of operations on the naturals, I might want my definitions
> to normalize, but other times I might not. For example, (1 + x) + ((1
> + y) * (1 + z)) will normalize to the horrible suc (x + suc (z + y *
> suc z)). If I have a proof about the original form, it takes a lot
> of squinting to realize that the normal form applies to it.
>
>
> Well, a simple heuristics would be to only unfold definitions when
> making progress, where progress means that a constructor-pattern
> matched and an equation fired.
>
> Unfortunately, that would still destroy your beautiful 1 + x.
>
> However,  Data.List's
>
> any p xs
>
> would not be unfolded to
>
> foldr _v_ false (map p xs).
>
> Which would already be something.


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/