programs.tex

%!TEX root = reference.tex
\chapter{Programs}
\label{programs}

This chapter focuses on the organization of programs using functions, procedures and other computational forms. Apart from program values themselves, a key concept is the \ntRef{ThetaEnvironment}. This is where many programs, types etc. are defined. \ntRef{ThetaEnvironment}s are also first-class values -- showing up as \ntRef{AnonymousRecord}s.


\section{Theta Environment}
\label{thetaEnvironment}
\index{theta environment}
\index{program declaration}

A \ntRef{ThetaEnvironment} consists of a set of definitions of types, programs and variables.

\begin{figure}[htbp]
\begin{eqnarray*}
\ntDef{ThetaEnvironment}&\arrow&\q{\{}\ntRef{Definition}\sequence{;}\ntRef{Definition}\q{\}}\\
\ntDef{Definition}&\arrow&\ntRef{TypeDefinition}\\
&\choice&\ntRef{Annotation}\\
&\choice&\ntRef{VariableDeclaration}\\
&\choice&\ntRef{FunctionDefinition}\\
&\choice&\ntRef{ProcedureDefinition}\\
&\choice&\ntRef{PatternAbstraction}\\
&\choice&\ntRef{Contract}\\
&\choice&\ntRef{Implementation}\\
&\choice&\ntRef{OpenStatement}\\
&\choice&\ntRef{ImportStatement}\\
&\choice&\ntRef{LocalAction}\\
\ntDef{LocalAction}&\arrow&\q{\{}\ntRef{Action}\sequence{;}\ntRef{Action}\q{\}}\\
&\choice&\q{assert} \ntRef{Condition}
\end{eqnarray*}
\caption{Theta Environment}
\label{statementFig}
\end{figure}

Many of the definitions in a\ntRef{ThetaEnvironment} define entities that may be recursive and mutually recursive.

\begin{description}
\index{type!definition}
\item[Type definition] is the definition of a type. See Section~\vref{typeDefinitions}.
\index{type!declaration}
\item[Type declaration] is a statement that defines the type of a variable or program. See Section~\vref{typeAnnotation}.
\index{variable!definition}
\item[Variable definition] is a statement that defines a variable and gives it a value. There are two forms of variable definition corresponding to a normal single assignment variable and a re-assignable variable. See Section~\vref{VariableDeclaration}.
\item[Function definition] 
\index{function!definition}is a group of equations that defines a function. See Section~\vref{equations}.
\item[Procedure definition]
\index{procedure!definition} is a statement that defines an action procedure. See Chapter~\vref{procedures}.
\item[LocalAction]
\index{actions!in a theta environment}
A \ntRef{LocalAction} is an action -- enclosed in braces -- that is performed prior to the bound expression of a \q{ThetaEnvironment}.

\item[Contract definition] 
\index{contract!definition}is a statement that defines a coherent collection of functions and procedures that may be associated with different types. See Section~\vref{		Definition}.
\item[Contract implementation] 
\index{contract!implementation}
is a statement that establishes that a particular type \emph{implements} a contract -- and gives the implementation. See Section~\vref{ContractImplementation}.
\item[Macro definition]
\index{macro!definition}
is a statement that indicates how source programs should be interpreted. See Appendix~\vref{MacroLanguage}. Macro statements may only appear at the \q{package}-level: they are not permitted within the body of a \q{let} expression, for example.
\end{description}

\subsection{Open Statement}
\label{openStatement}
\index{open statement@\q{open} statement}
\index{opening a record}
\index{record!opening}

