I mean, he obviously was aware of lambda-calculus as a thing that existed (since he used lambda notation for functions!), but might not have bothered to study it very closely. Nowadays the lambda calculus is considered very elegant, but in the 1940s I think it was considered quite weird and not very well known. (I forget who, but I think some famous logician complained that people did not read his thesis because it used the lambda-calculus formalism, or was adviced not to use it for that reason, or something like that.)
I think, actually the main reason it became so popular is exactly because it was implemented in Lisp/Scheme...
Why? Does every compiler writer know all the theoretical underpinnings and generalizations of their work? Or do that make something that solves a problem without investigating the entire universe around it?
Because he was certainly aware of the literature and he was a top notch scholar. Your follow-up questions seem to be implying something, care to spell it out for me?
But was he top notch back then? He's most well known for "creating" Lisp. And I put that in quotes because he never meant for anyone to implement it on a real machine.
re:was he top notch? By 1955 he was an assistant professor of Mathematics and known in his field. In 1956 he organised the Dartmouth conference where the field of Artificial Intellgence - got its name. He was a peer of Claude Channon, Marvin Minsky and Nathanial Rochester - so yes he was top notch. YC audience knows him for Lisp - but he was known for a lot more in his fields of research.
From what I understand, he purposefully took ideas from it, but because he did not feel like he understood it fully, he didn’t try to make a full implementation of it.
In his famous 1936 article, Turing correctly noted that proof of the computational undecidabilty of halting problem does not involve the same fixed point as the one used by Gödel.
I think, actually the main reason it became so popular is exactly because it was implemented in Lisp/Scheme...