2016 10th International Symposium on Theoretical Aspects of Software Engineering (TASE) (2016)

Shanghai, China

July 17, 2016 to July 19, 2016

ISBN: 978-1-5090-1765-2

pp: 113-116

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TASE.2016.25

ABSTRACT

Substitution in the λ-calculus is a subtle operation. In a formal description, Barendregt's variable convention isassumed to avoid variable capture, but such an assumption is notwell suited for implementation on computers. We introduce graphrepresentation and manipulation of λ-terms, in which bound andfree variables are encoded by using hyperlinks with differentattributes. A graph type called hlground is generalized to identifythe scope of a term n in substitution m[x:= n], which enablesbound variables and free variables to have suitable behaviorduring the substitution. Our representation of the λ-terms arereadable and the definition of substitution in this technique isfree from any side conditions on the freeness and freshness of variables.

INDEX TERMS

Syntactics, Electronic mail, Computers, Computer languages, Concrete, Software engineering,graph types, ?-terms, substitution, hypergraphs

CITATION

Alimujiang Yasen,
Kazunori Ueda,
"Hypergraph Representation of Lambda-Terms",

*2016 10th International Symposium on Theoretical Aspects of Software Engineering (TASE)*, vol. 00, no. , pp. 113-116, 2016, doi:10.1109/TASE.2016.25