A direct proof of the confluence of combinatory strong reduction
classification
🧮 math.LO
cs.LO
keywords
reductionstrongcombinatoryconfluencedirectgiveprooflambda-calculus
read the original abstract
I give a proof of the confluence of combinatory strong reduction that does not use the one of lambda-calculus. I also give simple and direct proofs of a standardization theorem for this reduction and the strong normalization of simply typed terms.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.