Concerning the Y combinator, I find it mind blowing in Javascript, because unlike the SKI calculus, Javascript is not meant to express that kind of things, but it actually can: https://bmsdave.github.io/blog/y-combinator-eng/Skepdick wrote: ↑Fri Mar 01, 2024 12:46 pm Shame. Are you unfamiliar with the Y combinator? From S,K and I we can construct Y and from there onwards... *kaboom*
The Y combinator may also be used in implementing Curry's paradox. The heart of Curry's paradox is that untyped lambda calculus is unsound as a deductive system, and the Y combinator demonstrates this by allowing an anonymous expression to represent zero, or even many values. This is inconsistent in mathematical logic.
Yes, S and K are meaningless. The symbol I is not meaningless, because it is the identity function, but it is redundant. You can replace I by (SKK) or (SKS).
The rewrite rules are:
1) Ix = x
2) Kxy = x
3) Sxyz = xz(yz)
A rewrite rule ("manipulation" rules) , is just a find-and-replace operation, just like a text editor does.
I "haha"= haha
K "whatever" "something" = whatever
x and y are just template placeholders. Below the rewrite rules look a bit more like in Perl or shell script:
1) I($x) => $x
2) K($x,$y) => $x
3) S($x,$y,$z) => $x$z($y,$z)
The third rewrite rule actually requires some extra power in the execution engine because implementing support for functions such as f($x) is not enough. You also need first-class functions such as $f($x), where the function itself is also a variable.
Without these rewrite rules the SKI calculus wouldn't be able to do anything. You need rules that allow you to rewrite an expression into another expression. Otherwise, it is not a calculus. Similarly, 1+2 can be rewritten to 3 in arithmetic calculus. So, we have a rewrite rule for the sum. i.e. a "manipulation" rule. The standard rewriting sequence in Peano arithmetic is 1+2 => 2+1 => 3+0 => 3. In the expression a+b, you just keep decreasing b while adding 1 to a until b is zero. At that point, you can switch to the final rewrite rule and say that n +0 => n.
Computability is an interesting branch in mathematics, but as far as I am aware of, it only has two interesting theorems: Turing's Halting problem and Rice's Theorem, which is itself actually a generalization of Turing's Halting problem. So, there is just one interesting theorem, so to speak of.
General computation "does" something. It does not explain things. It just executes them. I am mostly interested in surprising connections. Something that is insightful. Turing's Halting problem is definitely surprising and insightful. But where are the other insightful or surprising theorems in computability? Doing things or designing data structures and algorithms is something to do at work, as a job, because you get paid for that. I don't see where the interesting research would be.