next up previous
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: 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: 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 up previous
Next: Supercompilation and Verification: an Up: Verification via Supercompilation Previous: Supercompilation
Alexei Lisitsa 2005-07-14