Name Binding is Easy with Hypergraphs

Alimujiang YASEN; Kazunori UEDA

doi:10.1587/transinf.2017EDP7257

Name Binding is Easy with Hypergraphs

Alimujiang YASEN, Kazunori UEDA

Full Text Views

0

Cite this

Summary :

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.

Publication: IEICE TRANSACTIONS on Information Vol.E101-D No.4 pp.1126-1140

Publication Date: 2018/04/01

Publicized: 2018/01/12

Online ISSN: 1745-1361

DOI: 10.1587/transinf.2017EDP7257

Type of Manuscript: PAPER

Category: Software System

Authors

Alimujiang YASEN
Waseda University
Kazunori UEDA
Waseda University

Keyword

name binding, substitution, hypergraph rewriting, graph type, formal systems

Cite this

Copy

Alimujiang YASEN, Kazunori UEDA, "Name Binding is Easy with Hypergraphs" in IEICE TRANSACTIONS on Information, vol. E101-D, no. 4, pp. 1126-1140, April 2018, doi: 10.1587/transinf.2017EDP7257.
Abstract: 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.
URL: https://global.ieice.org/en_transactions/information/10.1587/transinf.2017EDP7257/_p

Copy

@ARTICLE{e101-d_4_1126,
author={Alimujiang YASEN, Kazunori UEDA, },
journal={IEICE TRANSACTIONS on Information},
title={Name Binding is Easy with Hypergraphs},
year={2018},
volume={E101-D},
number={4},
pages={1126-1140},
abstract={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.},
keywords={},
doi={10.1587/transinf.2017EDP7257},
ISSN={1745-1361},
month={April},}

Copy

TY - JOUR
TI - Name Binding is Easy with Hypergraphs
T2 - IEICE TRANSACTIONS on Information
SP - 1126
EP - 1140
AU - Alimujiang YASEN
AU - Kazunori UEDA
PY - 2018
DO - 10.1587/transinf.2017EDP7257
JO - IEICE TRANSACTIONS on Information
SN - 1745-1361
VL - E101-D
IS - 4
JA - IEICE TRANSACTIONS on Information
Y1 - April 2018
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.
ER -