The Community for Technology Leaders
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
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
172 ms
(Ver 3.3 (11022016))