TY - JOUR

T1 - Name binding is easy with hypergraphs

AU - Yasen, Alimujiang

AU - Ueda, Kazunori

N1 - Funding Information:
The authors are indebted to anonymous referees for their careful reading, useful comments and pointers to the literature. This work is partially supported by Grant-In-Aid for Scientific Research ((B) 26280024), JSPS, Japan.

PY - 2018/4

Y1 - 2018/4

N2 - We develop a technique for representing variable names and name binding which is a mechanism of associating a name with an entity in many formal systems including logic, programming languages and mathematics. The idea is to use a general form of graph links (or edges) called hyperlinks to represent variables, graph nodes as constructors of the formal systems, and a graph type called hlground to define substitutions. Our technique is based on simple notions of graph theory in which graph types ensure correct substitutions and keep bound variables distinct. We encode strong reduction of the untyped λ-calculus to introduce our technique. Then we encode a more complex formal system called System F<:, a polymorphic λ-calculus with subtyping that has been one of important theoretical foundations of functional programming languages. The advantage of our technique is that the representation of terms, definition of substitutions, and implementation of formal systems are all straightforward. We formalized the graph type hlground, proved that it ensures correct substitutions in the λ-calculus, and implemented hlground in HyperLMNtal, a modeling language based on hypergraph rewriting. Experiments were conducted to test this technique. By this technique, one can implement formal systems simply by following the steps of their definitions as described in papers.

AB - We develop a technique for representing variable names and name binding which is a mechanism of associating a name with an entity in many formal systems including logic, programming languages and mathematics. The idea is to use a general form of graph links (or edges) called hyperlinks to represent variables, graph nodes as constructors of the formal systems, and a graph type called hlground to define substitutions. Our technique is based on simple notions of graph theory in which graph types ensure correct substitutions and keep bound variables distinct. We encode strong reduction of the untyped λ-calculus to introduce our technique. Then we encode a more complex formal system called System F<:, a polymorphic λ-calculus with subtyping that has been one of important theoretical foundations of functional programming languages. The advantage of our technique is that the representation of terms, definition of substitutions, and implementation of formal systems are all straightforward. We formalized the graph type hlground, proved that it ensures correct substitutions in the λ-calculus, and implemented hlground in HyperLMNtal, a modeling language based on hypergraph rewriting. Experiments were conducted to test this technique. By this technique, one can implement formal systems simply by following the steps of their definitions as described in papers.

KW - Formal systems

KW - Graph type

KW - Hypergraph rewriting

KW - Name binding

KW - Substitution

UR - http://www.scopus.com/inward/record.url?scp=85044782736&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85044782736&partnerID=8YFLogxK

U2 - 10.1587/transinf.2017EDP7257

DO - 10.1587/transinf.2017EDP7257

M3 - Article

AN - SCOPUS:85044782736

VL - E101D

SP - 1126

EP - 1140

JO - IEICE Transactions on Information and Systems

JF - IEICE Transactions on Information and Systems

SN - 0916-8532

IS - 4

ER -