What is ALPHA?
The ALPHA
language was developed by Mauras [1]
at IRISA in Rennes, France.
It was a product of research in regular parallel array processors and
systolic arrays.
The ALPHA language is able to formally represent algorithms which have
a high degree of regularity and parallelism such as systolic algorithms.
It is based on the formalism of
recurrence equations which has been often used in various forms by several
authors [2] all of which
were based on the introduction of the notion of uniform recurrence
equations by Karp, Miller and Winograd [3].
ALPHA : An applicative equational language
An equational language is a natural way to describe a system of recurrence
equations. When thinking
about algorithms such as those used in signal processing or numerical
analysis applications,
a person
naturally thinks in terms of mathematical equations.
Mathematical notation has evolved over the centuries and obeys certain
basic rules.
- Given a function and an input, the same
output must be produced each time the function is evaluated.
If the function is time varying, then time must be a parameter to the function.
Turner [4] uses the term static to describe this property.
- Consistency in the use of names: a variable stands for the same value
throughout its scope. This is called referential transparency.
An immediate consequence of referential transparency
is that equality is substitutive --- equal expressions are always
and everywhere interchangeable.
This property is what gives mathematical notation its deductive power [4].
ALPHA shares both of these properties with mathematical notation:
it is static and it is referentially transparent.
Using a language that shares the properties of
mathematical notation eases the task of representing a mathematical algorithm
as a program. Furthermore, such a method of describing algorithms has
some interesting properties, as has been discovered by users of ALPHA.
An equation specifies an assertion on a variable which must always be
true. Reasoning about programs can thus be done in the context of
the program itself, and relies essentially on the fact that ALPHA programs
respect the substitution principle. This principle
states that an equation X = Expression specifies a total
synonymy between the variable on the left hand side of the equation
and the expression on the right hand side of the equation. Thus
any instance of a variable on the left hand side of any equation
may be replaced with the right hand side of its definition. Likewise, any
sub-expression may be replaced with a variable identifier, provided
that an equation exists, or one is introduced, in which that variable
is defined to be equal to that sub-expression.
ALPHA has other properties which should be mentioned.
-
ALPHA equations are unordered.
The only ordering of computations is that which is implied by data
dependencies.
-
ALPHA is a single assignment language. Each variable element
can only ever hold a single value which is ultimately
a function of system inputs.
-
Every ALPHA program is a static program,
meaning that its run time behavior can be analyzed at compile time.
-
ALPHA does not support any notion of global variables. An execution
of a system defined in ALPHA only affects the outputs of the system ---
there are never any side effects.
%Thus, a system without outputs is without purpose, and is dead code.
-
ALPHA is strongly typed. Each variable must be predeclared with
both a domain and data type attributed to that variable.
ALPHA adopts the classical principles of a functional language which
is structured and strongly typed. An ALPHA program defines a function
from its input variables to its output variables. This notion of a function
is embedded in the definition of the ALPHA system
construct.
system ForwardSubstitution : {N | N>0 }
(A : {i,j | 1<=i<=N; 1<=j<=i} of integer;
B : {i | 1<=i<=N } of integer)
returns (X : {i | 1<=i<=N } of integer);
var
b : {i,j | 1<=i<=N; 0<=j<i } of integer;
let
b[i,j] = case
{| j=0 } : 0;
{| j>0 } : A[i,j] * X[j] + b[i,j-1];
esac;
X[i] = ( B[i] - b[i,i-1] )/A[i,i];
tel;