funprog-ru
[Top] [All Lists]

[Funprog-ru] [funprog-ru commit] r167 - trunk/ru

From: codesite-noreply@xxxxxxxxxx
Subject: [Funprog-ru] [funprog-ru commit] r167 - trunk/ru
Date: Wed, 05 Sep 2007 07:00:34 -0700
Sender: funprog-ru-bounces@xxxxxxxxxxx
Author: pr.dimiii
Date: Wed Sep  5 07:00:11 2007
New Revision: 167

Modified:
   trunk/ru/examples.tex

Log:
Cleaned up "Symbolic differentiation",
started translation of "Prolog ..."

Modified: trunk/ru/examples.tex
==============================================================================
--- trunk/ru/examples.tex       (original)
+++ trunk/ru/examples.tex       Wed Sep  5 07:00:11 2007
@@ -4,11 +4,12 @@
 �������������� ������. ������ �� �������� � ��� ������ ������ ����������, �� 
�������
 ����� �� �������  <<���������� ����������>>. � ���� ����� �� ����� ��������� 
����������� 
 �������� ������������� ML. �� �������� �� ��������� �������������
-������ ���� �������, ���, ��������, � ������ �������  ����������� ������������
-�����, �������� �����. ������, ����� �������� ��� ��������� � ������� 
�������, � �����, 
-����������. ��������� ��� ������� �������,  ������������� ���  ML ������������ 
+������ ���� �������, ���, ��������, � ������ ����������� ������������
+�����, �������� �����. ������ ����� ����������� ��� ���������, ������� � 
+����������. ��������� ��� ������� ������� �������������, ���  ML ������������ 
 � ����������������.
 
+
 %%As we have said, ML was originally designed as a metalanguage for a computer
 %%theorem prover. However it is suitable for plenty of other applications, 
mostly
 %%from the same general field of `symbolic computation'. In this chapter we 
will
@@ -24,13 +25,13 @@
 %%\section{Symbolic differentiation}
 
 ����� <<���������� ����������>> �������� ��������̣���, �� ����� ������, ��� 
-���������� ���������� ������������, ������������� ��� ��������������� 
-{\em �����������}, � ����� ������ ����������� ����������, � �� ������ 
����������
-���ޣ����. ���� ��������� �������� <<������ ������������ �������>> ����� ���
-Maxima, Maple and Mathematica. ��� ��� ����� ��������� ��������
-�������������� ��������, ����� ��� ���������� ����������� �� ���������, 
-����������������� � �������������� ���������. (��� ����� �������� � ���
-������� ����������.) �� ������� ��� ������ ������ ���� ����� ���� ������ � 
������� ML.
+���������� ���������� ������������ �� ������ ���������� ���ޣ����, � 
������������� 
+��� ��������������� {\em �����������}, � ����� ������ ����������� ����������. 
���� 
+��������� �������� <<������ ������������ �������>> ����� ��� 
+Maxima, Maple and Mathematica. ��� ����� ��������� ��������
+�������������� ��������: ���������� ����������� �� ���������, 
+����������������� � �������������� ��������� � �.�. ��� ����� �������� � ���
+������� ����������. �� �������, ��� ������ ������ ���� ����� ���� ������ � 
������� ML.
 
 %%The phrase `symbolic computation' is a bit vague, but roughly speaking it
 %%covers applications where manipulation of mathematical {\em expressions}, in
@@ -43,7 +44,7 @@
 
 �� ������� ���������� ����������������� ��� ������ �������, ������ ��� ��� ����
 ���� �������� ������� � ��������� ��������. ��������, ��������, ������
-� ������̣����� ������������ �������� �������, �������� ${d \over dx} sin(x) =
+�  ������������ �������� �������, �������� ${d \over dx} sin(x) =
 cos(x)$, � ����� � ��������� ����������������� ������������ � ���������� 
 �������. ��������� ������ ����� �������������� ������������  ��� �������
 ��� ���������� �����������, �� �������� � ����������������� �� �� ML. 
@@ -65,7 +66,7 @@
 �� ����� ��������� �������������� ��������� � ������ ����� �����. ��� �����
 ���� ��������� �� ���������� � ��������, � �������������� ����������. ���������
 ����� ���� ��������, ���������, ����������, ���, � ����� ������, �������~$n$.
-�� �������� ��� � ������� ���������� ������������ ���� ������:
+��� ���������� � ������� ���������� ������������ ���� ������:
 
 %%We will allow mathematical expressions in a fairly general form. They may be
 %%built up from variables and constants by the application of operators. These
@@ -97,12 +98,12 @@
 
 ������ � ������ ��������� � ����� ���� �������� ��������. ��� ����� ��������
 ��� ���� ������ ���������� ����������, � ������ ��������� ������� ��������
-{\em �������������� ���������� (������)} � {\em ������� ������}, �����������
-������� � �������� ������ � �������� �����. ��������� ���������� 
��������������� 
-������� �� �������, ��������� ���, ���� �� ���� ������ ����, ����� ����������� 
-�����, � ������ �� ������� ����������� ������� ������ ��� ����� ���������. 
����� 
-�����, �� ������� ����, �� ����� ������ ��� ����������. �� �����, ����� 
-�������������� ������� ����������, ��� ��:
+{\em �������������� ���������� (������)} � {\em ������� �����-������},
+����������� ������� � �������� ������ � �������� �����. ������� ���� ���������
+���������� ��������������� �������, ��������� ���, ���� �� ���� ������ ����, 
����� ����������� 
+�����, � ������ �� ������� ����������� ������� ������ ��� ����� ���������. 
+�����, �� ������� ����, ����� ���� ������ ��� ����������. �� �����, ����� 
+�������������� ������� ����������, ���-��:
 
 %%Reading and writing expressions in their raw form is rather unpleasant. This 
