\section{The language \tgentzen{}}\label{tgentzen}

We now turn to a discussion of \tgentzen, a concrete \tcc{}
programming language. Subsequently, we shall examine several
programming idioms in \tgentzen, and discuss a simple
implementation.

\paragraph{Syntax.} 
The syntax of the language is summarized in
Table~\ref{tgentzen-table}. In general, \Prolog{} lexical and
syntactic conventions are followed. For technical reasons,
\tgentzen{} source programs are prevented from using the functor
{\tt '\_'/2}; this is reserved for internal use. 

The syntax {\tt \{C\}} is used to say that the constraints
(atomic formulas) in {\tt C} are to be added to the store. The
syntax {\tt C \then A} is used for $\nowt C \then A$, ${\tt C
\leadsto A}$ for $\nowe C \else A$.

Parametric asks are used to communicate ``data'' with signals:
they allow an agent to output in the store an atom with argument
structure (e.g. {\tt b(2,s)}), and another agent to explicitly
recover the values: e.g., the agent {\tt X\$Y\$(b(X,Y) \then A)}
will cause the generation of the agent $\tt A[X \mapsto 2, Y
\mapsto s]$. For simplicity of implementation, we require that
all the existentially and universally quantified \tgentzen{}
variables occurring in a clause are distinct \Prolog{} variables,
and distinct from variables occurring in the head of a
clause.\footnote{Thus, for example, the body $\tt X\Hat A,
X\Hat B$ is considered syntactically ill-formed, as is the clause
$\tt p(a,X) :: f(X), X\Hat A$.}

The syntax {\tt [A1, \ldots, An]} is used to signify the
parallel composition of the agents {\tt A1}, \ldots, {\tt An},
for $\tt n \geq 0$. In particular, {\tt []} stands for \Skip.

Using ``;'', an agent may check whether the current store entails
one of a set of constraints (Positive Ask), or does not entail
each of a set of constraints (Negative Ask). 


\paragraph{Semantics.}
\tgentzen{} allows a somewhat more liberal syntax for procedure
declarations than we have discussed in Section~\ref{tcc} for  the
general \tcc{} framework. The syntax is motivated by programming
considerations --- in particular, the conventions we adopt below
allow for a simple and succinct meta-interpreter for the language. 

\tgentzen{} allows multiple clauses for a procedure, and allows a
clause head to contain (non-variable) terms.  In the operational
semantics, the first clause whose head can be instantiated to
match the call is chosen for procedure reduction. 

It is easy to transform any such program into a program that
satisfies the procedure declaration syntax for general \tcc{}
languages. Assume the program has $\tt k$ clauses {\tt p(ti1, \ldots,
tin)::Ai}, for $\tt i \in 1\ldots k$. Assume further that all the
variables appearing in clause head {\tt i} are distinct from
those appearing in clause head {\tt j}, and from the variables
{\tt X1, \ldots, Xn}. The new program contains a single clause
for {\tt p/n}:

\begin{ccprogram}
\agent  p(X1, X2, \ldots, Xn) ::
     \[V1\$(C1 -> A1),
      V2\$(C2 -> A2), 
      \ldots
      Vk\$(Ck -> Ak)\]..
\end{ccprogram}
where
\begin{itemize}
\item  $\tt C1 = D1$, 
\item $\tt C2 = (D2, \neg \exists V1.D1)$, 
\item $\tt C3 = (D3, \neg \exists V2.D2, \neg \exists V1. D1)$ 
\item \ldots 
\item  $\tt Ck = (Dk, \neg \exists V1. D1, \ldots, \neg \exists
  V(k-1).D(k-1))$,
\end{itemize}
\noindent and $\tt Di = (X1 \doteq ti1, X2 \doteq ti2, \ldots Xn \doteq
tin)$.  Here, the usual axioms for equality (Clark's equality
theory) are understood to be in force for $\doteq$. However the
store is not allowed contain any $\doteq$ assertions. Hence for a
particular call {\tt p(s1, \ldots, sn)}, each equality ${\tt sj
\doteq tij}$ can be evaluated ``instantaneously''. There are no
other agents running simultaneously who can cause more equality
assertions to be generated, hence there is no need to ``suspend''.
Either the conditions for a particular clause are applicable or
not.

Thus, given the program:
\begin{ccprogram}
\agent   p(a(Y)) :: q(Y)..
\agent   p(a(Y)) :: s(Y)..
\agent  p(X)    :: r(X)..
\end{ccprogram}
\noindent the goal {\tt p(b)} will reduce to {\tt r(b)}, the goal {\tt p(a(1))} to
{\tt q(1)} (not  {\tt s(1)}, and not {\tt [s(1),q(1)]}). 

\paragraph{Other aspects.}
Three other aspects of \tgentzen{} relevant to (meta-) programming
should be pointed out.

