Skip to Main content Skip to Navigation
Conference papers

Unification of Hypergraph $\lambda $-Terms

Abstract : We developed a technique for modeling formal systems involving name binding in a modeling language based on hypergraph rewriting. A hypergraph consists of graph nodes, edges with two endpoints and edges with multiple endpoints. The idea is that hypergraphs allow us to represent terms containing bindings and that our notion of a graph type keeps bound variables distinct throughout rewriting steps. We previously encoded the untyped $\lambda $-calculus and the evaluation and type checking of System $F_\texttt {<:}$, but the encoding of System $F_\texttt {<:}$ type inference requires a unification algorithm. We studied and successfully implemented a unification algorithm modulo $\alpha $-equivalence for hypergraphs representing untyped $\lambda $-terms. The unification algorithm turned out to be similar to nominal unification despite the fact that our approach and nominal approach to name binding are very different. However, some basic properties of our framework are easier to establish compared to the ones in nominal unification. We believe this indicates that hypergraphs provide a nice framework for encoding formal systems involving binders and unification modulo $\alpha $-equivalence.
Document type :
Conference papers
Complete list of metadata

Cited literature [17 references]  Display  Hide  Download

https://hal.inria.fr/hal-01760636
Contributor : Hal Ifip <>
Submitted on : Friday, April 6, 2018 - 3:07:51 PM
Last modification on : Saturday, February 9, 2019 - 9:06:02 PM

File

440117_1_En_9_Chapter.pdf
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

Alimujiang Yasen, Kazunori Ueda. Unification of Hypergraph $\lambda $-Terms. 2nd International Conference on Topics in Theoretical Computer Science (TTCS), Sep 2017, Tehran, Iran. pp.106-124, ⟨10.1007/978-3-319-68953-1_9⟩. ⟨hal-01760636⟩

Share

Metrics

Record views

129

Files downloads

89