\section{Semantics for the Ideal Case Marking Language}
%
%
%
The semantics outlined in the previous section can be used 
to give a compositional account of the semantics of the 
ideal case marking language. We shall assume that the 
function symbol {\tt f} is of arity $\Omega(\mbox{\tt f})$ and 
has meaning $\mbox{\sf f}$. We shall also assume that 
we have symbols {\tt 0}, {\tt 1} etc. The lexical entry for 
{\tt f} is therefore the following:
%%
$$\begin{array}{|c|}
\multicolumn{1}{c}{\mbox{\tt f}} \\
\hline
\circ : \circ \\
\hline\hline 
\varnothing \\
\hline
\circ \doteq \mbox{\sf f}(\mbox{\tt 0}{^{\smallfrown}\circ}, 
	\mbox{\tt 1}{^{\smallfrown}\circ}, \ldots, 
	\Omega(f)-1{^{\smallfrown}\circ}) \\
\hline
\end{array}$$
%%
System variables like {\tt x} and {\tt y} are treated just like 0--ary 
function symbols:
%%
$$\begin{array}{|c|}
\multicolumn{1}{c}{\tt x} \\
\hline
\circ : \circ \\
\hline\hline
\varnothing \\
\hline
\circ \doteq \mbox{\tt x} \\
\hline
\end{array}$$
%%
The elements {\tt 0}, {\tt 1} have the following semantics: 
%%
$$\begin{array}{|c|}
\multicolumn{1}{c}{\tt 0} \\
\hline
\circ : \mbox{\tt 0}{^{\smallfrown}\circ} \\
\hline\hline
\varnothing \\
\hline
\varnothing \\
\hline
\end{array}$$
%%
There are only two conventions: 
%%
\begin{enumerate}
\item {\tt 0}, {\tt 1} etc may only be suffixes. 
\item {\tt 0}, {\tt 1} etc may only be attached 
	to simple expressions. 
\end{enumerate}
%%
Here a simple expression is one that contains only 
one function or variable symbol. A simple expression is 
one that corresponds to a single branch of the tree 
domain. We shall understand that this is a syntactic 
restriction that is not due to any semantics. We shall 
return to the implications of these conventions below. 

To see that this works as intended we shall reproduce 
an earlier example. Take the arithmetical term 
$\mbox{\tt +}(\mbox{\tt -}(\mbox{\tt x},\mbox{\tt y}),\mbox{\tt z})$. 
It is represented by the following string:
%%
$$\mbox{\tt y10+-0x00z1}$$
%%
By the conventions, this must be parsed in the following 
way:
%%
$$((\mbox{\tt y1})\mbox{\tt 0})(\mbox{\tt +})(\mbox{\tt -0})((\mbox{\tt 
x0})\mbox{\tt 0})(\mbox{\tt z1})$$
%%
Among the terms enclosed in brackets, one must go from left to right 
otherwise the merge is undefined. For all other terms, the direction 
is completely irrelevant. 

We start from the left end. We compose {\tt y} and {\tt 1}. 
%%
$$\begin{array}{|c|}
\multicolumn{1}{c}{\tt y1} \\
\hline
\circ : \circ \\
\hline\hline
\varnothing \\
\hline
\mbox{\tt 1}{^{\smallfrown}\circ} \doteq 
\mbox{\tt y} \\
\hline
\end{array}$$
%%
Next we compose with {\tt 0}:
%%
$$\begin{array}{|c|}
\multicolumn{1}{c}{\tt y10} \\
\hline
\circ : \circ \\
\hline\hline
\varnothing \\
\hline
\mbox{\tt 10}{^{\smallfrown}\circ} \doteq 
	\mbox{\tt y} \\
