Third order matching is decidable
type: Item
instance of: scholarly article
title: Third order matching is decidable
zbMATH Open document ID: 0822.03010
DOI: 10.1016/0168-0072(94)90083-3
author: Gilles Dowek
published in: Annals of Pure and Applied Logic
publication date: 1994-11-08T00:00:00Z
review text: The matching problem in the simply typed \(\lambda\)-calculus has been shown decidably by Huet in the case of at most second order, but it is open in general. The author shows that it is decidable in the case of third order. The main idea is that if a problem \(a=b\), where \(b\) is ground, has a solution, then it also has a solution whose depth (of Böhm tree) is bounded by some integer depending only on the problem. This is first shown for an interpolation problem as an intermediate stage. The proof is very neatly described.
Mathematics Subject Classification ID: 03B40
Mathematics Subject Classification ID: 03B25
zbMATH DE Number: 683705
zbMATH Keywords: decidability
zbMATH Keywords: matching problem
zbMATH Keywords: simply typed \(\lambda\)-calculus
zbMATH Keywords: third order
zbMATH Keywords: interpolation
reviewed by: Teruo Hikita
MaRDI profile type: Publication
full work available at URL: 0168-0072(94)90083-3
OpenAlex ID: W1988246540
cites work: The lambda calculus, its syntax and semantics
cites work: Q5667469
cites work: Q4722037
cites work: A unification algorithm for typed \(\overline\lambda\)-calculus
cites work: Proving and applying program transformations expressed with second-order patterns
cites work: Unification under a mixed prefix
cites work: Higher-order unification revisited: Complete sets of transformations
cites work: Completeness, invariance and λ-definability
cites work: The Clausal Theory of Types
cites work: Q3708774
description: scientific article; zbMATH DE number 683705