[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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/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.
-- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
