Talk:Binary combinatory logic

This isn't on the Language List, and its categorization seems incomplete. For consistency, either it should be added to the Language List, or recategorized. Any opinions? --ais523 13:08, 19 May 2006 (UTC)

I don't think this should be categorized as a language. Category:Computational_models is probably more appropriate. --Rune 14:15, 19 May 2006 (UTC)

It seems like a very grey zone. Why it but not Iota and Jot? Especially if as I suspect, it is a creation of John Tromp, who is obviously interested in both esoteric languages and in the mathematical implications of BCL. Which was his reason for creating it? Intention matters or not, as the case of the atrocious commercial language BancStar shows. But it seems like languages based on mathematical ideas might be even more difficult to decide. Maybe not even the creator knows. I just know this will bite me one day, as a mathematician. :-) --Ørjan 14:41, 19 May 2006 (UTC)

Since the discussion seemed to die out without a consensus, I added it to the language list, for consistency because it is already in the Languages category.

However I then thought of an additional argument. I think that it is not a computational model in itself because its semantics are not really different from the ordinary combinatory logic model. Only the syntax distinguishes it. --Ørjan 19:00, 8 Jun 2006 (UTC)

Input-output specification

Can we change an existing language by adding I/O specification? Or should it be a new language with unique name? I suppose that it might be good idea to add I/O specification to BCL. It could be something BLC-like:

• Program is executed by applying the program to the input: 1 <program> <input>
• Input is represented as Church list of booleans (true for 0 bit, false for 1 bit) which ends with nil
• false = KI = SK = 10100
• true = K = 00
• nil = false = 10100
• cons = 11011101100011101100001101100011101100101110100000010000
• car = 11011101000010000
• cdr = 11011101000010010100
• [a, b, c] = 11 cons a 11 cons b 11 cons c nil

Program execution is performed as follows:

1. <expr> := reduce(1 <program> <input>)
2. Test <expr> for being nil: if reduce(11 <expr> ATOM1 ATOM2) evaluates to ATOM2 then it's the end of the program's output. Stop execution.
3. Extract single bit of output: if reduce(111 car <expr> ATOM1 ATOM2) evaluates to ATOM1 then output 0 bit. If it evaluates to ATOM2 then output 1 bit. Otherwise (neither ATOM1 nor ATOM2) the program is invalid.
4. Prepare to extract the next bit of output: <expr> := reduce(1 cdr <expr>)
5. Repeat from step 2.

--Blashyrkh (talk) 09:59, 6 February 2025 (UTC)

It's not that easy, Mr. John Tromp himself (by the way, he's the author of BCL which is not mentioned in the article) explained to me. The example he demonstrated: a program could return K(S(SK)) as output. Being applied to ATOM1 and then to ATOM2 (step 2 of program execution: test expression for being nil), it gives

K (S(SK)) ATOM1 ATOM2 = S (SK) ATOM2

which doesn't reduce any further. But being applied to some another argument x it gives

S (SK) ATOM2 x = SKx (ATOM2 x) = I (ATOM2 x) = ATOM2 x

which means that S (SK) ATOM2 is eta-equivalent to ATOM2. So, the program can return something eta-equivalent to zeroes and ones, but it would be hard to establish what it exactly is (would it be possible at all? How many steps of eta-expansion will be needed to determine that the object in question is actually nil or true?) --Blashyrkh (talk) 17:24, 7 February 2025 (UTC)

(...continue talking to myself...) Probably, there's a solution: reduction of an expression may or may not evaluate to ATOM1 or ATOM2. But we may switch to pure lambda calculus in this moment, and perform beta-reduction(s). Let's try:

K(S(SK)) ATOM1 ATOM2 =
= S(SK) ATOM2 =
... doesn't reduce any further :( ...
... (let's "switch keyboard layout" from CL to LC) ...
= (lambda x y z . xz (yz)) (SK) ATOM2 =
... 2 beta-reductions ...
= lambda z . (SKz) (ATOM2 z) =
... a little bit of CL cheating, but anyway ...
= lambda z . I (ATOM2 z) =
= lambda z . ATOM2 z =
... and 1 eta-reduction ...
= ATOM2
q.e.d.

Looks okay. But requires to go far beyond simple rewriting rules. Looks like Mr. Tromp is right: LC is more compact and expressive.--Blashyrkh (talk) 22:28, 7 February 2025 (UTC)