[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Yes ! (I would consider it folklore now.) This is explicitly written out, for example, in Wadler's "Call-by-Value is Dual to Call-by-Name", 2003 -- propositions 5.2 and 5.3, page 8 of https://urldefense.com/v3/__https://homepages.inf.ed.ac.uk/wadler/papers/dual/dual.pdf__;!!IBzWLUs!FW5mQvtua1NFPPztYIIgaWEUxhsni5aYR8rRMELFL1q--cmMQj4e3nlcNlMgr8QUrF_0IfYjOd8$ On Sat, Aug 28, 2021 at 11:51 PM Klaus Ostermann < [email protected]> wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > In classical logic, implication A -> B can be encoded as (not A \/ B). > > Is there any work on how that encoding works on the term side of things, > that is, how > to encode lambda abstraction and application in terms of these logical > connectives. > For instance, there are variants of Parigot's lambda mu calculus with > primitive disjunction > and negation (such as by Pym, Ritter and Wallen or de Groote (2001) ). > Shouldn't it > be possible to remove implication / lambda from such calculi and encode > them as macros? > Has this been done? > > Regards, > > Klaus > > >
