\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}