Talk:Rippling

I started this page because there doesn't seem to be an existing one describing the rippling heuristic. It needs expanding a lot with examples and a detailed exposition of the technique DPMulligan 14:35, 22 December 2006 (UTC)

Need to discuss how measure is calculated, and expand example to demonstrate how the ripple steps decrease the standard ripple measure. DPMulligan (talk) 14:35, 9 April 2008 (UTC)

In the example, "$\Longrightarrow$" seems to mean "logically implies" at first glance. If, however, "rewrites to" is its intended meaning, a different arrow (e.g. "Failed to parse (unknown function "\leadsto"): {\displaystyle \leadsto} ") should be used instead, and/or its meaning should be mentioned explicit somewhere.

I got confused about the 1st vs. 2nd annotated rewrite rule: while the former works on a proposition (about two terms being equal), the latter works on a term. Is this mix really ok?!

I can't imagine where the 1st rule could originate from, anyway. Wouldn't the injectivity of $Suc$ rather be formalized as "$Suc(x)=Suc(y)\Rightarrow x=y$" or "Failed to parse (unknown function "\leadsto"): {\displaystyle Suc(x)=Suc(y) \leadsto x=y} " ?

The rippling rules could be numbered, and each rippling proof step cound be annotated by the number of the applied rule, to make it easier to understand. Maybe, it would be even more helpful to have the terms drawn as trees, to see how the wave-fronts move up and out.

In any case, the markings for both skeleton (currently "\underline") and wavefront (currently "\fbox") should be explained explicitly, as should be the meaning of "$\uparrow$".

The term "apply fertilization" is induction-prover-expert-speak for "apply the induction hypothesis", I guess?

Jochen Burghardt (talk) 18:47, 23 May 2013 (UTC)

Copyright?

The article contains text taken almost verbatim from http://dream.inf.ed.ac.uk/projects/ripple-faq.html 82.81.55.162 (talk) 21:58, 15 June 2017 (UTC)