Namespaces
Variants
Actions

Difference between revisions of "Refal"

From Encyclopedia of Mathematics
Jump to: navigation, search
(Importing text file)
 
m (tex encoded by computer)
 
Line 1: Line 1:
 +
<!--
 +
r0804801.png
 +
$#A+1 = 13 n = 0
 +
$#C+1 = 13 : ~/encyclopedia/old_files/data/R080/R.0800480 Refal,
 +
Automatically converted into TeX, above some diagnostics.
 +
Please remove this comment and the {{TEX|auto}} line below,
 +
if TeX found to be correct.
 +
-->
 +
 +
{{TEX|auto}}
 +
{{TEX|done}}
 +
 
''algorithmic language of recursive functions''
 
''algorithmic language of recursive functions''
  
 
An [[Algorithmic language|algorithmic language]] oriented towards problems of conversion of symbolic information. In its original version it was called a  "meta-algorithmic language"  (see [[#References|[1]]]). 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.
 
An [[Algorithmic language|algorithmic language]] oriented towards problems of conversion of symbolic information. In its original version it was called a  "meta-algorithmic language"  (see [[#References|[1]]]). 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080480/r0804801.png" /> on an argument <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080480/r0804802.png" /> is expressed in Refal in the form <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080480/r0804803.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080480/r0804804.png" /> is the sign for concretization, which serves as a specific instruction on the need to calculate the value of the function, and the symbol <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080480/r0804805.png" /> denotes the closing bracket for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080480/r0804806.png" />. 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:
+
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) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080480/r0804807.png" />,
+
1) $  \mathbf K + ( \mathbf E A) ( 0) \supseteq \mathbf E A $,
  
2) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080480/r0804808.png" />.
+
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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080480/r0804809.png" />, and it can include free variables (such as <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080480/r08048010.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080480/r08048011.png" />). It is considered to be applicable in the concretization of an expression of the form <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080480/r08048012.png" />, 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/r/r080/r080480/r08048013.png" /> enter the object.
+
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 [[#References|[3]]], [[#References|[4]]]; see [[#References|[5]]] for an example of the use of Refal for machine calculations in theoretical physics).
 
Efficient translators have been developed for the realization of programs in Refal (see [[#References|[3]]], [[#References|[4]]]; see [[#References|[5]]] for an example of the use of Refal for machine calculations in theoretical physics).

Latest revision as of 08:10, 6 June 2020


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 [1]). 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 [3], [4]; see [5] for an example of the use of Refal for machine calculations in theoretical physics).

References

[1] V.F. Turchin, "A meta-algorithmic language" Kibernetika : 4 (1968) pp. 45–54 (In Russian) (English abstract)
[2] V.F. Turchin, V.I. Serdobol'skii, "The language REFAL and its use for transformation of algebraic expressions" Kibernetika : 3 (1969) pp. 58–62 (In Russian) (English abstract)
[3] S.N. Florentzev, V.Yu. Olyunin, V.F. Turchin, , Proc. 1-st all-union Conf. on programming , Kiev (1968) pp. 114–133 (In Russian)
[4] S.A. Romanenko, V.F. Turchin, , Proc. 2-nd all-union Conf. on programming , Novosibirsk (1970) pp. 31–42 (In Russian)
[5] A.P., et al. Budnit, Yadernaya Fizika , 14 (1971) pp. 304–313
How to Cite This Entry:
Refal. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Refal&oldid=16538
This article was adapted from an original article by V.F. Turchin (originator), which appeared in Encyclopedia of Mathematics - ISBN 1402006098. See original article