Models of Computation: An Introduction to Computability Theory (Undergraduate Topics in Computer Science) [Paperback]

About me: I'm a grad student in math, but have no prior experience
of the topic of the book. I have actually not yet read the 40
last pages or so, so the review is about the rest of the book.

I will be quite negative below, so I want to start by saying
that most chapters are OK, and I love short books. And this
book gives you a quick way of getting aquainted with various models
of computation. I dont agree with the official reviewer that
it goes in to depth or is extremely clear and well written.
On the contrary, it does NOT go into depth in all chapters, but
is rather uneven. I really liked the chapter about lambda-calculus.

My general impression is that the author is often saying
"how to think" about the definitions and concepts, and what they
intuitively are, rather than precisely saying what the definition IS.
I believe that the cause of my confusion, other than perhaps ignorance,
is the lack of crucial pieces of information. (See examples below).

Many times I found myself confused after reading a definition, and
really needed an example to clarify what was going on. Although
there are fairly many examples in the book, there were several places
in desperate need thereof.

It is mostly chapters 5 and 7 that I find confusing.

Example (chapter 5, on logic programs)
Definitive clauses - Program clauses and Goals - are defined.
A definitive clause is P1 or (not P2 or not P3 .... or not Pn), i.e. a
disjunction of so called "literals", and atmost one literal is positive.
A definitive clause is a Goal if we remove P1, i.e. we have only negative literals.

The problem is that there is only a definition of what a Goal is but not
what meeting a Goal is...
Only a very vague and incomplete explaination is given:

"Program clauses can be seen as defining a database: [...] Goals are questions
to be answered using the information about the problem in the database.
This can be better seen with some examples."

Then there is only ONE example in which the goal has only ONE negative literal.
That leaves the reader wondering if each literal P2, ...., Pn should be true
or just "atleast one of them".

Since the notation for a goal is :- P2,P3,...,Pn
you might believe that the goal is to deduce ALL of the Pi's, but
since its a disjunction of negative literals, mathematically it only makes sense
if the goal clause should be disproven, which means that ONE of the Pi's hold.
It gets even more confusing later on. Although I might have my self to blame
for some of the confusion, I am pretty convinced this is far from optimally
written.

Other complaints:
There are some flaws in the technique of writing. For example the author mentions
multisets several times, but gives the definition only the last time. On another
instance a new symbol is used and defined afterwards.
There is also a logical flaw on page 61. There is an argument that "bounded minimisation"
of a primitive recursive predicate is also primitive recursive.
The argument uses a lemma whose input are functions f_1, ..., f_k that are primitive recursive
total functions. Then the lemma is applied in a case where f_1 is a priori only partially defined.
I'm sure its possible to fix this argument, but it still makes life unneccesarily difficult for
the reader.