is
 %%a general problem in all symbolic computation systems, and typically the
@@ -143,7 +144,7 @@
 
 \end{itemize}
 
-������� �� ������� ������ ��������� ���������� - ������ ��� �� ����� ���������
+������� �� ������� ������ ��������� ����������~-- ������ ��� �� ����� ���������
 � ��� ����������.
 
 %%First we declare a list of infixes, which is a list of pairs: each operator
@@ -154,10 +155,10 @@
 \end{verbatim}\end{boxed}
 
 ������������� ������� ��� ������������� �������� ��������� ������� �������� 
-����������� ���������. ��� ������ ���������� {\em �������������� ��������}, 
+����������� ���������. ��� ������ ���������� {\em �������������� ��������} 
 � ������ �������������� � �������������� ����������������.\footnote{��� �����
-������������ ����������, ������ �������� ������������, ����� ��� ��� - �������,
-�� ��� ������� ����������, � �������� ������ �� ������� ������, ������� � ���� 
��������� 
+������������ ���������� ������ �������� ������������, ����� ��� ���-�������,
+�� ��� ������� ����������, � ������� ������ �� ������� ������, ������� � ���� 
��������� 
 ������ �������� ������� � ����������.} ��� ���� ����� �������������� ������ �
 ��������� ������� �� ���������� {\tt assoc}:
 
@@ -200,7 +201,7 @@
 �������� ��������, ���� �� ����� - ���� ������� ���� ������ ����������, 
 �� ������ �������, ����� {\tt get\_precedence}, ������������ ���, ����������� 
 ��������������. ��� �������� �������� ��������, �� ������� ������  LISP 
������������ 
-������������ ������������ ����������. �� ����� ������� ��������� ��������� 
���������� 
+������������ ������������ ����������. ��������� ��������� ���������� ����� 
�������  
 ����������� �����������, ��������� ��������� �� ������:
 
 %%Note that if we ever change this list of infixes, then any functions such as
@@ -224,9 +225,9 @@
   - : int = 30
 \end{verbatim}\end{boxed}
 
-��������, �� �������� ���������� � ML, ������������� ��������� ����������� 
������
-����� ����, ��� {\tt get\_precedence} �������� ���� ���������, �, 
�������������, 
-���������� � ��������� ����������. �� ����� ����� ���������� �������, 
������������,
+�������, ��� �� �������� ���������� � ML, ������������� ��������� �����������
+������ ����� ����, ��� {\tt get\_precedence} �������� ���� ���������, �, 
�������������, 
+���������� �� ��������� ����������. �� ����� ����� ������ �������, 
������������,
 �������� �� ��������� ������� ��������� ����������. ����� ������ ������������ 
 {\tt get\_precedence} � �������� ��������� �� ���:
 
@@ -242,8 +243,8 @@
      with _ -> false;;
 \end{verbatim}\end{boxed}
 
-������������ ����������� � ������������� ����� ������� {\tt can}, ������� 
��������� ������� ��
-������ �������:
+������������ ����������� � ������������� ����� ������� {\tt can}, ������� 
��������� 
+���������� ���������� ������ �������:
 
 %%An alternative is to use a general function {\tt can} that finds out whether
 %%another function succeeds:
@@ -294,14 +295,15 @@
 ������ �������� {\tt prec} ���������� ������� ���������� ���������, ��� 
��������
 ������� ��������������� ��������� �������� ���������������� ���������. 
 ��� ��� ���� ������� ��������� ����� ��������� �������� � ��������� 
�����������, �� 
-������ ���������� ���� ��������� ����� ��������� ���� {\tt prec}, ����� 
�������, ���� ��
-������������� ������ �����  $x * (y + z)$. �������������, �� ���������� 
-������ ���� ����� ��� �����, ��� ����� ��������� �����������. 
+������ ����������, ���� ��������� ����� ��������� ���� {\tt prec}. ��������,
+���� �� ������������� ������ �����  $x * (y + z)$. �� ����� ����, ��� ����� 
+��������� �����������  �� ���������� ������ ���� ����� {\tt prec} � ��������� 
+�������� ��������� �����. 
 � ������ ������������� ����������, ����� $+$ ��� �� �����, �� �� ������ 
��������� 
-$x - (y - z)$ � $(x - y) - z$. (����� ��������� ����� ����� �� ��������� � 
������
-���������� ���������������.) ������, ������� �����������, �������
+$x - (y - z)$ � $(x - y) - z$. (����� ��������� ����� ����� �� ��������� 
+��������������� ������� ���������.) ������, ������� �����������, �������
 {\tt string\_of\_terms} ������������ ��� ������ ������ ������ ����� �������, 
��� 
-��� ���� � ����������� ����� $f(t_1,\ldots,t_n)$.
+��� ���� � ����������� ����� $f(t_1,\ldots,t_n)$.
 ������� ��������� ��� � ��������:
 
 %%The first argument {\tt prec} indicates the precedence level of the operator 
