Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I added to excluded middle a discussion of the constructive proof of double-negated LEM and how it is a sort of “continuation-passing” transform.
We have a stub entry continuation-passing style. I have now made “continuation-passing” redirect to it, so that one more of your links points somewhere.
Thanks!
My coding skills are so bad. It would be good to have one example at least at continuation-passing style, but I can’t read even that first simple pyth program at the wikipedia page.
The connection between the double-negation translation and the continuation-passing transform is indeed quite intriguing! Also note that, while there is only one transformation on propositions/types, there are actually a few variants of the transformation on proofs/terms, corresponding to the different kinds of the continuation-passing transform.
David, the key idea is the following. Ordinarily, you call a subroutine/procedure/function and it returns to you some result:
y = f(x).
In contrast, if you employ continuation-passing style, then subroutines never return. Instead, when calling a subroutine, you pass an additional argument (a so-called continuation). This argument is itself a subroutine; it expects the result of the computation as its argument:
$f(x, (y \mapsto \cdots)).$ $f(x, \lambda y. \cdots).$The continuation-passing transform is a mechanical procedure which transforms a program written in direct style into the equivalent program written in continuation-passing style.
I have some slides on this material; but they are directed at a general computer science audience. Therefore they explain intuitionistic logic, but not continuations.
These are nice slides of yours. I have now referenced them here.
Yes, great slides.
I’m slowly getting there with continuation-passing. The naive factorial example here helped.
added publication data for
added also pointer to
{#Diaconescu75} Radu Diaconescu, Axiom of choice and complementation, Proceedings of the American Mathematical Society 51:176-178 (1975) (doi:10.1090/S0002-9939-1975-0373893-X)
{#GoodmanMyhill78} N. D. Goodman J. Myhill, Choice Implies Excluded Middle, Zeitschrift fuer Mathematische Logik und Grundlagen der Mathematik 24:461 (1978)
And then I added pointer to a stand-alone entry Diaconescu-Goodman-Myhill theorem, which I am splitting off so that we may disambiguate from Diaconscu’s theorem
1 to 8 of 8