Nominal unification of higher order expressions with recursive let

DOI10.1007/978-3-319-63139-4_19MaRDI QIDQ2409747zbMATH OpenOpenAlexFDO

Authors Manfred Schmidt-Schauß, Temur Kutsia, Jordi Levy, Mateu Villaret

Publication date 13 October 2017

Full work available at URL https://arxiv.org/abs/1608.03771

zbMATH Keywords

higher-order expressionslambda calculusnominal unificationoperational semanticsrecursive let

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Analysis of algorithms and problem complexity (68Q25) Grammars and rewriting systems (68Q42) Semantics in the theory of computing (68Q55)

Abstract: A sound and complete algorithm for nominal unification of higher-order expressions with a recursive let is described, and shown to run in non-deterministic polynomial time. We also explore specializations like nominal letrec-matching for plain expressions and for DAGs and determine the complexity of corresponding unification problems.

Recommendations

• Nominal unification with atom-variables
• An efficient nominal unification algorithm
• A polynomial nominal unification algorithm
• Unifying nominal unification

Cited in

(14)

• Nominal unification with atom-variables
• Nominal unification with letrec and environment-variables
• A formalisation of nominal C-matching through unification with protected variables
• A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols
• Fixed-point constraints for nominal equational unification
• Nominal unification with atom and context variables
• Formalising nominal C-unification generalised with protected variables
• Nominal Unification and Matching of Higher Order Expressions with Recursive Let
• A certified functional nominal C-unification algorithm
• On nominal syntax and permutation fixed points
• (Nominal) unification by recursive descent with triangular substitutions
• Nominal AC-matching
• Unranked Nominal Unification
• Nominal anti-unification modulo equational theories

This page was built for publication: Nominal unification of higher order expressions with recursive let

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2409747)