TY - GEN
T1 - Unification of hypergraph λ-terms
AU - Yasen, Alimujiang
AU - Ueda, Kazunori
N1 - Funding Information:
Acknowledgement. The authors are indebted to anonymous referees for their useful comments and pointers to the literature. This work is partially supported by Grant-In-Aid for Scientific Research ((B)26280024), JSPS, Japan, and Waseda University Grant for Special Research Projects.
Publisher Copyright:
© 2017, IFIP International Federation for Information Processing.
PY - 2017
Y1 - 2017
N2 - 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 λ-calculus and the evaluation and type checking of System F<:, but the encoding of System F<: type inference requires a unification algorithm. We studied and successfully implemented a unification algorithm modulo α-equivalence for hypergraphs representing untyped λ-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 α-equivalence.
AB - 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 λ-calculus and the evaluation and type checking of System F<:, but the encoding of System F<: type inference requires a unification algorithm. We studied and successfully implemented a unification algorithm modulo α-equivalence for hypergraphs representing untyped λ-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 α-equivalence.
UR - http://www.scopus.com/inward/record.url?scp=85032483720&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85032483720&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-68953-1_9
DO - 10.1007/978-3-319-68953-1_9
M3 - Conference contribution
AN - SCOPUS:85032483720
SN - 9783319689524
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 106
EP - 124
BT - Topics in Theoretical Computer Science - 2nd IFIP WG 1.8 International Conference, TTCS 2017, Proceedings
A2 - Mousavi, Mohammad Reza
A2 - Sgall, Jirí
PB - Springer Verlag
T2 - 2nd IFIP WG 1.8 International Conference on Topics in Theoretical Computer Science, TTCS 2017
Y2 - 12 September 2017 through 14 September 2017
ER -