\hline
\end{array}$$
%%
We compose with {\tt +}:
%%
$$\begin{array}{|c|}
\multicolumn{1}{c}{\mbox{\tt y10+}} \\
\hline
\circ : \varepsilon \\
\hline\hline
\varnothing \\
\hline
\mbox{\tt 10}{^{\smallfrown}\circ} \doteq 
	\mbox{\tt y} \\
\circ \doteq \mbox{\tt +}(\mbox{\tt 0}{^{\smallfrown}\circ}, 
	\mbox{\tt 1}{^{\smallfrown}\circ}) \\
\hline
\end{array}$$
%%
Next we compose {\tt -} and {\tt 0} and get 
%%
$$\begin{array}{|c|}
\multicolumn{1}{c}{\mbox{\tt -0}} \\
\hline
\circ : \circ \\
\hline\hline
\varnothing \\
\hline
\mbox{\tt 0}{^{\smallfrown}\circ} \doteq 
	\mbox{\tt -}(\mbox{\tt 00}{^{\smallfrown}\circ}, 
	\mbox{\tt 10}{^{\smallfrown}\circ}) \\
\hline
\end{array}$$
%%
Together with the last this gives
%%
$$\begin{array}{|c|}
\multicolumn{1}{c}{\mbox{\tt y10+-0}} \\
\hline
\circ : \circ \\
\hline\hline
\varnothing \\
\hline
\mbox{\tt 10}{^{\smallfrown}\circ} \doteq 
	\mbox{\tt y} \\
\circ \doteq \mbox{\tt +}(\mbox{\tt 0}{^{\smallfrown}\circ}, 
	\mbox{\tt 1}{^{\smallfrown}\circ}) \\
\mbox{\tt 0}{^{\smallfrown}\circ} \doteq 
	\mbox{\tt -}(\mbox{\tt 00}{^{\smallfrown}\circ}, 
	\mbox{\tt 10}{^{\smallfrown}\circ}) \\
\hline
\end{array}$$
%%
The term {\tt x00} is analogous to {\tt y10} and 
{\tt z1} to {\tt y0}:
%%
$$\begin{array}{|c|}
\multicolumn{1}{c}{\tt x00} \\
\hline
\circ : \varepsilon \\
\hline\hline
\varnothing \\
\hline
\mbox{\tt 00}{^{\smallfrown}\circ} \doteq 
	\mbox{\tt x} \\
\hline
\end{array}
\qquad
\begin{array}{|c|}
\multicolumn{1}{c}{\tt z1} \\
\hline
\circ : \circ \\
\hline\hline
\varnothing \\
\hline
\mbox{\tt 1}{^{\smallfrown}\circ} \doteq 
	\mbox{\tt z} \\
\hline
\end{array}$$
%%
Composing them with the above result we get:
%%
$$\begin{array}{|c|}
\multicolumn{1}{c}{\mbox{\tt y10+-0x00z1}} \\
\hline
\circ : \circ \\
\hline\hline
\varnothing \\
\hline
\mbox{\tt 10}{^{\smallfrown}\circ} \doteq 
	\mbox{\tt y} \\
\circ \doteq \mbox{\tt +}(\mbox{\tt 0}{^{\smallfrown}\circ}, 
	\mbox{\tt 1}{^{\smallfrown}\circ}) \\
\mbox{\tt 0}{^{\smallfrown}\circ} \doteq 
	\mbox{\tt -}(\mbox{\tt 00}{^{\smallfrown}\circ}, 
	\mbox{\tt 10}{^{\smallfrown}\circ}) \\
\mbox{\tt 00}{^{\smallfrown}\circ} \doteq 
	\mbox{\tt x} \\
\mbox{\tt 1}{^{\smallfrown}\circ} \doteq 
	\mbox{\tt z} \\
