Abstract
We present here a particular case of the higher order matching problem — the linear interpolation problem. The problem consists in solving a collection of higher order matching equations of the shape xM 1 ... M k = N, where x is the only unknown quantity. We prove recursive equivalence of the higher order matching problem and the linear interpolation problem. We also investigate decidability of a special case of the fifth order linear interpolation problem. The restriction we consider consists in that arguments of variables from the main abstraction in terms M 1,..., M k cannot contain variables from the main abstraction.
This work has been partly supported by ESPRIT BRA 7232 GENTZEN, and KBN 8 T11C 034 10 grants.
Chapter PDF
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
H.P. Barendregt, The lambda calculus, its syntax and semantics, 2 ed., North Holland, 1984.
H.P. Barendregt, Lambda calculi with types, Handbook of Logic in Computer Science (S. Abramsky, D.M. Gabbay, and T.S.E. Maibaum, eds.), vol. 2, Oxford Science Publications, 1992, pp. 117–309.
G. Dowek, Third order matching is decidable, Annals of Pure and Applied Logic (1993).
B. Lang G. Huet, Proving and applying program transformations expressed with second order patterns, Acta Informatica (1978), no. 11, 31–55.
G. Huet, Résolution d'équations dans les languages d'ordre 1, 2, ..., Ω., Ph.D. thesis, Université Paris VII, 1976.
Vincent Padovani, Filtrage d'ordre superieur, Ph.D. thesis, Université Paris VII, January 1996.
Aleksy Schubert, Linear interpolation for the higher-order matching problem, Tech. Report TR 96-16 (237), Institute of Informatics Warsaw University, December 1996.
D.A. Wolfram, The clausal theory of types, Ph.D. thesis, University of Cambridge, 1989.
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Schubert, A. (1997). Linear interpolation for the higher-order matching problem. In: Bidoit, M., Dauchet, M. (eds) TAPSOFT '97: Theory and Practice of Software Development. CAAP 1997. Lecture Notes in Computer Science, vol 1214. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0030617
Download citation
DOI: https://doi.org/10.1007/BFb0030617
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62781-4
Online ISBN: 978-3-540-68517-3
eBook Packages: Springer Book Archive