injections.tex

\documentclass{article}
\usepackage{combelow}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{xcolor}
\usepackage{enumitem}

\usepackage{hyperref}

%\renewcommand\emph[1]{{\bf #1}}

\newcommand\comment[2]{\par\noindent\color{red}#1: #2\color{black}\par\noindent}
\newcommand\dl{\comment{Dorel}}

\theoremstyle{definition}
\newtheorem{example}{Example}[section]

\theoremstyle{definition}
\newtheorem{definition}{Definition}[section]

\theoremstyle{definition}
\newtheorem{remark}{Remark}[section]

\theoremstyle{theorem}
\newtheorem{theorem}{Theorem}[section]

\theoremstyle{theorem}
\newtheorem{fact}{Fact}[section]

\theoremstyle{theorem}
\newtheorem{lemma}{Lemma}[section]

\newcommand{\poly}[2]{\texttt{#1}\{#2\}}
\newcommand{\newpoly}[1]{\expandafter\newcommand\expandafter{\csname#1\endcsname}{\poly{#1}}}
\newpoly{Map}
\newpoly{MapInt}
\newpoly{List}
\newpoly{cons}
\newcommand{\Sort}[1]{\textit{sort}\{#1\}}
%\newcommand{\Map}[1]{\text{Map}\{#1\}}
%\newcommand{\List}[1]{\text{List}\{#1\}}
%\newcommand{\cons}[1]{\text{cons}\{#1\}}
\newcommand{\newkeyword}[1]{\expandafter\newcommand\expandafter{\csname#1\endcsname}{\texttt{#1}}}
\newkeyword{inj}
\newkeyword{syntax}
\newcommand{\KWsymbol}{\texttt{symbol}}
\newcommand{\sort}{\texttt{sort}}
\newcommand{\axiom}{\texttt{axiom}}
\newkeyword{String}
\newkeyword{Int}
\newkeyword{Exp}

\title{On Injections}
\author{Grigore Ro\cb{s}u}
\begin{document}
\maketitle

\section{Introduction}

\section{Parametric Productions}

Recall parametric productions (written using frontend syntax):
\[\syntax\{P_1,\ldots,P_k\}\ N ::= T_1 N_1 \ldots T_n N_n T_{n+1}\]
The non-terminals \(N,N_1,\ldots,N_n\) can make use of parameters
\(P_1,\ldots,P_k\).
We also discussed about allowing the parameters
to be optionally specified among the terminals \(T_1,\ldots,T_n,T_{n+1}\)
and nonterminals \(N_1,\ldots,N_n\), e.g. \(T_1\{P_1\}N_1\ldots\),
but that is irrelevant for this discussion.
The implicit semantics of parametric productions is that of infinitely
many instances, one for each concrete parameter instance.
In KORE, to each production like above we associate a parametric symbol:
\[\sigma\{P_1,\ldots,P_k\}(N_1,\ldots,N_n):N\]

\section{Injections: The Problem}
Now let's consider the special case of injections,
which correspond to productions like above where
\(n=1\) and \(T_1=T_2=\epsilon\), that is,
\[\syntax\ \{P_1,\ldots,P_k\} N::=N_1\]
As a concrete example, assume the following parametric definitions:
\begin{align*}
&\sort\ \Map{K,V}\\
&\syntax\{V\}\ \MapInt{V} ::= \Map{\Int,V}
\end{align*}
\dl{A minor observation. Even if we use curly brackets for the list of parameters, their order in the list is important for instantiation, Otherwise, we should write something like \(\Map{K\Rightarrow \Int, V\Rightarrow V}\). If the parameters order matters, then their names in the ``sort'' definition/production does not matter.}
\dl{The second syntax production can be simply written as
\[\syntax\{V\}\ \texttt{MapInt} ::= \Map{\Int, V}\]
There is no reason to specify the list of parameters twice; always the lhs will depend on all the parameters of the production. I.e.,
\[\syntax\{P_1,\ldots,P_k\}\ N ::= \ldots\]
is equivalent to
\[\syntax\{P_1,\ldots,P_k\}\ N\{P_1,\ldots,P_k\} ::= \ldots\]}
By abuse of notation, let
\[\inj_{N_1,N}\{P_1,\ldots,P_k\}(N_1):N\]
be the parametric symbol corresponding to the generic injection
production above.
Note that, for now, \(\inj\) is \emph{not} parametric in the two sorts,
each \(\inj_{N_1,N}\) is a separately-defined ordinary symbol.
For our example,
\[\inj_{\Map{\Int,V},\MapInt{V}}\{V\}(\Map{\Int,V}): \MapInt{V}\]
\comment{Brandon}{if each way of subscripting \(\inj\) is a distinct non-parametric
symbol, how do we have parameter \(V\) }
Injection symbols are different from ordinary symbols, in that they
inherit an expected semantics of ``injections''.
For example, take an instance \(\theta\) of the parameters
\(P_1,\ldots,P_k\).
Then any element of sort \(\theta(N_1)\) is expected to also be found
among the elements of sort \(\theta(N)\), possibly renamed.
\dl{It is not clear for me how the renaming can be involved here. I think that \(P_1,\ldots,P_k\) are the only parameters allowed in the production definition.}
Moreover, such injections are expected to be consistent.

\begin{example}\label{consistency-parallel}
For example, assume another production
\[\syntax\{Q_1,\ldots,Q_\ell\}\ M::=M_1\]
with corresponding injection
\[\inj_{M_1,M}\{Q_1,\ldots,Q_\ell\}(M_1):M\]
such that there is some instance \(\rho\) of the parameters
\(Q_1,\ldots,Q_\ell\) with \(\rho(M_1) = \theta(N_1)\) and
\(\rho(M) = \theta(N)\).
\dl{We should formally define what exactly means an equality $\rho(M)=\theta(N)$. Here is an example showing how I understand it:
\\
We suppose that the above example is written as follows:
\begin{align*}
&\sort\ \Map{K,V}\\
&\syntax\{V'\}\ \MapInt{V'} ::= \Map{\Int, V'}
\end{align*}
(this could be a particular example when the parameter $V$ is renamed as $V'$).
If \(\theta(K)=\Int\), \(\theta(V)=\String\),
and \(\rho(V')=\String\) then \(\theta(\Map{K,V})=\rho(\Map{\Int,V'})\).
\\
Supposing that the grammar include only these productions, can we deduce that
\(\theta({\tt Map}\{K,V\})=\rho(\MapInt{V'})\)?
This could makes sense since \(\MapInt{V'}\) is the smallest set including \(\Map{\Int,V'}\).
}
\comment{Brandon}{
I think this simply means applying the substitution gives identical instantiations
of the same parameterized sort.
}
Then we certainly want the following to hold:
\[\inj_{N_1,N}\{\theta(\bar{P})\}(\varphi:\theta(N_1))
 = \inj_{M_1,M}\{\rho(\bar{Q})\}(\varphi:\rho(M_1))\]
\end{example}

\begin{example}\label{consistency-compose}
As another example, assume productions
\begin{align*}
\syntax\{A_1,\ldots,A_a\}\ X & ::=X_1\\
\syntax\{B_1,\ldots,B_b\}\ Y_1 & ::=Y_2\\
\syntax\{C_1,\ldots,C_c\}\ Z_1 & ::=Z_2\\
\end{align*}
such that there are some parameter instances
\(\alpha\), \(\beta\), and \(\gamma\) with
\(\alpha(X_1) = \beta(Y_1)\), \(\alpha(X) = \gamma(Z)\),
and \(\beta(Y_2) = \gamma(Z_2)\).
Then we certainly want
\[\inj_{X_1,X}\{\alpha(\bar{A})\}(
  \inj_{Y_2,Y_1}\{\beta(\bar{B})\}(\varphi:\beta(Y_2)))
 = \inj_{Z_2,Z}\{\gamma(\bar{C})\}(\varphi:\gamma(Z_2))\]
\dl{The rule we can learn from this example is: ``the transitivity of injections does make sense (only?) on the (legal) sort instances''.}
\end{example}

\begin{example}\label{consistency-lifting}
We also want parametric sorts to lift subsorts.
That is, if
\[\inj_{N_1,N}\{P_1,\ldots,P_k\}(N_1):N\]
is an injection parametric symbol corresponding to production
\[\syntax\{P_1,\ldots,P_k\}\ N::=N_1,\]
then we also want to have parametric symbols
\[\inj_{\Sort{N_1,\ldots},\Sort{N,\ldots}}
   \{P_1,\ldots,P_k,\ldots\}
    (\Sort{N_1,\ldots}) : \Sort{N,\ldots}\]
for any other parametric sort \(\Sort{\_\!\_,\ldots}\).
\dl{Here is an instance of the above rule. Suppose that \(\Sort{\_\!\_,\ldots}\) is
\[\syntax\{S\}\ \List{S}\]
then we have
\[\inj_{\List{\Map{\Int,V}},\List{\MapInt{V}}}(\List{\MapInt{V}}):\List{\Map{\Int,V}}\]
The rule we can learn from this example is: ``the injections propagate among the parameterized sorts''. Shouldn't we consider here only the cases of instances, similar to the transitivity?
}
\end{example}

\begin{example}\label{consistency-parametric}
The situation is actually a lot more complex!
The injection symbols need to be consistent not only among
themselves, but also w.r.t. other symbols that end up
being overloaded due to parametricity.
Consider, for example:
\begin{align*}
&\syntax\ \Exp::=\Int\\
\syntax\{S\}\ \List{S}::=\texttt{cons}(S,\List{S})
\end{align*}
or in KORE:
\begin{align*}
&\sort\ \List{S}\\
&\KWsymbol\ \inj_{\Int,\Exp}(\Int):\Exp\\
&\KWsymbol\ \cons{S}(S,\List{S}):\List{S}
\end{align*}
Then we need to add the following axiom
\begin{multline*}
\inj_{\List{\Int},\List{\Exp}}(\cons{\Int}(\varphi:\Int,\psi:\List{\Int})) \\
 = \cons{\Exp}(\inj_{\Int,\Exp}(\varphi),\inj_{\List{\Int},\List{\Exp}}(\psi))
\end{multline*}
\dl{The rule we can learn from this example is: ``if the injections and a parametric symbol are \emph{well-defined (legal)} on both the arguments and the result, then they may
interchange (or, in other words, the injection propagates through parametric symbols).
}
\end{example}

\begin{example}\label{consistency-parametric-arg-only}
But what if the result of the parametric symbol
does not depend on the parameter, that is, say
\[\KWsymbol\ \poly{length}{S}(\List{S}):\Int\]
Then we need to add an axiom as follows
\[\poly{length}{\Int}(\varphi:\List{\Int})
= \poly{length}{\Exp}(\inj_{\List{\Int},\List{\Exp}}(\varphi))\]
\dl{This example is a particular case of the previous one if we consider
\[\inj_{S,S}(\varphi)=\varphi\]
}
\end{example}

\begin{example}\label{consistency-parametric-result-free}
On the other hand, if the result of a symbol depends on
a parameter that is not constrained by its arguments,
then we cannot add any injection axioms.
For example, consider
\[\KWsymbol\ \poly{cast}{P_1,P_2}(P_l1):P_2\]
While it makes sense to add axioms like
\[\inj_{\Int,\Exp}(\poly{cast}{\Int,\Int}(\varphi:\Int)
= \poly{cast}{\Int,\Exp}(\varphi)\]
you cannot instantiate \(P_2\) with everything, e.g., you cannot add
\[\inj_{\Int,\String}(\poly{cast}{\Int,\Int}(\varphi:\Int)
= \poly{cast}{\Int,\String}(\varphi)\]
because \(\Int\) is not a subset of \(\String\).
\dl{The rule we can learn from this example is: ``we have to consider only those injections defined on sort instances that are in a \emph{subsort partial-order relation}''.
}
\end{example}

\section{Injections: The Proposal}
So things are really tricky.
What I propose is to add the following axioms for now,
and \emph{in parallel} to have somebody really interested in this
problem study it in depth.
Note that knowledge of order-sorted algebra will be a big plus here!

\begin{enumerate}[label=(\arabic*)]
\item\label{assume-inj}
Define/assume one parametric symbol
\[\KWsymbol\ \inj\{P_1,P_2\}(P_1):P_2\]
This is what we do now, too.
Note that this is \emph{different} from having one \(\inj\)
symbol for each subsorting.
In particular, for the subsorting discussed in the previous section,
\[\syntax\{V\}\ \MapInt{V}::=\Map{\Int,V}\]
instead of the injection label we had there, namely
\[\KWsymbol\ \inj_{\Map{\Int,V},\MapInt{V}}\{V\}(\Map{\Int,V}):\MapInt{V}\]
we refer to this subsorting using the generic injection
\[\inj\{\Map{\Int,V},\MapInt{V}\}.\]
I do not know how to state that a subsorting has been declared,
or if it is needed, so I postpone this aspect for now.

\item\label{axiom-total-function-like}
Axiomatize that \(\inj\) is total-function-like, because otherwise we will not
be able to prove that \(1+x\), etc., are ``terms'':
\dl{{\(1 + \inj\{\texttt{Id}, \Int\}(x)\)}?}
\[\axiom\{P_1,P_2\}\ \forall x:P_1.\exists y:P_2.\inj\{P_1,P_2\}(x)=y\]
\dl{What if we want that an identifier not to be a \texttt{Bool} and an \Int{} in the same time?\\
\[(\forall X)\neg (\inj\{\texttt{Id},\texttt{Bool}\}(X)
  \land \inj\{\texttt{Id},\texttt{Int}\}(X))\]}
I do not think that we want to axiomatize that \(\inj\) is an
\emph{injective} function, because we may want to inject sets of larger
cardinalities (e.g.identifiers) into sets of smaller cardinalities
(e.g., \texttt{Bool}: \((x\ \text{or}\ y)\) and \(x=x\), etc.).
\dl{I do not understand the above example. If $x$ and $y$ are two different identifiers, then their injections denote different \texttt{Bool} names.}

\item\label{axiom-reflexive}
Axiomatize that \(\inj\) is reflexive:
\[\axiom\{S\}\ \inj\{S,S\}(\varphi:S) = \varphi\]

\item\label{axiom-transitive}
Axiomatize that injections compose (or are transitive):
\[\axiom\{P_1,P_2,P_3\}\ \inj\{P_2,P_3\}(\inj\{P_1,P_2\}(\varphi:P_1))
 = \inj\{P_1,P_3\}(\varphi)\]

\item\label{axiom-parametric-symbol}
And here is an aggressive axiom, but which I dare to claim is OK:
Unrestricted propagation through parametric symbols.
For each symbol \(\sigma\{P_1,\ldots,P_k\}(S_1,\ldots,S_n):S\)
where \(P_1,\ldots,P_k\) are parameters and
\(S_1,\ldots,S_n,S\) are sorts potentially parametric in
\(P_1,\ldots,P_k\), add axiom
\begin{multline*}
\axiom\{P_1,\ldots,P_k,P'_1,\ldots,P'_k\}\\
\inj\{S,S'\}(\sigma\{P_1,\ldots,P_k\}(\varphi_1:S_1,\ldots,\varphi_n:S_n)\\
= \sigma\{P'_1,\ldots,P'_k\}(\inj\{S_1,S'_1\}(\varphi_1),\ldots,\inj\{S_n,S'_n\}(\varphi_n))
\end{multline*}
\end{enumerate}

OK, now I can hear you guys yelling at me,
``what the heck is this? It is too aggressive!''.
In particular, that it admits nonsensical properties to be proven,
like the one for the cast symbol in Example~\ref{consistency-parametric-result-free} above.
And I would agree, but I do believe that we
should either disallow symbols like in Example~\ref{consistency-parametric-result-free}
above, or otherwise give a serious warning.
Note that \(\inj\) itself is such a symbol ;-).

What makes me believe that axiom \ref{axiom-parametric-symbol}
above is OK is that it corresponds to the main requirement of
order-sorted algebra, namely \emph{regularity}.
Let me elaborate.

\subsection{Order-Sorted Regularity (or pre-regularity?)}
In Order-Sorted Algebra(OSA), you have a partial order \((S,\le)\) on sorts \(S\).
Symbols are allowed to be overloaded, but they must obey the
\emph{regularity} property in order for things to make sense
mathematically:

\begin{definition}
\((S,\Sigma')\) is regular iff for any
\(\sigma:s_1\times\cdots\times s_n \rightarrow s\) and
\(\sigma:s'_1\times\cdots\times s'_n \rightarrow s'\) such that
\(s_1\le s'_1,\ldots,s_n\le s'_n\) we have \(s \le s'\).
\end{definition}

In our setting, since we disallow overloaded
symbols except for parametric ones, and since we build
our subset relation constructively through
parametric sorts starting with a base subsort relation,
I dare to claim two things:
\begin{enumerate}[label={(\alph*)}]
\item That the axiom in \ref{axiom-parametric-symbol} above corresponds to
regularity in OSA, which is therefore a
reasonable thing to have;
\item Under a mild restriction, that in each
\[\KWsymbol\ \sigma\{P_1,\ldots,P_n\}(S_1,\ldots,S_n):S\]
the sorts \(S_1,\ldots,S_n\) already refer to \emph{all} parameters
\(P_1,\ldots,P_k\), we can show that the resulting order-sorted
signature, whose only overloaded symbols are the parametric ones, is
\emph{regular}.
The ``resulting'' partial order on sorts is the least relation \(\le\)
closed under the following.
\begin{itemize}
\item \(\syntax\ S'::=S\) implies \(S \le S'\)
\dl{$S$ and $S'$ basic sorts?}
\comment{Brandon}{Good point, what happens if these are instances of parametric sorts?}
\item reflexive and transitive
\item If \(s_1\le s'_1,\ldots,s_k\le s'_k\) and
\(\Sort{P_1,\ldots,P_k}\) is a parametric sort,
then \(\Sort{s_1,\ldots,s_k} \le \Sort{s'_1,\ldots,s'_k}\).
\end{itemize}
\end{enumerate}

\dl{
The following definitions are from~\cite{osa}:\\
\begin{definition}
An \emph{order-sorted signature} is a triple $(S,\le,\Sigma)$ such that $(S,\Sigma)$ is a many-sorted signature, $(S, \le)$ is a poset, and the operations satisfy the following \emph{monotonicity condition}:
\[
\sigma\in\Sigma_{w,s}\cap\Sigma_{w',s'}\textrm{~and~}w\le w'\textrm{~imply~}s\le s'.
\]
\end{definition}

\begin{remark}
If $w=s_1\ldots s_m$ and $w'=s'_1\ldots s'_n$ then $w\le w'$ iff $m = n$ and $s_i\le s'_i$ for $i=1,\ldots,n$.
\end{remark}

\begin{definition}
An order-sorted signature $(S,\le,\Sigma)$ is \emph{regular} iff
\begin{itemize}
\item given $\sigma\in\Sigma_{w',s'}$ and $w_0\le w'$ there is a least rank $\langle w,s\rangle\in S^*\times S$ such that $w_0\le w$ and $\sigma\in\Sigma_{w,s}$.
\end{itemize}
An order-sorted signature $(S,\le,\Sigma)$ is \emph{pre-regular} iff
\begin{itemize}
\item given $\sigma\in\Sigma_{w',s'}$ and $w_0\le w'$ there is a least sort $s\in S$ such that  $\sigma\in\Sigma_{w,s}$ for some $w$ with $w_0\le w$.
\end{itemize}

\end{definition}

\begin{fact}\cite{osa}\label{fact:reg}
Let  $(S,\le,\Sigma)$ be an order-sorted signature such that $(S,\le)$ is \emph{coNoetherian}, i.e., there is no strictly decreasing infinite chain $s_1>s_2>s_3>\cdots$.
Then $(S,\le,\Sigma)$ is regular iff whenever $\sigma\in \Sigma_{w',s'}\cap\Sigma_{w'',s''}$ and $w_0\le w',w''$ then there is some $w\le w',w''$ such that $\sigma\in\Sigma_{w,s}$ and $w_0\le w$.
\end{fact}

\begin{definition}
Let  $(S,\le,\Sigma)$ be an order-sorted signature. An \emph{ $(S,\le,\Sigma)$-algebra} is a many-sorted $(S,\Sigma)$-algebra $M$ satisfying:
\begin{enumerate}
\item $s\le s'$ implies $M_s\subseteq M_{s'}$;
\item $\sigma\in \Sigma_{w',s'}\cap\Sigma_{w'',s''}$ and $w'\le w''$ implies $M_\sigma:M_{w'}\to M_{s'}$ equals  $M_\sigma:M_{w''}\to M_{s''}$ on $M_{w'}$,
\end{enumerate}
where if $w=s_1\ldots s_n$ then $M_w=M_{s_1}\times\cdots\times M_{s_n}$.
\end{definition}
I think that the "aggressive equation"~\ref{ax:aggressive} formalizes in fact the second condition in the above definition.
}

\dl{
Now we sketch out how a front-end grammar $G$ defines an order-sorted signature $(S^\textrm{osa},\le, \Sigma^\textrm{osa})$:
\begin{enumerate}
\item each parametric sort declaration
\[\sort\ N\{P_1,\ldots,P_k\}\]
together with each parameter valuation $\theta : \{P_1,\ldots,P_k\}\to S^\textrm{osa}$ i
define a sort $\theta(N)=N\{\theta(P_1),\ldots,\theta(P_k)\}$ in $S^\textrm{osa}$.
\\
If $k=0$ then there is a unique function  $\theta : \emptyset\to S^\textrm{osa}$ and we identify $\theta(N)$ with $N$ (or $N\{\}$?);
\item each parametric production $\pi$
\[\syntax\{P_1,\ldots,P_k\}\ N ::= T_1 N_1 \ldots T_n N_n T_{n+1}\]
where $n>1$ or at least $T_i$ is diferent from "", and each parameter valuation
$\theta : \{P_1,\ldots,P_k\}\to S^\textrm{osa}$ define
\begin{enumerate}
\item a sort $\theta(N)=N\{\theta(P_1),\ldots,\theta(P_k)\}$ in $S^\textrm{osa}$ and
\item a symbol $\sigma_\pi$ in $\Sigma^\textrm{osa}_{\theta(N_1)\ldots\theta(N_n),\theta(N)}$.
\end{enumerate}
Similar to above, if $k=0$ we identify $\theta(N)$ with $N$;
\item each parametric production
\[\syntax\{P_1,\ldots,P_k\}\ N ::= N_1\]
and each parameter valuation $\theta : \{P_1,\ldots,P_k\}\to S^\textrm{osa}$ define
\begin{enumerate}
\item a sort $\theta(N)=N\{\theta(P_1),\ldots,\theta(P_k)\}$ in $S^\textrm{osa}$ and
\item a relation $\theta(N_1)\le \theta(N)$.
\end{enumerate}
Again, if $k=0$ we identify $\theta(N)$ with $N$.
 \item each parametric production
\[\syntax\{P_1,\ldots,P_k\}\ N ::= \ldots\]
and each pair of parameter valuations $\theta,\theta' : \{P_1,\ldots,P_k\}\to S^\textrm{osa}$ such thar $\theta(P_i)\le \theta'(P_i)$, for $i=1,\ldots,n$, define
\begin{enumerate}
\item a relation $\theta(N)\le \theta'(N)$.
\end{enumerate}
\item $\le$ is extended such that it is reflexive and transitive.
\end{enumerate}

In order to show that $(S^\textrm{osa},\le, \Sigma^\textrm{osa})$ is regular, we need a formal definition for the nonterminals occurring in a parametric production.
\begin{definition}
Let $P$ denote the set of parameters $P=\{P_1,\ldots,P_k\}$. A \emph{$P$-sort-term} is inductively defined as follows:
\begin{itemize}
\item a simple sort name (identifier) is a $P$-sort-name;
\item a parameter $P_i$ is a $P$-sort-name;
\item if $N\{Q_1,\ldots,Q_\ell\}$ is a parametric sort name and $N_1,\ldots,N_\ell$ are $P$-sort-names, then $N\{N_1,\ldots,N_\ell\}$ is a $P$-sort-name.
\end{itemize}
\end{definition}

In a parametric production
\[\syntax\{P_1,\ldots,P_k\}\ N ::= T_1 N_1 \ldots T_n N_n T_{n+1}\]
we have:
\begin{enumerate}
\item $N$ is a simple sort name (identifier);
\item $N_i$ is a $\{P_1,\ldots,P_k\}$-sort-name, $i=1,\ldots,k$.
\end{enumerate}
\begin{lemma}
Let $N$ be a $P$-sorted-term, where $P=\{P_1,\ldots,P_k\}$ denotes the set of parameters occuring in $N$. If $\theta,\theta':P\to S^{\rm osa}$ such that $\theta(N)\le\theta'(N)$, then $\theta(P_i)\le \theta(P'_i)$ for $i=1,\ldots,n$.
\end{lemma}
\begin{proof}
By structural induction on $N$.
\end{proof}

I do not know yet whether the following theorem holds and, if yes, how to prove it.
\begin{theorem}
Let $G$ be a input front-end grammar and $(S^\textrm{osa},\le, \Sigma^\textrm{osa})$ the order-sorted signature associated to $G$ as above.
Then $(S^\textrm{osa},\le, \Sigma^\textrm{osa})$ is regular.
\end{theorem}
%\begin{proof}
%The relation $\le$ is obviously coNoetherian, so it is enough to show that the hypotheses of Fact~\ref{fact:reg} hold. Let $\sigma\in \Sigma^\textrm{osa}_{w',s'}\cap\Sigma^\textrm{osa}_{w'',s''}$ and $w_0\le w',w''$. Since the only overloaded symbols are those corresponding to instances of a syntax production, it follows that there are a production $\pi$
%\begin{alltt}
%    syntax \(\{P\sb{1},\ldots,P\sb{k}\} N ::= T\sb{1}N\sb{1}\ldots T\sb{n}N\sb{n}T\sb{n+1} \)
%\end{alltt}
%and parameter valuations $\theta',\theta'':\{P\sb{1},\ldots,P\sb{k}\}\to S^\textrm{osa}$  such that $\sigma=\sigma_\pi$, $w'=\theta'(N_1)\ldots\theta'(N_n)$, $s'=\theta'(N)$, $w''=\theta''(N_1)\ldots\theta''(N_n)$, and $s''=\theta''(N)$.
%\end{proof}

Having the order-sorted signature $(S^\textrm{osa},\le, \Sigma^\textrm{osa})$ associated to an input grrama $G$, it is quite easy to define a ML theory $(S,\Sigma, F)$ encoding the order-sorted one:
\begin{enumerate}
\item $S=S^\textrm{osa}$ (without partial order relation);
\item each overloaded symbol $\sigma\in \theta(N_1)\ldots\theta(N_n), \theta'(N)$ becomes a parametric one: $\sigma\{\theta(N_1)\ldots\theta(N_n), \theta'(N)\}\in \theta(N_1)\ldots\theta(N_n), \theta'(N)$
\item injections describe the partial order relation: $\inj\{\theta(N),\theta(N')\}\in\Sigma_{\theta(N),\theta(N')}$ iff $\theta(N)\le \theta(N')$;
\item the axioms $F$ are the above ones (perhaps with a small different notation).
\end{enumerate}
}

\begin{thebibliography}{ABC99a}

\bibitem[GM92]{osa}
Joseph A. Goguen and José Meseguer. 1992.
\newblock {\em Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations.}
\newblock Theor. Comput. Sci. 105, 2 (November 1992), 217-273.

\end{thebibliography}

\end{document}