Title

Lambda terms definable as combinators

RIS ID

87049

Publication Details

Bunder, M. W. (1996). Lambda terms definable as combinators. Theoretical Computer Science, 169 (1), 3-21.

Abstract

It si well known that for each ^-term there is a corresponding combinatory term formed using the combinators K and S instead of the ^-operator. Similarly for every combinatory term there is a ^-term. For weaker sets of combinators such as B, C and K or B, B', I and W we show how such a correspondence for 'translation; can be formulated and we determine in the case of several such sets of combinators the sets of ^ -terms that can be translated using them.

As combinators can represent Hilbert-style proofs of theorems of implicational logic and ^-terms natural deduction style proofs, this work allows us to formulate natural deduction systems equivalent to the Hilbert-style systems for various implicational logics and can form a basis for proof generating programs for these logics.

Please refer to publisher version or contact your library.

Share

COinS
 

Link to publisher version (DOI)

http://dx.doi.org/10.1016/S0304-3975(96)00111-9