Definition of sets and functions

Question

The main problem is that I do not understand what the hell is even being asked in this question. Is anyone familiar with inductive definitions that could help me go through these definitions and understand what the question is about? I think that for the base case of the definition I need to define the variables of type $t$ and the constants also of type $t$, and that the inductive step will be the functions that take more parameters. Otherwise, I am totally and completely stumped by the formulation of the question.

Answer 1

Let $I = \langle \phi, \theta \rangle$ and $V$ be given as you have stated (but replacing $n$ by $1$ in the type declarations for the functions, which I think is what you meant). There are two other bits of data in your problem that we need names for: $F = \mathrm{dom}(\phi)$ (the set of constant and function names) and $\tau$, the function $V \to \theta$ that assigns a type to each variable. The set $E_t = E_{I, V, t}$ of type-correct expressions of type $t$ for a type $t \in \theta$ comprise the smallest set of expressions that contains $\{v \in V \mid \tau(v) = t\}$ (the variables of type $t$ and $\{c : F \mid \phi(c) = t\}$ and that is closed under the operation on sets of expressions $X$, that, given $f \in F$ with $\phi(f) = t_1 \times \ldots t_k \to t$ and expressions $e_1 \in E_{t_1}, e_2 \in E_{t_2} \ldots e_k \in E_{t_k}$, adds $f(e_1, e_2, \ldots, e_k)$ to $X$.

Because we are having to define the $E_{t}$ in parallel, a more formal definition would define the $E_{t}$ (at once for all $t$) as the union of $\bigcup_{n=1}^\infty E_{t, n}$, where $E_{t, n}$ gives the expressions of height at most $n$. We would then have

\begin{align*} E_{t, 1} &= \{v \in V \mid \tau(v) = t\} \cup \{c : F \mid \phi(c) = t\} \\ E_{t, n + 1} &= \bigcup_{k=1}^\infty \{f(e_1, e_2, \ldots, e_k) \mid f \in F \land \phi(f) = t_1 \times \ldots t_k \to t \land {}\\ &\quad \quad \quad \quad \quad \quad \quad \quad e_1 \in E_{t_1, n} \land e_2 \in E_{t_2, n} \land \ldots \land e_k \in E_{t_k, n}\}\\ E_t &= \bigcup_{n=1}^\infty E_{t, n} \end{align*}