##
**Unification under a mixed prefix.**
*(English)*
Zbl 0768.68067

Summary: Unification problems are identified with conjunctions of equations between simply typed \(\lambda\)-terms where free variables in the equations can be universally or existentially quantified. Two schemes for simplifying quantifier alternation, called Skolemization and raising (a dual of Skolemization), are presented. In this setting where variables of functional type can be quantified and not all types contain closed terms, the naive generalization of first order Skolemization has several technical problems that are addressed. The method of searching for pre- unifiers described by Huet is easily extended to the mixed prefix setting, although solving flexible-flexible unification problems is undecidable since types may be empty. Unification problems may have numerous incomparable unifiers. Occasionally, unifiers share common factors and several of these are presented. Various optimizations on the general unification search problem are as discussed.

### MSC:

68W30 | Symbolic computation and algebraic computation |

03B15 | Higher-order logic; type theory (MSC2010) |

03B35 | Mechanization of proofs and logical operations |

### Keywords:

conjunctions of equations between simply typed \(\lambda\)-terms; quantifier alternation; Skolemization; raising; mixed prefix; unification; unifiers### Software:

Elf
Full Text:
DOI

### References:

[1] | Andrews, P., Resolution in type theory, Journal of symbolic logic, 36, 414-432, (1971) · Zbl 0231.02038 |

[2] | Andrews, P., General models and extensionality, Journal of symbolic logic, 37, 395-397, (1972) · Zbl 0264.02050 |

[3] | Andrews, P.; Cohn, E.; Miller, D.; Pfenning, F., Automating higher order logic, (), 169-192 |

[4] | Andrews, P., An introduction to mathematical logic and type theory, (1986), Academic Press |

[5] | Church, A., A formulation of the simple theory of types, Journal of symbolic logic, 5, 56-68, (1940) · JFM 66.1192.06 |

[6] | Elliott, C.; Pfenning, F., Higher-order abstract syntax, (), 199-208 |

[7] | Elliott, C., Higher-order unification with dependent types, (), 121-136 |

[8] | Farmer, W., Length of proofs and unification theory, () |

[9] | Felty, A.; Miller, D., Specifying theorem provers in a higher-order logic programming language, (), 61-80 |

[10] | Felty, A., Specifying and implementing theorem provers in a higher-order logic programming language, () · Zbl 0645.68097 |

[11] | Goldfarb, W., The undecidability of the second-order unification problem, Theoretical computer science, 13, 225-230, (1981) · Zbl 0457.03006 |

[12] | Hannan, J.; Miller, D., Uses of higher-order unification for implementing program transformers, (), 942-959 |

[13] | Hannan, J.; Miller, D., A meta language for functional programs, () |

[14] | Henkin, L., Completeness in the theory of types, Journal of symbolic logic, 15, 81-91, (1950) · Zbl 0039.00801 |

[15] | Hindley, J.; Seldin, J., Introduction to combinators and λ-calculus, (1986), Cambridge University Press · Zbl 0614.03014 |

[16] | Huet, G., The undecidability of unification in third order logic, Information and control, 22, 257-267, (1973) · Zbl 0257.02038 |

[17] | Huet, G., A mechanization of type theory, (), 139-146 |

[18] | Huet, G., A unification algorithm for type λ-calculus, Theoretical computer science, 1, 27-57, (1975) · Zbl 0337.68027 |

[19] | Huet, G.; Lang, B., Proving and applying program transformations expressed with second-order patterns, Acta informatica, 11, 31-55, (1978) · Zbl 0389.68008 |

[20] | Jensen, D.; Pietrzykowski, T., Mechanizing ω-order type theory through unification, Theoretical computer science, 3, 123-171, (1976) · Zbl 0361.02020 |

[21] | Lucchesi, C., The undecidability of the unification problem for third order languages, () |

[22] | Miller, D., A compact representation of proofs, Studia logica, 46/6, 345-368, (1987) |

[23] | Miller, D., Unification of simply typed lambda-terms as logic programming, (), 255-269 |

[24] | Miller, D., A logic programming language with lambdaa-abstraction, function variables, and simple unification, Journal of logic and computation, 2/4, 497-536, (1991) · Zbl 0738.68016 |

[25] | Miller, D.; Nadathur, G., A logic programming approach to manipulating formulas and programs, (), 379-388 |

[26] | Nadathur, G., A higher-order logic as the basis for logic programming, () · Zbl 0900.68129 |

[27] | Nadathur, G.; Miller, D., An overview of λprolog, (), 810-827 |

[28] | Nadathur, G.; Miller, D., Higher-order Horn clauses, Journal of the ACM, 37/4, 777-814, (1990) · Zbl 0711.68091 |

[29] | Paulson, L., Natural deduction as higher-order resolution, Journal of logic programming, 3/3, 237-258, (1986) · Zbl 0613.68035 |

[30] | Paulson, L., The foundation of a generic theorem prover, Journal of automated reasoning, 5, 363-397, (1989) · Zbl 0679.68173 |

[31] | Pfenning, F., Partial polymorphic type inference and higher-order unification, () |

[32] | Pfenning, F., Logic programming in the LF logical framework, (), 149-181 · Zbl 0760.68014 |

[33] | Pietrzykowski, T., A complete mechanization of second-order logic, Journal of the ACM, 20/2, 333-364, (1971) · Zbl 0253.68021 |

[34] | Pietrzykowski, T.; Jensen, D., Mechanizing ω-order type theory through unification, Theoretical computer science, 3, 123-171, (1976) · Zbl 0361.02020 |

[35] | Pym, D., Proofs, search and computation in general logic, () |

[36] | Snyder, W.; Gallier, J., Higher order unification revisited: complete sets of transformations, Journal of symbolic computation, 8/1-2, 101-140, (1989) · Zbl 0682.03034 |

[37] | Statman, R., Intuitionistic propositional logic is polynomial-space complete, Theoretical computer science, 9, 67-72, (1979) · Zbl 0411.03049 |

[38] | Statman, R., On the existence of closed terms in the typed λ-calculus II: transformations of unification problems, Theoretical computer science, 15, 329-338, (1981) · Zbl 0486.03011 |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.