Re:Where Did Combinators Come From? Hunting the Story of Mos...
by ignoranceprior on Monday December 07, 2020 @02:57PM
(#25336487)
There are actually single combinators which form a complete basis, i.e. from which you can get S and K, and thereby universal computation.
https://en.wikipedia.org/wiki/Combinatory_logic#One-point_ba...
Re:Where Did Combinators Come From? Hunting the Story of Mos...
by dvt on Monday December 07, 2020 @03:08PM
(#25336650)
Iota is still defined in terms of S and K. More technically, Iota is an "improper" combinator (see pg. 779 in [1]). Therefore, you can't axiomize Iota, so it would be hard to argue that it's more "fundamental" than S and K.
[1] https://books.google.com/books?id=1xEVkzuX5e0C&pg=PA779&lpg=...
Re:Where Did Combinators Come From? Hunting the Story of Mos...
by tromp on Monday December 07, 2020 @04:19PM
(#25337692)
A single point basis (like X = \z. z K S K for which
X X = K K, X X X = K, and X (X X) = S) is not in itself a combinator.
A combinator is not just a closed lambda term; it must have all lambdas in leading position. Like S = \x \y \z. x z (y z)
Re:Where Did Combinators Come From? Hunting the Story of Mos...
by Uzomidy on Wednesday December 09, 2020 @07:47PM
(#25367918)
Does this mean that the Y combinator, Y = λf.(λx.f (x x)) (λx.f (x x)), is not a combinator?
Re:Where Did Combinators Come From? Hunting the Story of Mos...
by a1369209993 on Monday December 07, 2020 @11:45PM
(#25341940)
> A single point basis [...] is not in itself a combinator.
> A combinator [...] must have all lambdas in leading position.
What's your opinion on:
ωabcd = bd(cd) if a has no normal form[0][1]
or = c if b has no normal form
or = d if c has no normal form
or = dd otherwise
where
SII = ωωωω
Ω = SII(SII) = ωωωω(ωωωω)
S = ωΩ = ω(ωωωω(ωωωω))
K = ωωΩ = ωω(ωωωω(ωωωω))
I = ωωωΩ = ωωω(ωωωω(ωωωω))
as a single-'combinator' basis?0: Aka, does not halt.
1: Evaluation diverges if a (or b or c, if queried) is somthing like:
SII(C(C(B(ωωx(KI)K)(SII))Ω)I)
(from https://en.wikipedia.org/wiki/Combinatory_logic#Undecidabili...) that tries to diagonalize ω.
[1] http://people.cs.uchicago.edu/~odonnell/Teacher/Lectures/For...