of
@@ -336,7 +338,7 @@
 \end{verbatim}\end{boxed}
 
 ��  ����� ����, ��� ���� �� ��������� �������������� �������������� ���� � 
������. CAML Light
-��������� ��� ��������� ���� ������� ������. ��� ��������� ��������� 
����������� ������:
+��������� ��� ��������� ���� ������� ������. ��� ������� ��������� ����������� 
������:
 
 %%In fact, we don't need to convert a term to a string ourselves. CAML Light
 %%allows us to set up our own printer so that it is used to print anything of
@@ -372,7 +374,7 @@
 
 ����� ���� ��� ����� ������� ����������, �� ����� �������������� ������ ���
 ��� ������ ���� {\tt term}, ���� ���� �� ������������ ����� ��������� 
-��� ������, ��� �������� ������:
+��� ������, ���, ��������, ������:
 
 %%Once the new printer is installed, it is used whenever CAML wants to print
 %%something of type {\tt term}, even if it is a composite datastructure
@@ -428,7 +430,7 @@
 \begin{itemize}
 
   \item ���� ��������� - ���� �� ������������ ������� ����������������� 
���������, 
-  �������� \alert{$sin(x)$}, �� ��������� ����������������� - ��������� 
����������� ���� �������.
+  �������� \alert{$sin(x)$}, �� ��������� �����������������~-- ��������� 
����������� ���� �������.
 
   %\item If the expression is one of the standard functions applied to an
   %argument, e.g. \alert{$sin(x)$}, return the known derivative.
