Hostname: page-component-74656f9884-2dmjx Total loading time: 0 Render date: 2026-11-09T03:57:53.382Z Has data issue: false hasContentIssue false

Decidability of fourth-order matching

Published online by Cambridge University Press:  01 June 2000

VINCENT PADOVANI
Affiliation:
Université PARIS VII-C.N.R.S U.R.A. 753, Equipe Preuves, Programmes et Systèmes, 2 Place Jussieu 75251 PARIS CEDEX 05 FRANCE. Email: padovani@pps.jussieu.fr
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

Higher Order Matching consists of solving finite sets of equations of the form u =βηv, where u, v are simply typed terms of λ-calculus, and v is a closed term. Whether this problem is decidable is an open question. In this paper its decidability is proved when the free variables of all equations are of order at most 4 – we actually extend this result to a more general situation in which in addition to equations, disequations are also considered.

Information

Type
Research Article
Copyright
2000 Cambridge University Press