Next: Supercompilation and Verification: an
Up: Verification via Supercompilation
Previous: Supercompilation
The Refal
programming language ((Recursive Functions Algorithmic Language) is a
first-order functional language with an applicative (inside-out) semantics.
Unlike LISP the language is
based on the model of computation known as Markov's algorithms.
Roughly speaking, a program in Refal
is a
term rewriting system. The semantics of Refal
is based on
pattern matching. As usually, the rewriting rules are
ordered to match from the top to the bottom.
The terms are
generated using two constructors:
- The first is the concatenation. It is binary, associative and is used in infix notation,
which allows us to drop its parenthesis. In Refal
the blank is
used to denote the concatenation.
The associativity turning Refal
data set into a monoid.
The monoid structure is reflected in the syntax of programs and
the operational semantics of Refal.
- The second constructor
is unary and is used for constructing tree structures.
It is syntactically denoted with just its parenthesis
(that is without a name).
Angular brackets are used to denote a function call.
Its name is put after the left bracket.
Every function is unary.
In Refal
the ground terms are referred to as constant expressions. Empty sequence is a spe-
cial basic ground term. This term is denoted with nothing
and called empty expression. It is neutral element (both
left and right) of the concatenation. All other basic ground
terms are named as symbols.
There exist three types of
basic non-ground terms (called variables) - e.name, s.name
and t.name:
- an e-variable can take any expression as its
value;
- an s-variable can take any symbol as its value; and
- a t-variable can take any symbol and any expression enclosed in the
parenthesis.
Thus, Refal
data d
and patterns pat
are defined with the
following grammar:
d ::= (d1) | d1 d2 | SYMBOL | empty
pat ::= tpat | pat1 pat2 | empty
tpat ::= (pat) | s.name | t.name | e.name | SYMBOL
Here empty
is the empty string (nihil).
Example: The following program replaces every occurrence
of the identifier Lisp with the identifier Refal
in an arbitrary
Refal
datum.
ENTRY Go { e.inp = <Repl (Lisp Refal) e.inp>; }
Repl {
(s.x e.v) = ;
(s.x e.v) s.x e.inp = e.v <Repl (s.x e.v) e.inp>;
(s.x e.v) s.y e.inp = s.y <Repl (s.x e.v) e.inp>;
(s.x e.v) (e.y) e.inp = (<Repl (s.x e.v) e.y>) <Repl (s.x e.v) e.inp>;
}
On the right side of the first sentence of Repl we see the
empty expression. The left sides of the last three
sentences and the right side of the second sentence of Repl
show associativity of the concatenation.
A detailed description of the language is
available in an electronic format:
Refal-5.
Next: Supercompilation and Verification: an
Up: Verification via Supercompilation
Previous: Supercompilation
Alexei Lisitsa
2005-07-14