Interaction System and Encoding for MLC
Apr. 2nd, 2015 09:48 pmhttps://www.scribd.com/doc/260727360
The goal of our Macro Lambda Calculus project (MLC) is to encode λ-terms into interaction nets. Its software implementation will accept input in the notation similar to λ-calculus allowing macro definitions. Output is similar to interaction calculus and is suitable for our Interaction Nets Compiler program (INC). In this paper, we describe the interaction system for call-by-need evaluation and the mechanism of encoding λ-terms into this system which MLC is based on.
(The paper provides formal definition for the interaction system and encoding of λ-terms that were previously successfully tested for Y (K M) = M using INC.)
The goal of our Macro Lambda Calculus project (MLC) is to encode λ-terms into interaction nets. Its software implementation will accept input in the notation similar to λ-calculus allowing macro definitions. Output is similar to interaction calculus and is suitable for our Interaction Nets Compiler program (INC). In this paper, we describe the interaction system for call-by-need evaluation and the mechanism of encoding λ-terms into this system which MLC is based on.
(The paper provides formal definition for the interaction system and encoding of λ-terms that were previously successfully tested for Y (K M) = M using INC.)
