Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

There are several ways to encode λ-terms in interaction nets; for instance, using the original optimal algorithm by Lamping, or compiling λ-calculus into interaction combinators. However, all the encodings we know implement only β-reduction, and not extensional λ-calculus (with η-reduction as well).

Is it possible to encode λ-terms into interaction nets implementing βη-reduction?

(The normal form of a net for a term should correspond to the βη-normal form of the term if any.)

share|improve this question
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Browse other questions tagged or ask your own question.