lambda calculus in some type system

Question

look at my system type (rules of them):
$$\frac{\Gamma(x:\tau)\vdash e:\rho}{\Gamma(x:\tau)\vdash \lambda x .e:\tau\rightarrow\rho}$$ $$\frac{\Gamma\vdash e_1:\tau\rightarrow\rho\ \ \ \ \ \Gamma\vdash e_2\rightarrow \tau}{\Gamma\vdash e_1e_2 : \rho}$$

$$\frac{}{\Gamma\vdash n:\text{int}}$$ $$\frac{}{\Gamma(x:\tau)\vdash x:\tau}$$

$$(\lambda x.e)e' \rightarrow ^{\beta} e[x:=e]$$

And types:
$$\tau ::= \text{int}|\tau_1 \rightarrow \tau_2$$ Possible expressions:
$$e::=x|n|e_1e_2|\lambda x.e$$ Now, I am trying to find some examples:
a) untypable expresssion: $(\lambda x.xx)$. It was fairly easy.
However, I am not sure about b)

b) $e$ should by untypable. $e', e \rightarrow ^{\beta} e'$ should be typable. Moreover, all variables in lambda expressions should be binded by lambda.

The only way that I see is:
$e = \lambda x.xx$ - untypable.
$e' = \lambda x.x$ - typable. $e \rightarrow ^{\beta} e' = \lambda x.x(\lambda x.x)$ seems to be typable.

What do you think about it ? Maybe, someone can give other example (assuming that my examples are correct).

Edit, second example
Give example of typable expressions $e, e'$ and type $\tau$ such that there are fullfilled three conditions:
(a) $e\rightarrow ^{\beta} e'$
(b) $e'$ is type of $\tau$
(c) $e$ is not type of $\tau$.

Answer 1

$e = \lambda x. x x$ does not reduce to $\lambda x. x(\lambda x. x)$. $e$ is an abstraction: remember the convention says $\lambda x. x x$ is syntactic sugar for $(\lambda x. (x\ x))$. Note that under full $\beta$-reduction strategy we could try reducing the body of the abstraction, but in our case the body of $e$ does not contain a redex (reducible expression).

If we are allowed to use integer literals, then $$(\lambda x. 0)\ (0\ 0)$$ is not well-typed, but it reduces (under the call-by-name strategy) to $0$, which has type $\mathsf{int}$.

Another example, which does not use any integer literals: $$ (\lambda z. (\lambda y. y))\ (\lambda x. x\ x) \to_\beta (\lambda y. y)[z := (\lambda x. x\ x)] = (\lambda y. y) $$ is not well-typed because the argument of the application is not well-typed, but it reduces in one step to $\lambda y. y$, which (for example) can be assigned the type $\mathsf{int} \to \mathsf{int}$.

As for your last example, it is impossible to find such two well-typed expressions $e$ and $e'$ with the properties $e\rightarrow ^{\beta} e'$ and $\mathrm{typeof}(e) \ne \mathrm{typeof}(e')$. Your system looks very much like a simply-typed lambda calculus (with implicit types) enhanced with integers. There is the preservation theorem for STLC: $$ \Gamma \vdash e : \tau \; \wedge \; e \to_\beta e' \implies \Gamma \vdash e' : \tau , $$ which does not let you find the desired $e$ and $e'$.

The preservation theorem is covered in the Types and Programming Languages book by B.C. Pierce.