Talk:Lambda-mu calculus

non-contradiction

The law of non contradiction is intuitionistically valid: if not(p) is defined as p -> False, then there is an easy proof of not(p/\not(p)). The reference to this property should probably be replaced with a reference to the excluded middle... User:82.244.102.132 14:42, 29 January 2011‎

TODO List

Some "interesting" things this article could mention and elaborate on:

• Lamda-mu and relation to "call-by-name", or rather, explain how a call-by-name beta-reduction strategy gets us to here.
• Call-by-value is Dual to Call-by-name, Reloaded
• There seems to be a typed version of lambda-mu...
• And its claimed that lambda-Delta (upper-case Delta) is a simpler, easier, better version of typed lambda-mu. Its easier to read.
• This article should give specific examples of natural deduction, and show how they work out in lambda-mu
• For typed lambda-mu, the types are in 1-1 correspondence with propositions, or something like that. Examples would be nice.

67.198.37.16 (talk) 21:07, 19 December 2017 (UTC)

More ToDo: Simplifications

Another item that may be added on the to do list is to incorporate the simplifications described in Streicher & Reus, "Classical logic, continuation semantics and abstract machines" (J. Functional Programming 8 (6): 543-572), to replace the awkward substitution rule by a simple substitution. The simplification consists of the following: (1) continuations [q]w may list embedded contexts, q = u∷⋯∷v∷α, rather than simple continuation variables α, (2) products fold into continuations [q](uv) = [v∷q]u. Then, (3) structural reduction simplifies to a form (μβ.u)v → u[v∷β/β] that involves simple substitution and (4) renaming generalizes to a form [q]μβ.u → u[q/β], that allows substitution with general contexts q = u∷⋯∷v∷α, instead of just with context variables α.