Abstract
We investigate the relationship between finite terms in lambdaletrec, the lambda calculus with letrec, and the infinite lambda terms they express. We say that a lambdaletrec term expresses a lambda term if the latter can be obtained as an infinite unfolding of the former. Unfolding is the process of substituting occurrences of function variables by the righthand side of their definition.
We consider the following questions:
(i) How can we characterise those infinite lambda terms that are lambdaletrecexpressible?
(ii) given two lambdaletrec terms, how can we determine whether they have the same unfolding?
(iii) given a lambdaletrec term, can we find a more compact version of the term with the same unfolding?
To tackle these questions we introduce and study the following formalisms:
 a rewriting system for unfolding lambdaletrec terms into lambda terms
 a rewriting system for `observing' lambda terms by dissecting their term structure
 higherorder and firstorder graph formalisms together with translations between them as well as translations from and to lambdaletrec
We identify a firstorder term graph formalism on which bisimulation preservesand reflects the unfolding semantics of lambdaletrec and which is closed under functional bisimulation. From this we derive efficient methods to determine whether two terms are equivalent under infinite unfolding and to compute the maximally shared form of a given lambdaletrec term.
We consider the following questions:
(i) How can we characterise those infinite lambda terms that are lambdaletrecexpressible?
(ii) given two lambdaletrec terms, how can we determine whether they have the same unfolding?
(iii) given a lambdaletrec term, can we find a more compact version of the term with the same unfolding?
To tackle these questions we introduce and study the following formalisms:
 a rewriting system for unfolding lambdaletrec terms into lambda terms
 a rewriting system for `observing' lambda terms by dissecting their term structure
 higherorder and firstorder graph formalisms together with translations between them as well as translations from and to lambdaletrec
We identify a firstorder term graph formalism on which bisimulation preservesand reflects the unfolding semantics of lambdaletrec and which is closed under functional bisimulation. From this we derive efficient methods to determine whether two terms are equivalent under infinite unfolding and to compute the maximally shared form of a given lambdaletrec term.
Original language  English 

Awarding Institution 

Supervisors/Advisors 

Award date  20 Jun 2016 
Publisher  
Publication status  Published  20 Jun 2016 
Keywords
 lambda
 calculus
 letrec
 unfolding
 semantics
 infinite
 subterm
 sharing
 bisimulation
 graph