[dvt]

I know Stephen Wolfram is a bit of a contentious figure, but his write-ups are always absolutely incredible. And if you're wondering why combinators are important (particularly S and K), SKI is a universal formal system[1]. Which is kind of crazy to think about: just two axioms and modus ponens can compute anything (I is just SKK).

[1] http://people.cs.uchicago.edu/~odonnell/Teacher/Lectures/For...

[ignoranceprior]

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...

https://en.wikipedia.org/wiki/Iota_and_Jot#Universal_iota

[dvt]

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=...

[tromp]

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)

[Uzomidy]

Does this mean that the Y combinator, Y = λf.(λx.f (x x)) (λx.f (x x)), is not a combinator?

[a1369209993]

> 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 ω.

[tromp]

Such a combinator ω cannot exist.