[ 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
