Hostname: page-component-586b7cd67f-t7czq Total loading time: 0 Render date: 2024-11-24T17:49:45.527Z Has data issue: false hasContentIssue false
  • English
  • Français

The Church-Rosser property in dual combinatory logic

Published online by Cambridge University Press:  12 March 2014

Katalin Bimbó
Katalin Bimbó*
Affiliation:
Automated Reasoning Group, Csl, Rsise, BLD. #115, Australian National University, Canberra, Act 0200, Australia, E-mail: [email protected], URL: http://arp.anu.edu.au/~bimbo
Get access Rights & Permissions [Opens in a new window]

Abstract

Dual combinators emerge from the aim of assigning formulas containing ← as types to combinators. This paper investigates formally some of the properties of combinatory systems that include both combinators and dual combinators. Although the addition of dual combinators to a combinatory system does not affect the unique decomposition of terms, it turns out that some terms might be redexes in two ways (with a combinator as its head, and with a dual combinator as its head). We prove a general theorem stating that no dual combinatory system possesses the Church-Rosser property. Although the lack of confluence might be problematic in some cases, it is not a problem per se. In particular, we show that no damage is inflicted upon the structurally free logics, the system in which dual combinators first appeared.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 68 , Issue 1 , March 2003 , pp. 132 - 152
Copyright
Copyright © Association for Symbolic Logic 2003

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1]Bimbó, K., Investigation into combinatory systems with dual combinators, Studio Logica, vol. 66 (2000), pp. 285–296.CrossRefGoogle Scholar
[2]Bimbó, K. and Dunn, J. M., Two extensions of the structurally free logic LC, Logic Journal of IGPL, vol. 6 (1998), pp. 403–424.CrossRefGoogle Scholar
[3]Church, A., The calculi of lambda-conversion, 1st ed., Princeton University Press, Princeton, 1941.Google Scholar
[4]Curry, H. B. and Feys, R., Combinatory logic, 1st ed., vol. I, North-Holland, Amsterdam, 1958.Google Scholar
[5]Curry, H. B., Hindley, J. R., and Seldin, J. P., Combinatory logic, vol. II, North-Holland, Amsterdam, 1972.Google Scholar
[6]Dunn, J. M. and Meyer, R. K., Combinatory logic and structurally free logic, Logic Journal of IGPL, vol. 5 (1997), pp. 505–537.CrossRefGoogle Scholar
[7]Hindley, J. R., An abstract form of the Church-Rosser theorem, I, this Journal, vol. 34 (1969), pp. 545–560.Google Scholar
[8]Hindley, J. R. and Seldin, J. P., Introduction to combinators and λ-calculus, Cambridge University Press, Cambridge (UK), 1986.Google Scholar
[9]Kleene, S. C., Proof by cases in formal logic, Annals of Mathematics, vol. 35 (1934), pp. 529–544.CrossRefGoogle Scholar
[10]Lambek, J., From categorial grammar to bilinear logic, Substructural logics (Došen, K. and Schroeder-Heister, P., editors), Clarendon and Oxford University Press, Oxford (UK), 1993, pp. 207–237.CrossRefGoogle Scholar
[11]Meyer, R. K., Bimbó, K., and Dunn, J. M., Dual combinators bite the dust, (abstract). The Bulletin of Symbolic Logic, vol. 4 (1998), pp. 463–464.Google Scholar
[12]Rosen, B. K., Tree-manipulating systems and Church-Rosser theorems, Journal of the Association for Computing Machinery, vol. 20 (1973), pp. 160–187.CrossRefGoogle Scholar
[13]Rosser, J. B., A mathematical logic without variables, Annals of Mathematics, vol. 2 (1936), pp. 127–150.Google Scholar
[14]Staples, J., Church-Rosser theorems for replacement systems, Algebra and logic (Crossley, J. N., editor), Lecture Notes in Mathematics, vol. 450, Springer, Berlin, 1975, pp. 291–307.CrossRefGoogle Scholar