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
|