Grothendieck
... something covering "how to do math". This might be an introductory real analysis or linear algebra book, or (alas, I haven't read much in this area) you could do no wrong looking for books on problem solving, contests, and inequalities, say by Polya or Andreescu.
... a higher-level view of day-to-day mathematical practice. There probably isn't one book for this, but I'd recommend Loomis and Sternberg's Advanced Calculus as a summation of linear algebra and calculus on manifolds; you'd also need to read on complex and functional analysis, algebra (Lang and the unofficial companion volume?), topology ...
... a broad but shallow introduction to several fields and applications unified but a common underlying approach (abstraction and programming language design). I'd recommend Geroch's Mathematical physics, which, as the name implies, studies algebra, algebraic topology, and functional analysis through the common lens of category theory.
... a somewhat quirky book on foundations? You could look for a book on naive or axiomatic set theory, categories, or type theory.
As you probably know, there are two major domains where lambda calculi appear: computability (which I know next to nothing about) and formal methods/type theory/PLs. The people talking about "showing functions can't be computed" are referencing the former. From the formal methods view, a calculus really consists of a syntax (the set of allowable terms; this is like the state space) plus a dynamic semantics (which is like the dynamics), and optionally a static semantics (e.g., typing rules). I.e., we have the following analogy (which holds best for small-step semantics; see below) between lambda calculus and physics:
semantics : programs :: differential equations : physical states.
(While ML is basically a compiler for a lambda calculus, you can even define calculi to prove things about Java if you wanted.)
Now, to answer your questions. Let's say our set of terms (our syntax) is
term := x -- var
| \x . t -- lambda abstraction
| t1 t2 -- application
| n -- natural number
| div n1 n2
We clearly expect the function defined syntactically by
f := \x . div 1 0
A denotational semantics would define a semantic function S[[ ]] taking our function into the mathematical (partial) function x |-> 1/0. We would also require that S is a homomorphism, so S[[ f x ]] = S[[ f ]](S[[ x ]]), which indeed is undefined in the usual mathematical sense.
A big-step operational semantics is similar to a small-step operational semantics and so I won't describe it except to say that it rather resembles an implementation of an eval/apply Scheme interpreter (but as a purely mathematical relation on terms, and usually using the fundamental LC idea of substitution instead of an "environment"). A big-step semantics often suppresses both nontermination and "bad" states arising from nondeterministic rules (think concurrency).
A small-step operational semantics is closest to the notion of a dynamics in physics (especially in the discrete case of difference equations). Let's define one. We have choices for what "div n 0" should be: it could be some arbitrary value of our choosing (or we could extend div with an extra argument to give as the answer in this case), we could "get stuck" (i.e., not allow any transitions out of such a state), or we could add an error state to the the syntax and evaluate div n 0 to error (this generalizes pretty easily to try/catch, assert(), ...). The semantics are (technically we are defining a relation called -> on terms):
If mathematical division gives an answer, so does our division program:
n/m = p
------------
div n m -> p
We also need more reduction rules:
t -> t'
---------------------
div t t2 -> div t' t2
t2 -> t2'
---------------------
div v t2 -> div v t2'
----------------
div n 0 -> error
Application proceeds by reducing the function first (we'll either end up with a lambda or a number, which we could avoid by typing our calculus):
t1 -> t1'
---------------
t1 t2 -> t1' t2
Then we prove certain things about the language using induction, usually induction on derivations (just a special case of well-founded induction). We can't prove much about an untyped calculus, though.
Now your first two questions should be clear, e.g.:
f v
-> div 1 0 -- by substitution rule
stuck! (i.e., no rule applies)
-> error
For your last question, you could add recursion either by hand (look up "fix") or with the Y combinator, then show that (again let's look at values first, since an arbitrary term might error in a different way):
f v -> .... -> f v
There's also the formal/mechanized logic/proving aspect (omitted for brevity). It's nice that it's easy to study lambda calculi with theorem provers since, as you can see, it's easy to forget a rule or make a small mistake in a proof.
(I'm being quite imprecise here: I haven't shown what rule induction is or why it's valid, or how the rule definitions work, or ... )
There are many lambda calculi, ranging from the untyped lambda calculus with strict evaluation underlying Scheme to the Calculus of Inductive Constructions which provides an alternative foundation for mathematics to set theory and is the basis of the Coq theorem prover which has formalized proofs of the Four-Color and Feit-Thompson theorems.
For a slightly more common architecture (although hopefully we are entering an FPGA-enabled golden age), try Harris & Harris's "Digital design and computer architecture". It covers the MIPS designs (using both SystemVerilog and VHDL simultaneously) in H&P's "Computer organization and design", but in a more compact and systematic way (omitting H&P's broad but shallow coverage of advanced topics).
http://ezyang.tumblr.com/post/62157468762/haskell-haskell-an...
For more on purely functional parallelism, see Guy Blelloch's research (https://www.cs.cmu.edu/~guyb/research.html) and CMU's algorithms course (https://www.cs.cmu.edu/afs/cs/academic/class/15210-f11/www/r...) and parallel algorithms course (https://www.cs.cmu.edu/afs/cs/academic/class/15499-s09/www), and Manticore, a parallel SML (http://manticore.cs.uchicago.edu/).
http://www.youtube.com/playlist?list=PL0E754696F72137EC
These could go with the either the book by W. Rudin or (haven't read) A. Browder. These are not easy for a complete beginner; maybe the lectures can provide some motivation. "Understanding Analysis" by S. Abbott is another rigorous and much easier, but very good, introduction.
"Advanced calculus" by Shlomo Sternberg ... a work of profound beauty. This was the book used at Harvard in the 60s for the best freshman students, but it begins in a slow yet deep way with sets, logic, linear algebra, calculus, metric spaces... It's my favourite book on calculus on manifolds. http://www.math.harvard.edu/~shlomo/
Some freely available books by Robert Ash: http://www.math.uiuc.edu/~r-ash/ - in particular, his misleadingly-named "Complex variables" (with W.P. Novinger) is a short, rigorous book on complex analysis.
"Naive Set Theory" by Paul Halmos is now available for something like $12.
(I have not read the following books.)
For number theory, maybe the book by George Andrews? It's very elementary and very cheap, and looks top notch.
I'd like to read "The Cauchy-Schwartz master class" (on inequalities) but haven't purchased it yet.
There are many books on combinatorics and graphs by the Hungarian school. Probably deserving special attention for discrete math are "Concrete mathematics" by Knuth et al. and "Analysis of algorithms" by Sedgewick and Flajolet (distinct from Sedgewick's "Algorithms").