@@ -534,13 +536,13 @@
     -(inv(cos(x - exp(y)) ^ 2)))) - (0 + 0) * inv(1 + x)`
 \end{verbatim}\end{boxed}
 
-������, ��� �� ��������� ��������� ��������� ���������, ����� ��� $0 * x = 0$
+������ ��� �� ��������� ��������� ��������� ���������, ����� ��� $0 * x = 0$
 � $x + 0 = x$. ��������� �� ���� ���������� ��������� ��������� ����� 
������������� 
 ���������� �����������������, �������, ��������, ��������� �������
-����������������� �����������������~$f(t)$ ���� ����� $t$~-~����� ���� 
����������
-�����������������. ������ ����������� ���������� ������� �����������������
-������� ������� ��������� ������� ���������, ������� ����� ������������ 
-�� �������������� ���������.
+����������������� �����������������~$f(t)$ ���� ����� $t$~-- ����� 
+���� ���������� �����������������. ������ ����������� ���������� ������� 
+����������������� ������� ������� ��������� ������� ���������, ������� ����� 
+����������� �� �������������� ���������.
 
 %%However, it fails to make various obvious simplifications such as $0 * x = 0$
 %%and $x + 0 = x$. Some of these redundant expressions are created by the 
rather
@@ -568,14 +570,14 @@
        | t -> t;;
 \end{verbatim}\end{boxed}
 
-�� ������ ��������� ��������� � ������ ������� ������. �� ������ ��������� ���
-� ������ ��������� ����� - �����. 
+�� ������ ��������� ���������, ������� � ����� ������ ���������. �� ��������� 
+��� � ������ ����� - �����. 
 % This will also bring negations upwards through products. 
 % - ��� - �� ��� ���� "-"  
-� ��������� ������� ���� �� ����� ���������� ��������� ��� ������ ����� - 
����, 
-��������, $0 * t$ ��� ���������� ��������� $t$, �� ��� ��������� ����������
-��� ������ ����� $(0 + 0) * 2$. ����� ����� ���������� ����� �����
-���������� � ������������� �������� �������� � ������ ����������.
+� ��������� ������� ���� �� ����� ���������� ��������� ��� ������ ������ - 
����, 
+��������, ��� $0 * t$ � �������� ��������� $t$, �� ��� ��������� ����������
+� ������ ������ ����� $(0 + 0) * 2$. ����� ����� ���������� ����� �����
+���������� � ������������� �������� �������� � ������-����������.
 
 
 %%This just applies the simplification at the top level of the term. We need to
@@ -609,7 +611,7 @@
   - : term = `0`
 \end{verbatim}\end{boxed}
 
-� �����, ������ ����� �������� ����� ��������� ������� ���������. 
+� �����, ������ ����� �������� ����� ��������� ������� ���������. 
 ��������, ����������:
 
 
@@ -671,8 +673,8 @@
 
 ����� ������ � ������, � ����� ��������. ��� �� �����, ����� ������� 
������������
 �� ���, ��� �� ����� �����������  �������� ����������� ������������������ 
�������,
-����� {\tt sec}. ����� ������ �� ������ ������, ��������, ����� ������������,
-�������� ��� �� �������.
+����� {\tt sec}. ��� �� ������ �� ������ ������, ��������, �����
+������������, �������� ��� �� �������.
 
 %%Certainly, it is shorter and more conventional. However it relies on the fact
 %%that we know the definitions of these fairly obscure trig functions like {\tt
@@ -2508,49 +2510,84 @@
 %directly rather than by iterating the addition function; this leads to much
 %better error behaviour.
 
-\section{Prolog and theorem proving}
+\section{������ � �������������� ������}
 
-The language Prolog is popular in Artificial Intelligence research, and is used
-in various practical applications such as expert systems and intelligent
-databases. Here we will show how the main mechanism of Prolog, namely
-depth-first search through a database of rules using unification and
-backtracking, can be implemented in ML. We do not pretend that this is a
-full-blown implementation of Prolog, but it gives an accurate picture of the
-general flavour of the language, and we will be able to run some simple
-examples in our system.
-
-\subsection{Prolog terms}
-
-Prolog code and data is represented using a uniform system of first order
-terms. We have already defined a type of terms for our mathematical
-expressions, and associated parsers and printers. Here we will use something
-similar, but not quite the same. First of all, it simplifies some of the code
-if we treat constants as nullary functions, i.e. functions that take an empty
-list of arguments. Accordingly we define:
+���� ������ ��������� � ������� ������������ �� �������������� ����������,
+� ������������ � ��������� ������������ �����������, ����� ��� ���������� 
+������� � ���������������� ���� ������. � ���� ����� ��������������� ���
+��������� ��������� �������, � ������: ����� ������ � ����������� � ���������,
+����� ���� ����������� � ML. �� �� ���������� �� ������ ���������� �������,
+�� ��� ���� ���  ������ ������������� �� �������� ������������ ����� �
+�� ������ ��������� ��������� ��������.
+% The language Prolog is popular in Artificial Intelligence research, and is 
used
+% in various practical applications such as expert systems and intelligent
+% databases. Here we will show how the main mechanism of Prolog, namely
+% depth-first search through a database of rules using unification and
+% backtracking, can be implemented in ML. We do not pretend that this is a
+% full-blown implementation of Prolog, but it gives an accurate picture of the
+% general flavour of the language, and we will be able to run some simple
+% examples in our system.
+
+\subsection{����� �������}
+
+������ � ��� � ������� �������������� � ������� ������ ������� ������ �������
+�������. �� ��� ���������� ��� ������ ��� ����� �������������� ���������, �� 
+������, � ��������������� ��������. ������ �� ����� ������������ �����
+�������, �� � ���������� �������������. ��-������, ������� �������� ���, ����� 
+������������� ��������� ��� ����-����� �������, �.�. ��� �������, ����������� 
+������ ������ ����������. �������������� ���������:
+%%Prolog code and data is represented using a uniform system of first order
+%%terms. We have already defined a type of terms for our mathematical
+%%expressions, and associated parsers and printers. Here we will use something
+%%similar, but not quite the same. First of all, it simplifies some of the code
+%%if we treat constants as nullary functions, i.e. functions that take an empty
+%%list of arguments. Accordingly we define:
 
 \begin{boxed}\begin{lstlisting}
   type term = Var of string
             | Fn of string * (term list);;
 \end{lstlisting}\end{boxed}
 
-Where we would formerly have used {\verb+Const s+}, we will now use
-{\verb+Fn(s,[])+}. Note that we will treat functions of different arities
-(different numbers of arguments) as distinct, even if they have the same name.
-Thus there is no danger of our confusing constants with true functions.
-
-\subsection{Lexical analysis}
-
-In order to follow Prolog conventions, which include case sensitivity, we also
-modify lexical analysis. We will not attempt to conform exactly to the full
-details of Prolog, but one feature is very important: alphanumeric identifiers
-that begin with an {\em upper case} letter or an underscore are treated as
-variables, while other alphanumeric identifiers, along with numerals, are
-treated as constants. For example {\verb+X+} and {\verb+Answer+} are variables
-while {\verb+x+} and {\verb+john+} are constants. We will lump all symbolic
+���, ��� ������ �������������  {\verb+Const s+}, ������ �����
+{\verb+Fn(s,[])+}. �������� ��������, ��� �� ����� ������������� ������� 
��������� �������
+(������ ������ ����������) ��� ���������, ���� ���� � ��� ���������� ���.
+������������� ��� ���������, ��� ��������� ����� ������� � ����������
+���������.
+%%Where we would formerly have used {\verb+Const s+}, we will now use
+%%{\verb+Fn(s,[])+}. Note that we will treat functions of different arities
+%%(different numbers of arguments) as distinct, even if they have the same 
name.
+%%Thus there is no danger of our confusing constants with true functions.
+
+\subsection{����������� ������}
+
+� ����� ���������� ����������� �������, ������� �������� ���������������� �
+��������, �� ������� ������� ������������ �������. �� �� ����� ���������
+������� ���������� �� �ӣ�, �� ���� ������ ����� �����: 
+���������-�������� ��������������, ������������ � ����� {\em � ������� 
��������},
+��������������� ��� ����������, � ������ ���������-�������� �������������� �
+�����~-- ��� ���������. ��������, {\verb+X+} � {\verb+Answer+}~-- ����������,
+����� ��� {\verb+x+} � {\verb+john+}~-- ���������. �� ����� ��������� ��� 
+���������� �������������� ������ � �����������, �� ����� ���������
+������� ����������: ����� � ������ ������, ������� � ����� � �������. 
+���������� �������������� ������ �������� ����� ��� �� ������ �������
+���������������� ������� ���������� ������, ��� ���  
+We
+will lump all symbolic
 identifiers together as constants too, but we will distinguish the punctuation
 symbols: left and right brackets, commas and semicolons. Non-punctuation
 symbols are collected together into the longest strings possible, so symbolic
 identifiers need not consist only of one character.
+% In order to follow Prolog conventions, which include case sensitivity, we 
also
+% modify lexical analysis. We will not attempt to conform exactly to the full
+% details of Prolog, but one feature is very important: alphanumeric 
identifiers
+% that begin with an {\em upper case} letter or an underscore are treated as
+% variables, while other alphanumeric identifiers, along with numerals, are
+% treated as constants. For example {\verb+X+} and {\verb+Answer+} are 
variables
+% while {\verb+x+} and {\verb+john+} are constants. We will lump all symbolic
+% identifiers together as constants too, but we will distinguish the 
punctuation
+% symbols: left and right brackets, commas and semicolons. Non-punctuation
+% symbols are collected together into the longest strings possible, so symbolic
+% identifiers need not consist only of one character.
 
 \begin{boxed}\begin{lstlisting}
   type token = Variable of string
@@ -2558,7 +2595,8 @@
              | Punct of string;;
 \end{lstlisting}\end{boxed}
 
-\noindent The lexer therefore looks like this:
+\noindent ����������� ����������, ������������� �������� ���:
+% \noindent The lexer therefore looks like this:
 
 \begin{boxed}\begin{lstlisting}
   let lex =
@@ -2585,7 +2623,7 @@
     fst o alltokens o explode;;
 \end{lstlisting}\end{boxed}
 
-\noindent For example:
+\noindent ��������:
 
 \begin{boxed}\begin{verbatim}
   #lex "add(X,Y,Z) :- X is Y+Z.";;
@@ -2596,15 +2634,21 @@
     Constant "+"; Variable "Z"; Punct "."]
 \end{verbatim}\end{boxed}
 
-\subsection{Parsing}
+\subsection{�������������� ������}
 
-The basic parser is pretty much the same as before; the printer is exactly the
-same. The main modification to the printer is that we allow Prolog lists to be
-written in a more convenient notation. Prolog has `.' and `nil' corresponding
-to ML's `{\tt ::}' and `{\tt []}', and we set up the parser so that lists can
-be written much as in ML, e.g. `{\tt [1,2,3]}'. We also allow the Prolog
-notation `{\verb+[H|T]+}' instead of `{\verb+cons(H,T)+}', typically used for
-pattern-matching. After the basic functions:
+�������� �������������� ���������� �������� � ������������ ������� ����� ��,
+��� ��� �����, ������� ������ �� ��������. ������������ �����������~-- 
������������
+������ ������������ � ����� ������� �������. � ������� <<.>> � <<nil>> 
+�������������  <<{\tt ::}>> � <<{\tt []}>> � ML. �� ����� ��������� 
+������������ ������ <<{\verb+[H|T]+}>> ������ <<{\verb+cons(H,T)+}>>, ������
+������������ ��� ��������� �� �������. ����� �������� �������:
+% The basic parser is pretty much the same as before; the printer is exactly 
the
+% same. The main modification to the printer is that we allow Prolog lists to 
be
+% written in a more convenient notation. Prolog has `.' and `nil' corresponding
+% to ML's `{\tt ::}' and `{\tt []}', and we set up the parser so that lists can
+% be written much as in ML, e.g. `{\tt [1,2,3]}'. We also allow the Prolog
+% notation `{\verb+[H|T]+}' instead of `{\verb+cons(H,T)+}', typically used for
+% pattern-matching. After the basic functions:
 
 \begin{boxed}\begin{lstlisting}
   let variable =
