Can anyone explain briefly (if thats possible!) or refer me to a reference, summarizing the differences between untyped lambda calculus and the more common typed lambda calculi?
I'm particularly looking for statements of their expressive power, equivalences to logic/arithmetic systems or computation methods, and analogies to programming languages if applicable.
While I certainly intend to read, something like a reference table outlining the calculi and their equivalences/differences/place in the heirarchy would be a HUGE reference for helping me sort them out.
Not saying the below is correct, just trying to sketch together some of the impressions i have to see if they at least serve as a starting point (or something to correct!)
Untyped lambda calculus - eq. to first order logic - cannot do X
Simply typed lambda calculus - eq to ... logic, related to Lisp?
'Polymorphic' lambda calc - etc.
Calculus of Constructions - intutionist logic?
Combinatory Logic - comparable to ??? typed lambda calculus, related to APL/J kind of languages
If this ties into the lambda cube and its three axes all the better.
While I'm familiar with the basics of lambda calculus and programming with functional languages, I have never wrapped my head around, or made any significant connections to, the type systems involved and different flavors of lambda (and maybe pi?) calculi.
When I attempt to research this i cant help but find myself sidetracked, opening up many browser tabs and branching in so many directions I never get into any of them with any depth!
I'm not sure if what I'm asking for is reasonable, but hopefully at the very least I've painted enough of a picture to suggest some reading that can explain what im looking for?