Name binding is easy with hypergraphs

Alimujiang Yasen, Kazunori Ueda

    Research output: Contribution to journalArticle

    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.

    Original languageEnglish
    Pages (from-to)1126-1140
    Number of pages15
    JournalIEICE Transactions on Information and Systems
    VolumeE101D
    Issue number4
    DOIs
    Publication statusPublished - 2018 Apr 1

    Fingerprint

    Substitution reactions
    Computer programming languages
    Functional programming
    Logic programming
    Graph theory
    Experiments

    Keywords

    • Formal systems
    • Graph type
    • Hypergraph rewriting
    • Name binding
    • Substitution

    ASJC Scopus subject areas

    • Software
    • Hardware and Architecture
    • Computer Vision and Pattern Recognition
    • Electrical and Electronic Engineering
    • Artificial Intelligence

    Cite this

    Name binding is easy with hypergraphs. / Yasen, Alimujiang; Ueda, Kazunori.

    In: IEICE Transactions on Information and Systems, Vol. E101D, No. 4, 01.04.2018, p. 1126-1140.

    Research output: Contribution to journalArticle

    Yasen, Alimujiang ; Ueda, Kazunori. / Name binding is easy with hypergraphs. In: IEICE Transactions on Information and Systems. 2018 ; Vol. E101D, No. 4. pp. 1126-1140.
    @article{f87fe6ad5b6946f7a62afc8b504277ce,
    title = "Name binding is easy with hypergraphs",
    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 = "Formal systems, Graph type, Hypergraph rewriting, Name binding, Substitution",
    author = "Alimujiang Yasen and Kazunori Ueda",
    year = "2018",
    month = "4",
    day = "1",
    doi = "10.1587/transinf.2017EDP7257",
    language = "English",
    volume = "E101D",
    pages = "1126--1140",
    journal = "IEICE Transactions on Information and Systems",
    issn = "0916-8532",
    publisher = "Maruzen Co., Ltd/Maruzen Kabushikikaisha",
    number = "4",

    }

    TY - JOUR

    T1 - Name binding is easy with hypergraphs

    AU - Yasen, Alimujiang

    AU - Ueda, Kazunori

    PY - 2018/4/1

    Y1 - 2018/4/1

    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 -