@@ -2616,14 +2660,17 @@
       | _ -> raise Noparse;;
 \end{lstlisting}\end{boxed}
 
-\noindent we have a parser for terms and also for Prolog rules, of these forms:
+\noindent � ��� ���� �������������� ���������� ��� ������, � ����� ������
+������� � ��������� �����: 
+% \noindent we have a parser for terms and also for Prolog rules, of these 
forms:
 
 \begin{eqnarray*}
 term\mbox{.}    & &                                             \\
 term            & \mbox{ :- } & term,\ldots,term\mbox{.}
 \end{eqnarray*}
 
-\noindent The parsers are as follows:
+\noindent ���������� �������:
+% \noindent The parsers are as follows:
 
 \begin{boxed}\begin{lstlisting}
   let rec atom input
@@ -2666,44 +2713,66 @@
   let parse_rules = fst o (many rule ++ finished >> fst) o lex;;
 \end{lstlisting}\end{boxed}
 
-\subsection{Unification}
+\subsection{����������}
 
-Prolog uses a set of rules to solve a current {\em goal} by trying to match one
-of the rules against the goal. A rule consisting of a single term can solve a
-goal immediately. In the case of a rule $term \mbox{ :- }
-term_1,\ldots,term_n\mbox{.}$, if the goal matches $term$, then Prolog needs to
-solve each $term_i$ as a subgoal in order to finish the original goal.
-
-However, goals and rules do not have to be exactly the same. Instead, Prolog
-assigns variables in both the goal and the rule to make them match up, a
-process known as {\em unification}. This means that we can end up proving a
-special case of the original goal, e.g. $P(f(X))$ instead of
-$P(Y)$. For example:
+������ ���������� ����� ������ ��� ���������� ������� {\em ����}. ��� ����� ��
+��������� ������� ��� ����. �������, ��������� �� ������ �����, ���������
+���� ����������, ���� ������������� ����. � ������ ������� $term \mbox{ :- } 
+term_1,\ldots,term_n\mbox{.}$, ���� ���� ������������� $term$, �� ������� 
+���������� ���������, ��� �������, �� ������� ������ $term_i$. ���� ��
+����� ��������� ���, �������������� ���� ��������� �����ۣ����.  
+% Prolog uses a set of rules to solve a current {\em goal} by trying to match 
one
+% of the rules against the goal. A rule consisting of a single term can solve a
+% goal immediately. In the case of a rule $term \mbox{ :- }
+% term_1,\ldots,term_n\mbox{.}$, if the goal matches $term$, then Prolog needs 
to
+% solve each $term_i$ as a subgoal in order to finish the original goal.
+
+������, ���� � ������� �� ������� � �������� ���������. ������ ������ ���������
+���������� ��� ���� � ��������������� �������, ����� �������� ���������� 
+{\em �����������}. ��� ��������, ��� �� ����� �������� �������� ����������
+�������� ������������ ����, �.�.  $@(f(X))$ ������ $P(Y)$.
+��������:
+% However, goals and rules do not have to be exactly the same. Instead, Prolog
+% assigns variables in both the goal and the rule to make them match up, a
+% process known as {\em unification}. This means that we can end up proving a
+% special case of the original goal, e.g. $P(f(X))$ instead of
+% $P(Y)$. For example:
 
 \begin{itemize}
 