The \ntRef{OpenStatement} takes a \ntRef{Record}-valued expression and `opens its contents' in a \ntRef{ThetaEnvironment}. It is analogous to an \ntRef{Import} of the record.

\begin{figure}[htbp]
\begin{eqnarray*}
\ntDef{OpenStatement}&\arrow&\q{open}\ \ntRef{Expression}
\end{eqnarray*}
\caption{Open Statement}
\label{openStatementFig}
\end{figure}

Any fields and types that are declared within the \ntRef{Expression}'s type become defined within the enclosing \ntRef{ThetaEnvironment}.
\begin{aside}
The existing scope rules continue to apply; in particular, if there is a name that is duplicated already in scope then a duplicate definition error will be signaled. 
\end{aside}

\begin{aside}
Normal type inference is not able to infer anything about the type of the \q{open}ed \ntRef{Expression}. Hence, this statement requires that the type of the expression is already known.
\end{aside}

For example, given the definition:
\begin{lstlisting}
def R is {
  type integer counts as elem
  fun op(X,Y) is X+Y
  def zero is 0
}
\end{lstlisting}
then we can \q{open} \q{R} in a \ntRef{LetExpression}:
\begin{lstlisting}
let{
  open R
  Z has type elem
  def Z is zero
} in Z
\end{lstlisting}
\begin{aside}
Although the \q{open} statement makes available the types and fields embedded in a record; existential abstraction still applies. In particular, in this case the fact that the \q{elem} type is manifest as \q{integer} within the record expression \q{R} is hidden.

The \q{elem} type (and the \q{zero} and \q{op} fields) are available within the \q{let}; but no information about what \q{elem} actually is is available.
\end{aside}

\subsection{Local Actions}
\label{localAction}
\index{Actions executed within a \ntRef{ThetaEnvironment}}
A local action is a sequence of actions -- enclosed in braces -- that are performed when the theta environment is first entered and before any dependent bound expressions are evaluated.

For example, in:
\begin{lstlisting}
traceF has type (integer)=>integer;
fun traceF(X) is 
  let{
    fun f(0) is 1
     |  f(XX) is XX*f(XX-1)
    {
      logMsg(info,"in theta environment");
    }
  } in f(X)
\end{lstlisting}
The action
\begin{lstlisting}
logMsg(info,"in theta environment")
\end{lstlisting}
is executed as part of `establishing' the \ntRef{ThetaEnvironment} prior to the function \q{f} being evaluated.

Local actions are useful for situations where proper initialization of the entries in the theta environment are more extensive than binding a variable to a value.
\begin{aside}
There is no predetermined order of execution of \ntRef{LocalAction}s. The compiler ensures that all the preconditions for the \ntRef{LocalAction} -- specifically definitions that are referenced by the \ntRef{LocalAction} -- are established prior to the execution of the action.
\end{aside}

\section{Functions and Equations}
\label{functions}

A function is a program for computing values; organized as a set of equations. 

\begin{figure}[htbp]
\begin{eqnarray*}
\ntDef{Function}&\arrow&\q{fun}\ \ntRef{Equation}\sequence{|}\ntRef{Equation}\\
\ntDef{Equation}&\arrow&\ntRef{EquationHead}\ [\ntRef{RuleGuard}\,]\ \q{is}\ \ntRef{Expression}\\
\ntDef{EquationHead}&\arrow&\ntRef{Identifier}\q{(}\,\ntRef{Pattern}\sequence{,}\ntRef{Pattern}\,\q{)}\\
\ntDef{RuleGuard}&\arrow&\q{default}\\
&\choice&\q{where}\ \ntRef{Condition}
\end{eqnarray*}
\caption{Functions}\label{functionFig}
\end{figure}

\begin{aside}
Functions and other program values are first class values; as a result they may be passed as arguments to other functions as well as being assigned as attributes of records.
\end{aside}

\label{equations}
An equation is a rule for deciding how to rewrite an expression into simpler expressions. Each equation consists of a \ntRef{Pattern} that is used to match the call to the function and a replacement expression. The left hand side of the function may also have a guard associated with it, this guard may use variables introduced in the pattern.

\begin{aside}
An equation is said to apply iff the patterns in the left hand side of the equation (including any \q{where} clauses) all match the corresponding actual arguments to the function application.
\end{aside}


\index{theta environment}
\noindent
Functions are defined in the context of a \ntRef{ThetaEnvironment} -- for example, in the body of a \q{let} expression (see Section~\vref{letExpression}), or at the top-level of a \q{package} -- see Section\vref{thetaEnvironment}.

It is not necessary for the equations that define a function to be contiguous within a \ntRef{ThetaEnvironment}. However, all the equations for a function must be present in the \emph{same} \ntRef{ThetaEnvironment}. 

