2016 10th International Symposium on Theoretical Aspects of Software Engineering (TASE) (2016)
July 17, 2016 to July 19, 2016
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TASE.2016.25
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.
Syntactics, Electronic mail, Computers, Computer languages, Concrete, Software engineering,graph types, ?-terms, substitution, hypergraphs
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