First, some rudimentary arithmetic and communication abilities
are provided through Ask and Tell operations. Conceptually, one imagines
that the store contains the infinite collection of assertions
about the extension of the relevant arithmetic relations (e.g,
{\tt 3 > 2}, {\tt 2 = 2}, etc.). Thus, the program fragment {\tt
X\$(a(X), X > 3 \then proc(X))} will invoke {\tt proc} only if the
store contains an atom {\tt a(N)} where {\tt N} is a number great
than {\tt 3}.  An ersatz ask-predicate {\tt read(X)} is provided
to input (synchronously) a term from an input channel.
Conceptually, one imagines that an external agent places the atom
{\tt read(t)} in the store, if {\tt t} is the term returned by
the read operation. Conversely, some output operations are
provided as Tell operations --- conceptually, these are thought
as being added to the store, and being read by and executed on by
some external agent. 


Second, each of the combinators:
\begin{verbatim}
   ({}/1, ->/2, ~>/2,next/1,$/2,^/2,[]/0,`.'/2,::/2) 
\end{verbatim}
are also data-constructors.  Hence a \tgentzen{} agent is also directly
representable as a \tgentzen{} data-structure. 

Third, it is assumed that the user program is available in the
store, as a collection of assertions of the form $\tt (\forall)
Head::Body$. Asks are allowed to query this database, with the
restriction that in all queries of the form {\tt t::s} in the
body of a clause $K$, all variables occurring in {\tt t} must
occur in the head of $K$. This ensures that by the time {\tt
t::s} has to be executed in the body of the clause, {\tt t} will
contain no uninstantiated universally quantified variables.  Such
queries can be implemented by merely doing a lookup of the
program stored in a \Prolog{} database, and returning the first
answer.\footnote{Without this restriction, the implementation
could be forced to return all possible instantiations of the
query. This can become complicated, given the semantics for
mutually exclusive clauses above.}

Thus, the following is a legal \tcc{} clause:
\begin{ccprogram}
\agent   tcc(Proc)    :: Body\$(Proc::Body -> tcc(Body))..
\end{ccprogram}
\noindent (and indeed is a crucial clause in the definition of a
meta-interpreter for \tgentzen, Section~\ref{meta-interp}).
Given a procedure call, say {\tt tcc(f(3))}, the effect of this
clause would be to determine the unique body, say {\tt B}  for the procedure
call {\tt f(3)}, and invoke {\tt tcc(B)}. 

The approach we have chosen to make the program available at
run-time is very conservative. Clearly, it is possible to think
of the program changing arbitrarily from one time-step to the
next, just as the store does. Indeed, conceptually the program
and the content of the store are identical --- a program happens
to have more logical structure in its formulas than the store
does. We leave the investigation of this line of approach for
future work.
 
\begin{table}
\begin{tabular}{|l|}
\hline
\begin{minipage}[t]{\columnwidth}
\begin{equation}
 \begin{array}{lllll}
\mbox{(Agents)}&    {\tt A} & {::=} & {\tt \{C\}} &\mbox{ --- Constraint Tells}\\
        && \alt & {\tt E \then A} &               \mbox{  --- Positive Ask}\\
         && \alt & {\tt (X_1, \ldots, X_n)\$E \then A} & \mbox{ --- Parametric (positive) Ask}\\   
         && \alt & {\tt E  \leadsto A}      &\mbox{        --- Negative Ask}\\
         && \alt &{\tt next{}\ A}        &\mbox{        --- Next}\\
         && \alt &{\tt (X_1,\ldots,X_n)\Hat A}           &\mbox{        --- Hiding}\\
         && \alt &{\tt abort}              &\mbox{ --- Process abortion}\\
         && \alt &{\tt [A_1, \ldots, A_n]} &\mbox{        --- Parallel composition}\\
         && \alt & {\tt p(t_1, \ldots, t_n)}&\mbox{        --- Procedure call}\\
\quad\\
 \mbox{(Tell-Constraints)}&     {\tt C}  & {::=}& {\tt c} &
 \mbox{--- Primitive constraint}\\
 && \alt & {\tt C,C} &\mbox{--- Conjunction}\\
\quad\\
 \mbox{(Ask-Constraints)}&     {\tt E}  & {::=}& {\tt c} &
 \mbox{--- Primitive constraint}\\
 && \alt & {\tt E,E} &\mbox{--- Conjunction}\\
&& \alt & {\tt E;E} &\mbox{ --- Disjunction}\\
\quad\\
\mbox{(Declarations)}&     {\tt D} & {::=}& {\tt p(t_1,\ldots,t_n)::A}  &\mbox{     --- Clause}\\
         && \alt & {\tt D.D} &\\
\quad\\
\end{array}
\end{equation}
Multiple declarations are allowed per procedure. The first to
match is selected.

The following defined agents are also accepted:
\begin{equation}
 \begin{array}{lllll}
\mbox{(Agents)}&   {\tt A} & {::= } & {\tt clock(A, B)} & \\
 &&        \alt & {\tt always(A)} &\\
 &&        \alt & {\tt whenever(C, A)}&\\
 &&        \alt & {\tt watching(C, A)}&\\
\end{array}
\end{equation}
\end{minipage}\\
\hline
\end{tabular}
\caption{Syntax for \tgentzen{}.}\label{tgentzen-table}
\end{table}
