[Agda] [TYPES] Progress + Preservation = Evaluation

[Philip Wadler]

Thanks, Sam and Andreas, for the elegant examples of how to encode general
recursion in a language that guarantees termination. Sam, am I right in
thinking Conor's paper does not touch on the idea of combining constructive
proofs of progress and preservation to derive a constructive evaluator?
(But I could apply Conor's technique or a trampoline to express such an
evaluator. Indeed, I considered using Delay for the evaluator in the
textbook, but decided that supplying a step count was simpler, and avoided
the need to explain coinduction.) 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 19:23, Sam Lindley <Sam.Lindley at ed.ac.uk> wrote:

> You should certainly cite Conor McBride's MPC 2015 paper
> "Turing-Completeness Totally Free":
>
>   https://personal.cis.strath.ac.uk/conor.mcbride/TotallyFree.pdf
>
> Sam
>
> On 06/07/18 17:49, Philip Wadler wrote:
>
>> [ The Types Forum, http://lists.seas.upenn.edu/ma
>> ilman/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.
>>
>>
> --
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180706/c6209a70/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180706/c6209a70/attachment.ksh>