Rice's theorem

[thomaskwaring]

This pull request extends the development of SKI combinatory logic — adding notions of evaluation and normal forms, and proving a version of Rice's theorem. The results and definitions are contained in the new file CombinatoryLogic/Evaluation.lean, which is based heavily on the following development by Bhavik Mehta.

Notes

The definitions and results of this PR allows us to define normal-order evaluation as a PFun, in the sense of Mathlib. The missing piece to make this useful is the so-called Standardisation theorem, saying that normal-order reduction will find a normal form, if there is one. The proof of Theorem T9 of Section C in A Mathematical Logic Without Variables (Rosser, 1935) should be amenable to formalization. This would be very interesting, as it ought to define a surjection from SKI terms to, for instance, partial recursive functions on the natural numbers, demonstrating that SKI terms are Turing-complete.

[fmontesi]

There seem to be conflicts?

[thomaskwaring]

oops my mistake! i've fixed the conflicts but it doesn't want to build remotely (it goes through on my computer) i think because of the linter warnings — i'll come back to this soon but it seems to want no space after the transition arrows (ie (P ⬝ Abs) ↠TT instead of (P ⬝ Abs) ↠ TT) which seems strange

[chenson2018]

it seems to want no space after the transition arrows (ie (P ⬝ Abs) ↠TT instead of (P ⬝ Abs) ↠ TT) which seems strange

Depending on how your terminal displays certain Unicode, what appears as roughly a single space after an arrow may actually be multiple spaces

[thomaskwaring]

Hmm I don't think that's it, it's definitely asking for no spaces. It's only complaining about hypotheses of the form "blank reduces to blank" (eg hxz : x ↠z), not for instance hxt : ∃ x : SKI, (P ⬝ x) ↠ TT, and not anywhere other than as hypotheses to a theorem. Anyway not a huge deal, just strange.

I expect it's because in the declaration
notation3 t:39 " ⭢" $sym:str t':39 => (ReductionSystem.Red $rs) t t'
there's no space after the arrow, was that for any reason?

[chenson2018]

I expect it's because in the declaration notation3 t:39 " ⭢" $sym:str t':39 => (ReductionSystem.Red $rs) t t' there's no space after the arrow, was that for any reason?

For this branch with a symbol after the arrow, I think this makes sense. I see though that for the notation without a symbol it is also like this, is that what is being linted for you? This should be changed, probably not noticed previously because we don't use it much.

[thomaskwaring]

For this branch with a symbol after the arrow, I think this makes sense. I see though that for the notation without a symbol it is also like this, is that what is being linted for you? This should be changed, probably not noticed previously because we don't use it much.

Ahh yes you're absolutely right — I've changed it and replaced the spaces after the transitions now