# Refal

algorithmic language of recursive functions

An algorithmic language oriented towards problems of conversion of symbolic information. In its original version it was called a "meta-algorithmic language" (see ). Refal was created as a universal meta-language for describing the conversion of linguistic objects. It is used when translating from one algorithmic language into another, in the machine realization of analytic calculations, in proving theorems, in translating between natural languages, etc.

Writing an algorithm in Refal consists of describing a specific number of recursive functions on a set of expressions, (i.e. sequences of symbols and brackets) correctly constructed (in the usual sense) relative to the brackets. The value of a function $\phi$ on an argument ${\mathcal E}$ is expressed in Refal in the form $\mathbf K \phi {\mathcal E} \dot{-}$, where $\mathbf K$ is the sign for concretization, which serves as a specific instruction on the need to calculate the value of the function, and the symbol $\dot{-}$ denotes the closing bracket for $\mathbf K$. The description of a function is split up into several propositions (rules of concretization) relating to particular forms of the argument. For example, the function of addition in recursive arithmetic is described in Refal by two propositions:

1) $\mathbf K + ( \mathbf E A) ( 0) \supseteq \mathbf E A$,

2) $\mathbf K + ( \mathbf E A) ( \mathbf E B1) \supseteq \mathbf K + ( \mathbf E A) + ( \mathbf E B) \dot{-} 1$.

A proposition consists of a left- and a right-hand part, separated by the sign $\supseteq$, and it can include free variables (such as $\mathbf E A$ and $\mathbf E B$). It is considered to be applicable in the concretization of an expression of the form $\mathbf K \phi {\mathcal E} \dot{-}$, if the latter can be identified with the left-hand part of a proposition for certain values of the free variables contained in it. The application of a proposition consists of substituting the formula being concretized for the right-hand part of the proposition in which the free variables are replaced by their values. In order to calculate the value of a function, propositions are examined in succession and the first one that appears suitable is used. This process is repeated as long as the signs $\mathbf K$ enter the object.

Efficient translators have been developed for the realization of programs in Refal (see , ; see  for an example of the use of Refal for machine calculations in theoretical physics).

How to Cite This Entry:
Refal. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Refal&oldid=48467
This article was adapted from an original article by V.F. Turchin (originator), which appeared in Encyclopedia of Mathematics - ISBN 1402006098. See original article