Abstract
Automated deduction in higherorder program calculi, where properties of transformation rules are demanded, or confluence or other equational properties are requested, can often be done by syntactically computing overlaps (critical pairs) of reduction rules and transformation rules. Since higherorder calculi have alphaequivalence as fundamental equivalence, the reasoning procedure must deal with it. We define ASD1unification problems, which are higherorder equational unification problems employing variables for atoms, expressions and contexts, with additional distinctvariable constraints, and which have to be solved w.r.t. alphaequivalence. Our proposal is to extend nominal unification to solve these unification problems. We succeeded in constructing the nominal unification algorithm NomUnifyASD. We show that NomUnifyASD is sound and complete for this problem class, and outputs a set of unifiers with constraints in nondeterministic polynomial time if the final constraints are satisfiable. We also show that solvability of the output constraints can be decided in NEXPTIME, and for a fixed number of contextvariables in NP time. For terms without contextvariables and atomvariables, NomUnifyASD runs in polynomial time, is unitary, and extends the classical problem by permitting distinctvariable constraints.
BibTeX  Entry
@InProceedings{schmidtschau_et_al:LIPIcs:2018:9198,
author = {Manfred SchmidtSchau{\ss} and David Sabel},
title = {{Nominal Unification with Atom and Context Variables}},
booktitle = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
pages = {28:128:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959770774},
ISSN = {18688969},
year = {2018},
volume = {108},
editor = {H{\'e}l{\`e}ne Kirchner},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2018/9198},
URN = {urn:nbn:de:0030drops91983},
doi = {10.4230/LIPIcs.FSCD.2018.28},
annote = {Keywords: automated deduction, nominal unification, lambda calculus, functional programming}
}
Keywords: 

automated deduction, nominal unification, lambda calculus, functional programming 
Collection: 

3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018) 
Issue Date: 

2018 
Date of publication: 

04.07.2018 