HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

Positive and negative results for higher-order disunification

Denis Lugiez 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : This paper is devoted to higher-order disunification which is the process of solving quantified formulae built on simply-typed lambda-terms, the equality induced by the $\eta$ and the $\beta$ reductions, boolean connectives and the negation. This problem is motivated by tests of completeness of definitions in algebraic higher-order specification languages which combine the advantages of algebraic specification languages and higher-order programming languages. We show that higher-order disunification is not semi-decidable and we prove the undecidability of second-order complement problems which are the formulae expressing the completeness of some scheme, by encoding Minsky machines. On the other hand, we show that second-order complement problems are decidable if second-order variables and bound variables satisfy some (reasonable) conditions and that the validity of any quantified equational formula can be checked when all the terms occurring in this formula are patterns, i.e. s.t. the arguments of free variables are distinct bound variables. Both cases are decided using quantifier elimination techniques.
Document type :
Complete list of metadata

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 2:42:02 PM
Last modification on : Friday, February 4, 2022 - 3:22:35 AM
Long-term archiving on: : Tuesday, April 12, 2011 - 3:50:39 PM


  • HAL Id : inria-00074183, version 1



Denis Lugiez. Positive and negative results for higher-order disunification. [Research Report] RR-2492, INRIA. 1995, pp.36. ⟨inria-00074183⟩



Record views


Files downloads