\hline
\end{array}$$
%%
We shall verify that the value of $\circ$ is actually the same as 
the value of $\mbox{\tt +}(\mbox{\tt -}(\mbox{\tt x}, \mbox{\tt y}), 
\mbox{\tt z})$. This can be shown by reducing the system of equations. 
Notice first of all that in the body of the DRS there is an equation
saying that $\mbox{\tt 00}{^{\smallfrown}\circ}$ has the 
same value as {\tt x}, $\mbox{\tt 10}{^{\smallfrown}\circ}$ 
the same value as {\tt y} and $\mbox{\tt 1}{^{\smallfrown}\circ}$ 
the same value as {\tt z}. We may therefore reduce the 
body of the last structure to 
%%
$$\begin{array}{c}
\circ \doteq +(\mbox{\tt 0}{^{\smallfrown}\circ}, \mbox{\tt z}) \\
\mbox{\tt 0}{^{\smallfrown}\circ} \doteq 
	\mbox{\tt -}(\mbox{\tt x}, \mbox{\tt y}) 
	\end{array}$$
	%%
We may finally replace $\mbox{\tt 0}{^{\smallfrown}\circ}$ 
by $\mbox{\tt -}(\mbox{\tt x},\mbox{\tt y})$ in the first line. 
We then get 
%%
$$\circ \doteq \mbox{\tt +}(\mbox{\tt -}(\mbox{\tt x}, %
\mbox{\tt y}), \mbox{\tt z})$$
%%
%%
Notice that the merge is always defined, so that any binary parse of 
the string yields a string--to--meaning translation. However, not all 
of them can be correct. A specific example and a thorough discussion 
of this will follow in Section~\ref{sec6}. So, we need a 
characterization of those strings that yield a proper traslation. 
Call a sequence of case markers a {\it register}. Call a string of the 
form $f{^{\smallfrown}\sigma}$ a {\it block}, if $f \in F$ and 
$\sigma$ a register. Any string over $\Omega^{\gamma}$ can be 
naturally decomposed into a sequence of blocks. The grammar that 
generates a parse is the following. (Here, {\tt S} stands for 
{\it string}, {\tt B} for {\it block}, {\tt C} for {\it case}, 
{\tt F} for {\it function}, and {\tt R} for {\it register}.)
%%
$$\begin{array}{l@{\quad \pf \quad}l}
\mbox{\tt S} & \mbox{\tt B}\mid \mbox{\tt SB} \\
\mbox{\tt B} & \mbox{\tt FR} \\
\mbox{\tt R} & \varepsilon \mid \mbox{\tt CR}
\end{array}$$
%%
\begin{thm}
A string $\vec{x}$ over $\Omega^{\gamma}$ is in 
$\mbox{\it ICM}_{\Omega}$ iff 
%%
\begin{enumerate}
\item No two blocks of $\vec{x}$ have the same register.
\item If $\sigma{^{\smallfrown}\mbox{\tt c}_k}$ is a register of $\vec{x}$, 
	then so is $\sigma$.
\item If $f{^{\smallfrown}\sigma}$ is a block of $\vec{x}$, then 
	\begin{enumerate}
	\item
	there is no register of the form $\sigma{^{\smallfrown}
	\mbox{\tt c}_k}$ where $k \geq \Omega(f)$,
	\item
	for all $k < \Omega(f)$ there is a register of the form 
	$\sigma{^{\smallfrown}\mbox{\tt c}_k}$.
	\end{enumerate}
\end{enumerate}
\end{thm}
%%
The proof is rather straightforward and omitted. Likewise, the 
weak ideal case marking language is characterized by omitting the 
existential clauses of the previous definition:
%%
\begin{thm}
A string $\vec{x}$ over $\Omega^{\gamma}$ is in 
$\mbox{\it WICM}_{\Omega}$ iff 
%%
\begin{enumerate}
\item No two blocks of $\vec{x}$ have the same register.
\item If $f{^{\smallfrown}\sigma}$ is a block of $\vec{x}$, then 
	there is no register of the form $\sigma{^{\smallfrown}
	\mbox{\tt c}_k}$ where $k \geq \Omega(f)$,
