SK computation

Stream: computer science

[Bhavik Mehta]

Just wanted to mention this file: https://gist.github.com/b-mehta/e412c837818223b8f16ca0b4aa19b166 which I made a little while ago, that defines SK terms, shows they're a confluent rewrite system, formalises logic and arithmetic relative to them, and proves things about the semantics and evaluation also; in case it is interesting to people here.

[Fabrizio Montesi]

Nice! @Thomas Waring, maybe interesting for our SKI development in https://github.com/cs-lean/cslib/tree/main/Cslib%2FComputability%2FCombinatoryLogic?

[Thomas Waring]

very interesting! i started playing around with code for reductions / reflexes / normal forms so this is very helpful — rice’s theorem would also be very interesting!

[Bhavik Mehta]

Rice's theorem is in there too :)

[Fabrizio Montesi]

@Bhavik Mehta let us know if you'd be interested in porting (portions of?) your code to our common lib. :⁠-⁠)

[Bhavik Mehta]

I think there might be a challenge because I treated I as a non-primitive, whereas it's a primitive for you. But you're welcome to take parts of my code that's useful to you.