[Agda] [TYPES] Progress + Preservation = Evaluation

[Andreas Abel]

Dear Phil,

to me, deriving an evaluator from preservation & progress resembles a 
use of the

   trampoline : (A -> B + A) -> A -> Delay B

where A would be "well-typed terms" and B "values".

Delay is the coinductive type with coconstructors

   now   : B       -> Delay B
   later : Delay B -> Delay B

trampoline is the coiteration principle for Delay.

For Delay, see Venanzio Capretta.

   https://doi.org/10.2168/LMCS-1(2:1)2005

I don't have a reference for your specific problem.

Best,
Andreas

On 06.07.2018 22:18, Philip Wadler wrote:
> Thanks, Pierre and Eelco. I'm well aware of "fuel" as folklore. For 
> instance, I've heard Conor McBride describe fuel as an argument that, 
> despite the guarantee that all programs terminate, Agda can effectively 
> encode every recursive function. But that is different from my question; 
> please see my second, clarifying email. I had a look at the three 
> references cited, and I don't believe they exploit constructive proofs 
> of progress and preservation to define an evaluator. 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/
> 
> On 6 July 2018 at 17:57, Pierre Courtieu <pierre.courtieu at gmail.com 
> <mailto:pierre.courtieu at gmail.com>> wrote:
> 
>     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
>     <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 <wadler at inf.ed.ac.uk
>     <mailto:wadler at inf.ed.ac.uk>> a écrit :
>     >
>     > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list
>     <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 <http://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/
>     <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.
> 
> 
> 
> 
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
> 
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 


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

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/