Hostname: page-component-78c5997874-4rdpn Total loading time: 0 Render date: 2024-11-19T05:39:19.067Z Has data issue: false hasContentIssue false

Axioms for strong reduction in combinatory logic

Published online by Cambridge University Press:  12 March 2014

Roger Hindley*
Affiliation:
Pennsylvania State University

Extract

In combinatory logic there is a system of objects which intuitively represent functions, and a binary relation between these objects, which represents the process of evaluating the result of applying a function to an argument. (This is explained fully in [1].) From this relation called weak reduction, “≥,” an equivalence relation is defined by saying that X is weakly equivalent to Y if and only if there exist n (with 0 ≤ n) and X0,…,Xη such that

It turns out that equivalent objects represent the same function, but two objects representing the same function need not be equivalent.

Type
Research Article
Copyright
Copyright © Association for Symbolic Logic 1967

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

[1]Curry, H. B. and Feys, R., Combinatory logic, vol. 1, North-Holland Co., Amsterdam, 1958.Google Scholar
[2]Sanchis, L. E., Normal combinations and the theory of types, Doctoral thesis, Pennsylvania State University, 1963; Notre Dame journal of formal logic, vol. 5 (1964), p. 161.Google Scholar
[3]Lercher, B., Strong reduction and recursion in combinatory logic, Doctoral thesis, Pennsylvania State University, 1963.Google Scholar
[4]Lercher, B., The decidability of Hindley's axioms for strong reduction, this Journal, vol. 32 (1967), pp. 237239.Google Scholar