Next: Supercompilation and Verification: an Up: Verification via Supercompilation Previous: Supercompilation

# Refal

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