-\item To unify $f(g(X),Y)$ and $f(g(a),X)$ we can set
-$X = a$ and $Y = a$. Then both terms are $f(g(a),a)$.
+\item ��� ���������� $f(g(X),Y)$ � $f(g(a),X)$ �� ����� ���������
+$X = a$ � $Y = a$. ����� ����� ����� �����: $f(g(a),a)$.
 
-\item To unify $f(a,X,Y)$ and $f(X,a,Z)$ we can set $X
-= a$ and $Y = Z$, and then both terms are $f(a,a,Z)$.
+\item ��� ���������� $f(a,X,Y)$ � $f(X,a,Z)$ �� ����� ��������� 
+$X = a$ � $Y = Z$, ����� ���� ��� ����� ������ ��� $f(a,a,Z)$.
 
-\item It is impossible to unify $f(X)$ and $X$.
+\item ����������� ������������� $f(X)$ � $X$.
+% \item To unify $f(g(X),Y)$ and $f(g(a),X)$ we can set
+% $X = a$ and $Y = a$. Then both terms are $f(g(a),a)$.
+% 
+% \item To unify $f(a,X,Y)$ and $f(X,a,Z)$ we can set $X
+% = a$ and $Y = Z$, and then both terms are $f(a,a,Z)$.
+% 
+% \item It is impossible to unify $f(X)$ and $X$.
 
 \end{itemize}
 
-In general, unifiers are not unique. For example, in the second example we
-could choose to set $Y = f(b)$ and $Z = f(b)$. However one can always choose
-one that is {\em most general}, i.e. any other unification can be reached from
-it by further instantiation (compare most general types in ML). In order to
-find it, roughly speaking, one need only descend the two terms recursively
-in parallel, and on finding a variable on either side, assigns it to whatever
-the term on the other side is. One also needs to check that the variable hasn't
-already been assigned to something else, and that it doesn't occur in the term
-being assigned to it (as in the last example above). A simple implementation of
-this idea follows. We maintain an association list giving instantiations
-already made, and we look each variable up to see if it is already assigned
-before proceeding. We use the existing instantiations as an accumulator.
+� ����� ������, ����������� �� ���������. ��������, �� ������ ������� ��
+����� ������� ������������ $Y = f(b)$ � $Z = f(b)$. ������, ������ �����
+�������  {\em most general}, i.e. any other unification can be reached from
+% it by further instantiation (compare most general types in ML)
+% In general, unifiers are not unique. For example, in the second example we
+% could choose to set $Y = f(b)$ and $Z = f(b)$. However one can always choose
+% one that is {\em most general}, i.e. any other unification can be reached 
from
+% it by further instantiation (compare most general types in ML). In order to
+% find it, roughly speaking, one need only descend the two terms recursively
+% in parallel, and on finding a variable on either side, assigns it to whatever
+% the term on the other side is. One also needs to check that the variable 
hasn't
+% already been assigned to something else, and that it doesn't occur in the 
term
+% being assigned to it (as in the last example above). A simple implementation 
of
+% this idea follows. We maintain an association list giving instantiations
+% already made, and we look each variable up to see if it is already assigned
+% before proceeding. We use the existing instantiations as an accumulator.
 
 \begin{boxed}\begin{lstlisting}
   let rec unify tm1 tm2 insts =
