Not to dispute your point, but note the lambda-calculus-as-a-reasonable-machine papers from the last couple of years: it turns out (despite the seeming general understanding to the contrary in the past) that polynomial interpreters for some meanings of “lambda calculus” (including IIRC a weird very general one, call-by-need on open terms) are perfectly possible, meaning that many fundamental questions of computational complexity can be straightforwardly expressed in terms of the lambda-calculus machine as well. Linear-time interpretation (thus e.g. classes L and NL) seemed out of reach last I checked, though.
To echo my other comment here, it’s not that Church himself knew that. Even five years ago people did not know that. It’s not a question of priority. But I find it fascinating and reassuring nevertheless, as actually programming e.g. a self-interpreter for a Turing machine—or for general recursive functions, or for combinatory calculus—is an absolute slog.
Didn’t have access to my archive at the time, so got some of the details wrong it seems (e.g. CbV not CbN, result for time is older than I remembered). Main thrust should remain valid, but be careful. In any case, here you go:
Dal Lago, Martini (2008). “The weak lambda calculus as a reasonable machine”. DOI:10.1016/j.tcs.2008.01.044, apparently not on arXiv.
Accattoli (2012). “A fresh look at the lambda-calculus”. DOI: 10.4230/LIPIcs.FSCD.2019.1, apparently not on arXiv.
Accattoli, Dal Lago (2014). “Beta reduction is invariant, indeed”. DOI: 10.1145/2603088.2603105, arXiv: 1405.3311 [cs.LO].
Accattoli, Dal Lago (2016). “(Leftmost-outermost) beta reduction is invariant, indeed”. DOI: 10.2168/LMCS-12(1:4)2016, arXiv: 1601.01233 [cs.PL].
Forster, Kunze, Roth (2020). “The weak call-by-value lambda-calculus is reasonable for both time and space”. DOI: 10.1145/3371095, arXiv: 1902.07515 [cs.CC].
Now that I’m looking through bibliographies, there are apparently other relevant intervening papers in the vicinity, even by some of the same authors, but these are what I’ve looked at personally.
Bonus: the paper
Hackett, Hutton (2019). “Call-by-need is clairvoyant call-by-value”. DOI: 10.1145/3341718, apparently not on arXiv.
is unrelated to questions of complexity but is just so absolutely lovely.
To echo my other comment here, it’s not that Church himself knew that. Even five years ago people did not know that. It’s not a question of priority. But I find it fascinating and reassuring nevertheless, as actually programming e.g. a self-interpreter for a Turing machine—or for general recursive functions, or for combinatory calculus—is an absolute slog.