A direct proof of the confluence of combinatory strong reduction
Logic
2009-05-19 v1 Logic in Computer Science
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.
Keywords
Cite
@article{arxiv.0905.2545,
title = {A direct proof of the confluence of combinatory strong reduction},
author = {René David},
journal= {arXiv preprint arXiv:0905.2545},
year = {2009}
}
Comments
To appear in TCS