\begin{aside}
Although equations do not need to be contiguous; it is recommended that they are written contiguously where possible. This helps to avoid a certain kind of error where equations seem to `go missing' but are just misplaced.
\end{aside}

\subsubsection{Type Safety}
The type safety of a function is addressed in stages. In the first place, we give the rules for individual equations:
\begin{prooftree}
\AxiomC{\typeprd{E}{\q{(}P\sub1,\ldots,P\subn\q{)}}{\q{(}t\sub1,\ldots,t\subn\q{)}}}
\AxiomC{\typeprd{E}{Ex}{T\sub{Ex}}}
\BinaryInfC{\typeprd{E}{F\q{(}P\sub1,\ldots,P\subn\q{) is }Ex}{\q{(}t\sub1,\ldots,t\subn\q{)=>T\sub{Ex}}}}
\end{prooftree}
If the equation has a guard \ntRef{Condition}, that that condition must be type satisfiable:
\begin{prooftree}
\AxiomC{\typeprd{E}{\q{(}P\sub1,\ldots,P\subn\q{)}}{\q{(}t\sub1,\ldots,t\subn\q{)}}}
\AxiomC{\typesat{E'}{C}}
\AxiomC{\typeprd{E''}{Ex}{T\sub{Ex}}}
\TrinaryInfC{\typeprd{E}{F\q{(}P\sub1,\ldots,P\subn\q{) where }C\q{ is }Ex}{\q{(}t\sub1,\ldots,t\subn\q{)=>T\sub{Ex}}}}
\end{prooftree}
where $E'$ is the original environment $E$ extended with the variable definitions found in the patterns $P\subi$ and $E''$ is $E'$ extended with the variables found in the condition $C$.

In fact this rule slightly understates the type safety requirement. For any statement in a theta environment we may also have:
\begin{prooftree}
\AxiomC{F\q{ has type }T\ $in$\ E}
\UnaryInfC{\typeprd{E}{F\sub{def}}{T}}
\end{prooftree}
where F\sub{def} is the set of statements that define F. I.e., the computed type of a function must agree with the declared type of the function.

\subsection{Evaluation Order of Equations}
\label{functionEvaluation}
\index{equations!evaluation order}
Using multiple equations to define a function permits a case-base approach to function design -- each equation relates to a single case in the function. When such a function is \emph{applied} to actual arguments then only one of the equations in the definition may apply.


Equations are applied in the order that they are written -- apart from any equation that is marked \q{default}. If two equations overlap in their patterns then the first equation to apply is the one used.

\subsection{Default Equations}
\label{defaultEquation}
\index{default equation@\q{default} equation}
\index{functions!default@\q{default} equation}

It is permitted to assign one of the equations in a function definition to be the \q{default} equation. An equation marked as \q{default} is guaranteed \emph{not} to be used if any of the non-default equations apply. Thus, a \q{default} equation may be used to capture any remaining cases not covered by other equations.

\index{patterns!variable pattern}
A \q{default} equation may not have a \q{where} clause associated with it, and furthermore, the patterns in the left hand-side should be generally be variable patterns (see Section~\vref{patternVariables}). 
\begin{aside}
In particular, it \emph{should} be guaranteed that a \q{default} equation cannot fail to apply.
\end{aside}

\subsection{Evaluation Order of Arguments}
\index{function application!evaluation order}

There is \emph{no} guarantee as to the order of evaluation of arguments to a function application. In fact, there is no guarantee that a given expression will, in fact, be evaluated.

\begin{aside}
The programmer should also \emph{not} assume that argument expressions will \emph{not} be evaluated!

In general, the programmer should make the fewest possible assumptions about order of evaluation.
\end{aside}

\subsection{Pattern Coverage}
\label{patternCoverage}
\index{patterns!coverage of}
Any given equation in a function definition need not completely cover the possible arguments to the function. For example, in
\begin{lstlisting}
F has type (integer)=>integer;
fun F(0) is 1
 |  F(X) is X*F(X-1)
\end{lstlisting}
the first equation only applies if the actual argument is the number \q{0}; which is certainly not all the \q{integer}s.

The set of equations that define a function also define a coverage of the potential values of the actual arguments. In general, the coverage of a set of equations is smaller than the possible values as determined by the type of the function.

If a function is \emph{partial} -- i.e., if the coverage implied by the patterns of the function's equations is not complete with respect to the types -- then the compiler may issue an incomplete coverage warning.

\begin{aside}
The programmer is advised to make functions \emph{total} by supplying an appropriate \q{default} equation. In the case of the \q{F}actorial function above, we can make the \q{default} case explicit as is shown in Program~\vref{factorialFun}.
\end{aside}

\begin{program}
\begin{lstlisting}
fact has type (integer)=>integer
fun fact(X) where X>0 is X*fact(X-1)
 |  fact(X) default is 1
\end{lstlisting}
\caption{Factorial Function\label{factorialFun}}
\end{program}

\subsection{Anonymous Function}
\label{anonymousFunction}
\index{anonymous function}
\index{expressions!function}

Anonymous functions are expressions of the form:
\begin{lstlisting}
(X) => X+Y
\end{lstlisting}
Anonymous functions may appear anywhere a function value is permitted.


\begin{figure}[htbp]
\begin{eqnarray*}
\ntDef{AnonymousFunction}&\arrow&\ntRef{TuplePattern}\ \q{=>}\ \ntRef{Expression}
\end{eqnarray*}
\caption{Anonymous Function}
\label{anonymousFunctionFig}
\end{figure}

\begin{aside}
If it desired to have a single-argument anonymous function that takes a tuple pattern then use double parentheses:
\begin{lstlisting}
((X,Y)) => X+Y
\end{lstlisting}
\end{aside}

For example, an anonymous function to add 1 to its single argument would be:
\begin{lstlisting}
(X) => X+1
\end{lstlisting}
Anonymous functions are often used in function-valued functions. For example in:
\begin{lstlisting}
addX has type (integer)=>((integer)=>integer);
fun addX(X) is (Y) => X+Y;
\end{lstlisting}
the value returned by \q{addX} is another function -- a single argument function that adds a fixed number to its argument.

\begin{aside}
Anonymous functions may reference free variables; but cannot be recursive.
\end{aside}


\subsubsection{Type Safety}
The type of an anonymous function is determined by the types of the argument patterns and the return type. Unlike named functions, anonymous functions are not explicitly typed.

\begin{prooftree}
\AxiomC{\typeprd{E}{A\sub1}{T\sub1}\sequence{\quad}\typeprd{E}{A\subn}{T\subn}}
\AxiomC{\typeprd{E}{R}{T\sub{R}}}
\BinaryInfC{\typeprd{E}{\q{(}A\sub1\sequence{,}{A\subn}\q{) => }R}{\q{(}T\sub1\sequence{,}T\subn\q{)=>}T\sub{R}}}
\end{prooftree}


\subsection{Overloaded Functions}
\label{overloadedFunctions}
The type of an overloaded function has a characteristic signature: it's type is universally quantified but with a constraint on the bound type variables.

For example, given the definition:
\begin{lstlisting}
fun dble(X) is X+X
\end{lstlisting}
the generalized type assigned to the \q{dble} variable is:
\begin{lstlisting}
for all t such that (t)=>t where arithmetic over t
\end{lstlisting}

As noted in Section~\vref{overloading}, the \q{dble} function is converted to a function with an explicit `dictionary' argument that carries the implementation of the \q{arithmetic} contract:
\begin{lstlisting}
fun dble(A) is let{
  fun dble'(X) is (A.+)(X,X)
} in dble'
\end{lstlisting}
In effect, this means that the \q{dble} has \emph{two} types assigned to it: the constrained type above that is inferred through type inference and an overloaded type that results from its translation.
\begin{lstlisting}
for all t such that (arithmetic of t) $=> (t)=>t
\end{lstlisting}
\begin{aside}
Overloaded types are function types, but we use a different types symbol -- \q{\$=>} -- to help distinguish the special role that overloaded types have.
\end{aside}