\end{enumerate}
\end{thm}
%%
We shall use these results to establish some complexity results 
about these languages. 
%%
\begin{defn}
Let $A = \{a_i : i < n\}$ be a finite set and $\BN^n$ the 
monoid of $n$--tuples of natural numbers with 0 and addition 
as operations. Let $e_i := \auf \delta^i_j : j < n\zu$ 
where $\delta^i_j := 1$ iff $i = j$ and $\delta^i_j := 0$ 
otherwise.  Define $\psi : A^{\ast} \pf \BN^n$ inductively 
as follows. 
%%
$$\begin{array}{l@{\quad := \quad}l}
\psi(\varepsilon) & 0 \\
\psi(\vec{x} \cdot a_i) & \psi(\vec{x}) + e_i 
\end{array}$$
%%
Call $S \subseteq A^{\ast}$ {\bmi linear} if there are 
$u_i \in \BN^n$, $i < \lambda$, such that 
%%
$$\psi[S] = \{u_0 + \sum_{i = 1}^{\lambda} \mu_i e_i : 
	\mu_i \in \BN, 1 \leq i \leq \lambda\}$$
%%
Finally, call $S$ {\bmi semilinear} if it is a finite union 
of linear sets. 
\end{defn}
%%
By a theorem of Parikh, context--free languages are semilinear 
(see \cite{harrison:formal} for a proof). It can be shown that 
also linear indexed languages and MCTALs as well as multiply 
context--free languages are semilinear. However, the following 
is shown in \cite{ebert:stacks}, building on results of 
\cite{michaeliskracht:semilinear}. 
%%
\begin{thm}[Ebert]
$\mbox{\it ICM}_{\Omega}$ and $\mbox{\it WICM}_{\Omega}$ 
are not semilinear, unless they are finite.
\end{thm}
%%
This does not mean, however, that these languages are complex. 
First, they can be parsed using a Turing machine with linearly 
bounded space. Hence, they are context--sensitive. Moreover, 
the parsing complexity is even polynomial.
%%
\begin{thm}[Ebert]
Membership in $\mbox{\it ICM}_{\Omega}$ and 
$\mbox{\it WICM}_{\Omega}$ can be decided in 
$O(n^{3/2} \log_2 n)$ time on a deterministic multihead 
Turing machine with linearly bounded space, or 
$O(n^{5/2} \log_2 n)$ on a single head Turing machine 
with linearly bounded space.
\end{thm}
%%
Context--free languages can be parsed in $O(n^{\log_2 7})$ 
steps on a multi--head Turing machine. The exponent is larger
than $2.7$, so the word marking languages are faster 
to recognize than many context--free languages. Polish Notation 
is however still faster. It is recognizable in linear time on 
a deterministic, linearly space bounded two--head Turing machine. 

The strategy of proof is to first order the blocks lexicographically 
(this takes $O(n^{3/2} \cdot \log_2 n)$ time, using efficient sorting 
techniques, for example Merge Sort). Compliance with the conditions is 
then verified in linear time. Another strategy is as follows. It 
takes time linear in the input to construct a semantic representation 
on the basis of a parse using the above grammar. Since this grammar is 
deterministic, the translation is done in overall linear time. The 
conditions can be checked on the semantics as well. For 
$\mbox{\it ICM}_{\Omega}$ there is even a completely semantic 
procedure. Namely, a string is in $\mbox{\it ICM}_{\Omega}$ iff its 
semantics can be reduced to a single term using a step by step 
elimination of equations. This gives another way of checking 
membership in $\mbox{\it ICM}_{\Omega}$. The two methods 
are of the same complexity. Notice also that the merge operation 
in this semantics is of very low complexity: it is linear in 
the length of the input structures, if the case stacks are 
implemented as pointer structures. The set of all case stacks 
forms a tree rooted at $\circ$. Substitution is nothing 
but putting one more cell at the root of the tree. 
