[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Hi, I think this is now well known as the "fuel" pattern. Ideally n is very big and computed lazily. I am not aware of a paper specifically about this trick, it is there as a very useful folklore I guess. Note however that Bertot Balaa presented a more "complete" version of this by refining this trick: the function itself is defined by means of a proof that there exists a number N of iterations such that any greater number would give the same result. i.e. that N is a sufficient fuel to reach the fixpoint. This mechanism is used in the current implementation of the "Function" command in coq (when given a non structurally recursive function). http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.28.601&rep=rep1&type=pdf Best, Pierre Le ven. 6 juil. 2018 à 21:28, Philip Wadler <[email protected]> a écrit : > > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Everyone on this list will be familiar with Progress and Preservation > for terms in a typed calculus. Write ∅ ⊢ M : A to indicate that term > M has type A for closed M. > > Progress. If ∅ ⊢ M : A then either M is a value or M —→ N, > for some term N. > > Preservation. If ∅ ⊢ M : A and M —→ N then ∅ ⊢ N : A. > > It is easy to combine these two proofs into an evaluator. > Write —↠ for the transitive and reflexive closure of —→. > > Evaluation. If ∅ ⊢ M : A, then for every natural number n, > either M —↠ V, where V is a value and the reduction sequence > has no more than n steps, or M —↠ N, where N is not a value > and the reduction sequence has n steps. > > Evaluation implies that either M —↠ V or there is an infinite > sequence M —→ M₁ —→ M₂ —→ ... that never reduces to a value; > but this last result is not constructive, as deciding which of > the two results holds is not decidable. > > An Agda implementation of Evaluation provides an evaluator for terms: > given a number n it will perform up to n steps of evaluation, stopping > early if a value is reached. This is entirely obvious (at least in > retrospect), but I have not seen it written down anywhere. For > instance, this approach is not exploited in Software Foundations to > evaluate terms (it uses a normalize tactic instead). I have used it > in my draft textbook: > > https:plfa.inf.ed.ac.uk > > Questions: What sources in the literature should one cite for this > technique? How well-known is it as folklore? Cheers, -- P > > > . \ Philip Wadler, Professor of Theoretical Computer Science, > . /\ School of Informatics, University of Edinburgh > . / \ and Senior Research Fellow, IOHK > . http://homepages.inf.ed.ac.uk/wadler/ > > Too brief? Here's why: http://www.emailcharter.org/ > The University of Edinburgh is a charitable body, registered in > Scotland, with registration number SC005336.