\begin{aside}
The existence of an overloaded type associated with a variable is an important signal: it means that references to the variable must be resolved -- that appropriate \q{implementation}s of the required contracts are found.
\end{aside}

When an overloaded function variable is referenced the normal type of the variable expression is identical to the normal rule for variable expressions: the type of the expression is the refreshed type of the constrained type associated with the variable.

However, the existence of the overloaded type associated with the variable acts as a signal that the overloading must be resolved.

For example, in the function:
\begin{lstlisting}
fun quad(X) is dble(dble(X))
\end{lstlisting}
the type of each \q{dble} variable expression is determined to be:
\begin{lstlisting}
(%t)=>%t where arithmetic over %t
\end{lstlisting}
\begin{aside}
They are the same type in this case because of the calling pattern for \q{dble}.
\end{aside}

Since \q{dble} originally had a constrained type -- together with its associated overloaded type -- both references must be resolved by supplying an implementation of \q{arithmetic}. I.e., both \q{dble} expressions are interpreted as:
\begin{lstlisting}
dble[A](dble[A](X))
\end{lstlisting}
where we use \q{dble[A]} as a special form function call\footnote{We use this notation for exposition purposes only -- it is not normal `\Sr syntax'.} that denotes a use of the overloaded function.

The \q{quad} function is generic, and so its type is also a generalized constrained type:
\begin{lstlisting}
for all t such that (t)=>t where arithmetic over t
\end{lstlisting}
and is also transformed into the overloaded definition:
\begin{lstlisting}
fun quad(A) is let{
  fun quad'(X) is dble[A](dble[A](X))
} in quad'
\end{lstlisting}
In effect, the resolved dictionary for \q{arithmetic} is `pulled out' to a larger scope. 

In all cases, for overloaded functions to be invoked correctly, there must be some outermost point where an overloaded function is invoked with a concrete implementation value. 

If an overloaded variable is not properly resolved, then the compiler will issue a syntax error.

In most cases, the outermost scope of a program is package-level. It is possible for a package to export an overloaded function -- in which case imports of the package must resolve the overloaded function.


\section{Procedures}
\label{procedures}

An action procedure is an action script -- a program for performing actions. Analogously to functions and other rule types, procedures are written as a set of action rules.

\begin{figure}[htbp]
\begin{eqnarray*}
\ntDef{Procedure}&\arrow&\q{prc}\ \ntRef{ActionRule}\sequence{|}\ntRef{ActionRule}\\
\ntDef{ActionRule}&\arrow&\ntRef{Identifier}\q{(}\,\ntRef{Pattern}\sequence{,}\ntRef{Pattern}\,\q{)}\ [\ntRef{RuleGuard}\,]\ \q{do}\ \ntRef{Action}\\
\ntDef{RuleGuard}&\arrow&\q{default}\\
&\choice&\q{where}\ \ntRef{Condition}
\end{eqnarray*}
\caption{Procedures and Action Rules}\label{procedureSyntaxFig}
\end{figure}

Action rules are analogous to the use of equations for defining functions; except that an action is being specified.

The equivalent of `Hello World' as a procedure would be:
\begin{lstlisting}
prc hello() do logMsg(info,"Hello World");
\end{lstlisting}

The left hand side of an action rule may contain patterns other than variables, it may also include \emph{guard} conditions:
\begin{lstlisting}
prc displaySigned(X) where X>0 do logMsg(info,"\$X is positive")
 |  displaySigned(X) default do logMsg(info,"\$X is not positive")
\end{lstlisting}

\subsubsection{Type Safety}

A procedure is type safe if the action(s) in the body are type safe -- in the environment augmented by the variables in the head of the procedure.

\begin{prooftree}
\AxiomC{\typeprd{E}{P}{\q{(}T\sub1,\ldots,T\subn\q{)=>()}}}
\AxiomC{\typesafe{E\minsert{\cup}H\sub1:T\sub1\minsert{\cup}\ldots\minsert{\cup}H\subn:T\subn}{A}}
\BinaryInfC{\typesafe{E}{\q{prc }P\q{(}H\sub1,\ldots,H\subn\q{) \q{do} A}}}
\end{prooftree}


\subsection{Anonymous Procedure}
\label{anonymousAction}
\index{anonymous action procedure}
\index{expressions!procedure}

A procedure is a `first class value' and can be assigned to variables, passed in functions and so on. In addition, a procedure may be expressed as a \emph{literal expression} in the form of an \emph{anonymous procedure} expression. An anonymous action procedure consists of an action procedure -- using \q{procedure} as the `name' of the procedure.

\begin{figure}[htbp]
\begin{eqnarray*}
\ntDef{AnonProcedure}&\arrow&\q{(}\ntRef{TuplePattern}\ \q{do}\ \ntRef{Action}\q{)}
\end{eqnarray*}
\caption{Anonymous Action Procedure}
\label{anonymousProcedureFig}
\end{figure}

For example, to use the `tree walk' as defined in Program~\vref{treeWalkProg} to display all the leaf nodes, we pass in to \q{walk} an anonymous procedure to display the leaf:
\begin{lstlisting}
walk(Tr,((X) do logMsg(info,"$X")))
\end{lstlisting}

\begin{aside}
Unlike anonymous functions, it nearly always is necessary to enclose an anonymous procedure in parentheses. This is due to the operator precedence of the \q{do} operator.
\end{aside}

Anonymous procedures may access free variables; but may not be directly recursive (see Section~\vref{anonymousFunction}).


\section{Pattern Abstractions}
\label{tauPattern}
A \q{pattern} abstraction allows patterns to be treated as first class values; in an analogous way that lambda abstractions allow expressions to be processed.
\index{pattern abstractions}

\begin{figure}[htbp]
\begin{eqnarray*}
\emph{Expression}&\arrowplus&\ntRef{AnonymousPattern}\\
\ntDef{AnonymousPattern}&\arrow&\q{(}\ntRef{TupleLiteral}\q{ from } \ntRef{Pattern}\q{)}\\
\ntDef{PatternAbstraction}&\arrow&\q{ptn}\ \ntRef{PatternRule}\sequence{|}\ntRef{PatternRule}\\
\ntDef{PatternRule}&\arrow&\ntRef{Identifier}\q{(}\ntRef{Expression}\sequence{,}\ntRef{Expression}\q{) from } \ntRef{Pattern}
\end{eqnarray*}
\caption{Pattern Abstraction Definitions}
\label{tauPtnFig}
\end{figure}

A pattern of the form
\begin{lstlisting}[mathescape=true]
$\emph{Ab}$($\emph{Ptn\sub1}\sequence{,}\emph{Ptn}$)
\end{lstlisting}
represents an application of the pattern abstraction \q{\emph{Ab}}; i.e., the pattern matches if the abstracted pattern within the definition \q{\emph{Ab}} matches \emph{and} that \q{\emph{Ptn\subi}} match the `returned' values from the pattern.

For example, the definition:
\begin{lstlisting}
ptn TM(X) from ("fred",X)
\end{lstlisting}
defines \q{TM} as a pattern that will match binary tuples -- of which the first element is the string \q{"fred"} and returns the second element of the tuple.

We can use \q{TM} to match such tuples, as in:
\begin{lstlisting}[mathescape=true]
for TM(Y) in R do
  $\ldots$
\end{lstlisting}
assuming that the type of \q{R} was appropriately a \q{list} of 2-tuples.

The application argument of a pattern abstraction is also a pattern; so we can look for special forms of \q{TM} patterns in \q{R}:
\begin{lstlisting}[mathescape=true]
if TM(3) in R then
  $\ldots$
\end{lstlisting}
The pattern application \q{TM(3)} is equivalent to the pattern 
\begin{lstlisting}
("fred",3)
\end{lstlisting}
Program~\vref{filterProg} is a more elaborate example that uses a pattern abstraction to filter elements of a \q{list}, removing elements that are less than zero.
\index{filtering elements of a \q{list} with pattern abstractions}
\index{list!filtering with pattern abstractions}
\index{pattern abstractions!using to filtering lists}
\begin{program}
\begin{lstlisting}
positive has type (integer) <= integer
ptn positive(I) from I where I>=0
  
filter has type for all s,t such that
    (list of t, (s)<=t) => list of s
fun filter(L,P) is let{
  fun flt(list of []) is list of []
   |  flt(list of [P(I),..More]) is list of [I,..flt(More)]
   |  flt(list of [_,..More]) default is flt(More)
} in flt(L)
\end{lstlisting}
\caption{Filtering \q{list}s with Pattern Abstractions\label{filterProg}}
\end{program}
The result of evaluating the expression
\begin{lstlisting}
filter(list of [1,3,-2,0,10,-20],positive)
\end{lstlisting}
is
\begin{lstlisting}
list of [1,3,0,10]
\end{lstlisting}

\subsubsection{Type Safety}
The type of a pattern abstraction is determined by the type of pattern matched by the abstraction:
\begin{prooftree}
\AxiomC{\typeprd{E}{P}{T}}
\AxiomC{\typeprd{E}{X\sub1}{t\sub1}\sequence{\quad}\typeprd{E}{X\subn}{t\subn}}
\BinaryInfC{\typeprd{E}{\q{(}{X\sub1}\sequence{,}{X\subn}\q{) from }P}{\q{(}t\sub1}\sequence{,}{t\subn}\q{)<=}T}
\end{prooftree}