Notation: I use
-  \x denotes lambda abstraction
-

(1) If we take A_sigma = IN (the natural numbers) and App = *
(multiplication), this cannot be made into a type frame. (See the
definition on page 53 of the notes of Gunter.) Prove this.

Hint: assume that there is an interpretation [[-]] satisfying the definition.
(a) Show that [[\x.\y. xy]] = [[\x.\y. yx]]
(b) Conclude that d = e for any element in IN
So: contradicion.

(2) Prove Lemma 8.2 in the notes of Gunter: M*[N*/x] = (M[N/x])*,
where (-)* is the embedding of untyped lambda-calculus into simple
type theory.

(3) Compute in D_X the interpretation of:
(a) \x.x
(b) \x.\y.x

(4) Compute in D_X the interpretation of y and of \x.yx and coclude
that the eta-rule does not hold in D_X.