Re: single-combinator basis with direct algebraic characterisation?

From: r.e.s. (r.s_at_ZZmindspring.com)
Date: 11/02/04 

Date: Tue, 02 Nov 2004 16:25:11 GMT

"Torben Ęgidius Mogensen" <torbenm@diku.dk> wrote ...
> "r.e.s." <r.s@ZZmindspring.com> writes:
>
>> Combinators K,S can be characterised as satisfying
>> K a b = a
>> S a b c = a c (b c)
>> for arbitrary terms a,b,c.
>>
>> Does there exist a single-combinator basis, say X,
>> which can be similarly characterised as satisfying
>> X a b c ... = ...
>> in which only the arbitrary terms a,b,c,... appear
>> on the RHS? (X := \f.fKSK fails, evidently.)
>
> If I understand you correctly, you are asking for the
> RHS of X to have only variables and application operators
  ^^^^^^^^
> (i.e., no combinator names or local lambdas). In that
> case, the answer is no.

I think you meant to write "the RHS of the equation",
in which case that is indeed what I meant. Maybe the
negative answer should be obvious (?), but would you
care to give some indication of how to establish it?

--r.e.s.

Relevant Pages