Check-in [e8532f2591]

Not logged in

Many hyperlinks are disabled.
Use anonymous login to enable hyperlinks.

Overview
Comment:Started work on better handling of forall/exists in the reasoning language.
Downloads: Tarball | ZIP archive | SQL archive
Timelines: family | ancestors | descendants | both | forall-exists
Files: files | file ages | folders
SHA1:e8532f259168f79209908995035387b5099cdc88
User & Date: andy 2015-04-21 21:35:42
Context
2015-04-22
10:29
Presentation work. Added PDF of presentation. Leaf check-in: a24ff57f47 user: andy tags: trunk
2015-04-21
21:35
Started work on better handling of forall/exists in the reasoning language. Leaf check-in: e8532f2591 user: andy tags: forall-exists
19:26
The new clausal-expansion system for goals is complete. Closed-Leaf check-in: d8a8e82a90 user: andy tags: bc-subst
Changes
Hide Diffs Side-by-Side Diffs Ignore Whitespace Patch

Changes to report/arend-report.tex.

   893    893       {\Gamma, P(y) |- G}
   894    894       {\Gamma, \exists x: P(x) |- G}
   895    895   \]
   896    896   
   897    897   % Unification rules
   898    898   \[
   899    899   \inference[$=_R$]
   900         -    {[t_1 = t_2]}
   901         -    {\Gamma |- t_1 = t_2}
          900  +    {}
          901  +    {\Gamma |- t = t}
   902    902   \qquad\qquad
   903    903   \inference[$=_L$]
   904    904       {\Gamma_{[t_1 = t_2]} |- G_{[t_1 = t_2]}}
   905    905       {\Gamma, t_1 = t_2 |- G}
   906    906   \]
   907    907   
   908    908   % Atomic goals
................................................................................
  1324   1324   capturing the names $S$ and $T$, respectively, within their bodies. Thus, to
  1325   1325   apply a substitution $X \mapsto 1$ to $\forall X, P(X)$ it is \emph{not}
  1326   1326   correct to give $\forall 1, P(1)$. In addition, consider the problem of 
  1327   1327   applying the substitution 
  1328   1328   $X \mapsto Y$ to $\forall Y, P(X,Y)$; clearly, one of the $Y$'s will need to 
  1329   1329   be renamed. Since the $Y$ in the substitution is most likely bound somewhere
  1330   1330   else in the derivation, we choose to rename the $Y$ bound within the $\forall$.
         1331  +
         1332  +\subsection{Universal and Existential Quantification}
         1333  +
         1334  +In the specification language, variables are implicitly quantified: variables
         1335  +occurring in the head of a clause are universally quantified, while 
         1336  +variables that occur \emph{only} in the body of a clause are existentially
         1337  +quantified.\marginnote{This is the same as the implicit quantifications rules
         1338  +for Prolog.} However, the reasoning language supports both implicit and 
         1339  +explicit quantification. We wish to preserve compatibility between the two
         1340  +languages, so that queries which are provable in the specification language,
         1341  +are also provable in the reasoning language. For this reason, we adopt the
         1342  +following scheme with regard to implicitly quantified variables in 
         1343  +reasoning queries:
         1344  +\begin{itemize}
         1345  +\item An unquantified variable occurring \emph{to the left} of an implication
         1346  +    is implicitly $\forall$-quantified.
         1347  +\item An unqualified variable occurring to the \emph{right} of an implication
         1348  +    is implicitly $\exists$-quantified. 
         1349  +\end{itemize}
         1350  +
         1351  +Note that, if \texttt{:-} is regarded as $\leftarrow$, this is the opposite of
         1352  +the implicit quantification in the specification. However, these rules match
         1353  +the normal expectation for proof-style statements. For example:
         1354  +\begin{itemize}
         1355  +\item $\mathsf{nat}(X) -> \mathsf{add}(X,a,X)$ is equivalent to 
         1356  +    $\forall X: \mathsf{nat}(X) -> \mathsf{add}(X,a,X)$.
         1357  +\item $\mathsf{nat}(X) \land \mathsf{nat}(Y) -> \mathsf{add}(X,Y,Z) \land
         1358  +    \mathsf{nat}(Z)$ is equivalent to $\forall X,Y: \mathsf{nat}(X) \land 
         1359  +    \mathsf{nat}(Y) -> \exists Z: \mathsf{add}(X,Y,Z) \land \mathsf{nat}(Z)$.
         1360  +\end{itemize}
         1361  +
         1362  +Internally, when processing a proof tree, Arend maintains two sets of 
         1363  +in-scope variables: \emph{universals} and \emph{existentials}. Universals are
         1364  +those introduced by the $\forall$-R and $\exists$-L rules; they implicitly
         1365  +represent fresh \emph{constants} and cannot be bound by unification. 
         1366  +Existentials are introduced by $\exists$-R and $\forall$-L rules; they are
         1367  +true variables which have simply not been instantiated yet. In fact, the
         1368  +behavior of unification is to supply the instantiation of one or more 
         1369  +existential variables, possibly in terms of the in-scope universal variables.
         1370  +
         1371  +
  1331   1372   
  1332   1373   \subsection{Unification}
  1333   1374   
  1334   1375   The Robinson unification algorithm is presented, in natural deduction style,
  1335   1376    in figure~\ref{unification-rules}. 
  1336   1377    Note that the same algorithm is used, with minor 
  1337   1378   modification, in both the Javascript and Prolog implementations (for a direct