@@ -2760,13 +2829,18 @@
            else raw_augment (v,t') insts;;
 \end{lstlisting}\end{boxed}
 
-\subsection{Backtracking}
+\subsection{������� � ����������}
 
-Prolog proceeds by depth-first search, but it may backtrack: even if a rule
-unifies successfully, if all the remaining goals cannot be solved under the
-resulting instantiations, then another initial rule is tried. Thus we consider
-the whole list of goals rather than one at a time, to give the right control
-strategy.
+������ ��������� ����� � �������, �� �� ����� ������������ �������: ���� ����
+������� ��������� �������������, ���� ��� ����������� ���� �� ����� ���� 
���������
+��� ������� ����������� ����������, �� ��������� ������ �������� 
(��������������)
+�������. �������������, �� ������������� ����� ������ �����, ������ ����� ��
+���. 
+% Prolog proceeds by depth-first search, but it may backtrack: even if a rule
+% unifies successfully, if all the remaining goals cannot be solved under the
+% resulting instantiations, then another initial rule is tried. Thus we 
consider
+% the whole list of goals rather than one at a time, to give the right control
+% strategy.
 
 \begin{boxed}\begin{lstlisting}
   let rec first f =
@@ -2787,8 +2861,9 @@
       expand (n + 1) rules global goals') rules;;
 \end{lstlisting}\end{boxed}
 
-Here we use a function `rename' to generate fresh variables for the rules each
-time:
+�� ���������� ������� {\tt rename} ��� ��������� ����� ����������:
+% Here we use a function `rename' to generate fresh variables for the rules 
each
+% time:
 
 \begin{boxed}\begin{verbatim}
   let rec rename s =
@@ -2799,8 +2874,10 @@
     (rename s conc,map (rename s) asms);;
 \end{verbatim}\end{boxed}
 
-Finally, we can package everything together in a function {\tt prolog} that
-tries to solve a given goal using the given rules:
+�������, �� ����� ������� �ӣ ������, � ���� ������� {\tt prolog}, �������
+�������� ��������� �������� �������, ��������� �������: 
+% Finally, we can package everything together in a function {\tt prolog} that
+% tries to solve a given goal using the given rules:
 
 \begin{boxed}\begin{verbatim}
   type outcome = No | Yes of (string * term) list;;
@@ -2812,14 +2889,16 @@
     with error _ -> No;;
 \end{verbatim}\end{boxed}
 
-This says either that the goal cannot be solved, or that it can be solved with
-the given instantiations. Note that we only return one answer in this latter
-case, but this is easy to change if desired.
-
-\subsection{Examples}
-
-We can use the Prolog interpreter just written to try some simple examples from
-Prolog textbooks. For example:
+% This says either that the goal cannot be solved, or that it can be solved 
with
+% the given instantiations. Note that we only return one answer in this latter
+% case, but this is easy to change if desired.
+
+\subsection{�������}
+
+�� ����� ������������ ������ ��� ���������� ������������� ���
+������� �������� �� �����-������ ����� �� �������. ��������:
+% We can use the Prolog interpreter just written to try some simple examples 
from
+% Prolog textbooks. For example:
 
 \begin{boxed}\begin{verbatim}
   #let rules = parse_rules
@@ -2848,10 +2927,10 @@
   - : outcome = Yes ["Y", `edward`; "X", `alice`]
 \end{verbatim}\end{boxed}
 
-The following are similar to some elementary ML list operations. Since Prolog
-is relational rather than functional, it is possible to use Prolog queries in a
-more flexible way, e.g. ask what arguments would give a certain result, rather
-than vice versa:
+% The following are similar to some elementary ML list operations. Since Prolog
+% is relational rather than functional, it is possible to use Prolog queries 
in a
+% more flexible way, e.g. ask what arguments would give a certain result, 
rather
+% than vice versa:
 
 \begin{boxed}\begin{verbatim}
   #let r = parse_rules
@@ -2870,48 +2949,52 @@
   - : outcome = Yes ["Y", `1 . (2 . X)`]
 \end{verbatim}\end{boxed}
 
-In such cases, Prolog seems to be showing an impressive degree of intelligence.
-However under the surface it is just using a simple search strategy, and this
-can easily be thwarted. For example, the following loops indefinitely:
+� ����� ������� ������ �������������� � ������������ ������� ����������������.
+�� �� ���� ����������� ����� ������� �����, � ������ <<������������������>> 
+������. ��������, ��������� ����� ��������̣���:
+
+% In such cases, Prolog seems to be showing an impressive degree of 
intelligence.
+% However under the surface it is just using a simple search strategy, and this
+% can easily be thwarted. For example, the following loops indefinitely:
 
 \begin{boxed}\begin{verbatim}
   #prolog r (parse_term "append(X,[3,4],X)");;
 \end{verbatim}\end{boxed}
 
-\subsection{Theorem proving}
+\subsection{�������������� ������}
 
-Prolog is acting as a simple theorem prover, using a database of logical facts
-(the rules) in order to prove a goal. However it is rather limited in the facts
-it can prove, partly because its depth-first search strategy is incomplete, and
-partly because it can only make logical deductions in certain patterns. It is
-possible to make Prolog-like systems that are more powerful, e.g. see
-\citeN{stickel-pttp}. In what follows, we will just show how to build a more
-capable theorem prover using essentially similar technology, including the
-unification code and an identical backtracking strategy.
-
-In particular, unification is an effective way of deciding how to specialize
-universally quantified variables. For example, given the facts that
-$\all{X} p(X) \Imp q(X)$ and $p(f(a))$, we can unify the two
-expressions involving $p$ and thus discover that we need to set
-$X$ to $f(a)$. By contrast, the very earliest theorem provers tried all
-possible terms built up from the available constants and functions (the
-`Herbrand base').
-
-Usually, depth-first search would go into an infinite loop, so we need to
-modify the Prolog strategy slightly. We will use {\em depth first iterative
-deepening}. This means that the search depth has a hard limit, and attempts to
-exceed it cause backtracking. However, if no proof is found at a given depth,
-the bound is increased and another attempt is made. Thus, first one searches
-for proofs of depth $1$, and if that fails, searches for one of depth $2$, then
-depth $3$ and so on. For `depth' one can use various parameters, e.g. the
-height or overall size of the search tree; we will use the number of unifiable
-variables introduced.
-
-\subsubsection*{Manipulating formulas}
-
-We will simply use our standard first order terms to denote formulas,
-introducing new constants for the logical operators. Many of these are written
-infix.
+% Prolog is acting as a simple theorem prover, using a database of logical 
facts
+% (the rules) in order to prove a goal. However it is rather limited in the 
facts
+% it can prove, partly because its depth-first search strategy is incomplete, 
and
+% partly because it can only make logical deductions in certain patterns. It is
+% possible to make Prolog-like systems that are more powerful, e.g. see
+% \citeN{stickel-pttp}. In what follows, we will just show how to build a more
+% capable theorem prover using essentially similar technology, including the
+% unification code and an identical backtracking strategy.
+
+% In particular, unification is an effective way of deciding how to specialize
+% universally quantified variables. For example, given the facts that
+% $\all{X} p(X) \Imp q(X)$ and $p(f(a))$, we can unify the two
+% expressions involving $p$ and thus discover that we need to set
+% $X$ to $f(a)$. By contrast, the very earliest theorem provers tried all
+% possible terms built up from the available constants and functions (the
+% `Herbrand base').
+
+% Usually, depth-first search would go into an infinite loop, so we need to
+% modify the Prolog strategy slightly. We will use {\em depth first iterative
+% deepening}. This means that the search depth has a hard limit, and attempts 
to
+% exceed it cause backtracking. However, if no proof is found at a given depth,
+% the bound is increased and another attempt is made. Thus, first one searches
+% for proofs of depth $1$, and if that fails, searches for one of depth $2$, 
then
+% depth $3$ and so on. For `depth' one can use various parameters, e.g. the
+% height or overall size of the search tree; we will use the number of 
unifiable
+% variables introduced.
+
+\subsubsection*{��������������� ���������}
+
+% We will simply use our standard first order terms to denote formulas,
+% introducing new constants for the logical operators. Many of these are 
written
+% infix.
 
 \begin{center}
 \begin{tabular}{|l|l|}
@@ -2929,15 +3012,15 @@
 \end{tabular}
 \end{center}
 
-An alternative would be to introduce a separate type of formulas, but this
-would require separate parsing and printing support. We will avoid this, for
-the sake of simplicity.
-
-\subsubsection*{Preprocessing formulas}
-
-It's convenient if the main part of the prover need not cope with implications
-and `if and only if's. Therefore we first define a function that eliminates
-these in favour of the other connectives.
+% An alternative would be to introduce a separate type of formulas, but this
+% would require separate parsing and printing support. We will avoid this, for
+% the sake of simplicity.
+
+\subsubsection*{��������������� ��������� ������}
+
+% It's convenient if the main part of the prover need not cope with 
implications
+% and `if and only if's. Therefore we first define a function that eliminates
+% these in favour of the other connectives.
 
 \begin{boxed}\begin{lstlisting}
   let rec proc tm =
@@ -2955,10 +3038,10 @@
     | t -> t;;
 \end{lstlisting}\end{boxed}
 
-The next step is to push the negations down the formula, putting it into
-so-called `negation normal form' (NNF). We define two mutually recursive
-functions that create NNF for a formula, and
-its negation.
+% The next step is to push the negations down the formula, putting it into
+% so-called `negation normal form' (NNF). We define two mutually recursive
+% functions that create NNF for a formula, and
+% its negation.
 
 \begin{boxed}\begin{lstlisting}
   let rec nnf_p tm =
@@ -2980,15 +3063,15 @@
     | t -> Fn("~",[t]);;
 \end{lstlisting}\end{boxed}
 
-We will convert the negation of the input formula into negation normal form,
-and the main prover will then try to derive a contradiction from it. This will
-suffice to prove the original formula.
-
-\subsubsection*{The main prover}
-
-At each stage, the prover has a current formula, a list of formulas yet to be
-considered, and a list of literals. It is trying to reach a contradiction. The
-following strategy is employed:
+% We will convert the negation of the input formula into negation normal form,
+% and the main prover will then try to derive a contradiction from it. This 
will
+% suffice to prove the original formula.
+
+\subsubsection*{������� ������������}
+
+% At each stage, the prover has a current formula, a list of formulas yet to be
+% considered, and a list of literals. It is trying to reach a contradiction. 
The
+% following strategy is employed:
 
 \begin{itemize}
 
@@ -3067,7 +3150,7 @@
 required and any toplevel instantiations, throwing away instantiations for
 internally created variables.
 
-\subsubsection*{Examples}
+\subsubsection*{�������}
 
 Here are some simple examples from \citeN{pelletier-problems}.
 
@@ -3127,7 +3210,7 @@
   P55' : int * (string * term) list = 6, ["X", `agatha`]
 \end{verbatim}\end{boxed}
 
-\section*{Further reading}
+\section*{���������� ������}
 
 Symbolic differentiation is a classic application of functional languages.
 Other symbolic operations are major research issues in their own right ---
@@ -3162,7 +3245,7 @@
 another important theorem proving method conveniently based on Prolog-style
 search, look at the Prolog Technology Theorem Prover \cite{stickel-pttp}.
 
-\section*{Exercises}
+\section*{����������}
 
 \begin{enumerate}
 
_______________________________________________
Funprog-ru mailing list
Funprog-ru@xxxxxxxxxxx
http://www.sxemacs.org/mailman/listinfo/funprog-ru
<Prev in Thread] Current Thread [Next in Thread>
  • [Funprog-ru] [funprog-ru commit] r167 - trunk/ru, codesite-noreply <=