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 Unified Diffs Ignore Whitespace Patch

Changes to report/arend-report.tex.

893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
....
1324
1325
1326
1327
1328
1329
1330









































1331
1332
1333
1334
1335
1336
1337
    {\Gamma, P(y) |- G}
    {\Gamma, \exists x: P(x) |- G}
\]

% Unification rules
\[
\inference[$=_R$]
    {[t_1 = t_2]}
    {\Gamma |- t_1 = t_2}
\qquad\qquad
\inference[$=_L$]
    {\Gamma_{[t_1 = t_2]} |- G_{[t_1 = t_2]}}
    {\Gamma, t_1 = t_2 |- G}
\]

% Atomic goals
................................................................................
capturing the names $S$ and $T$, respectively, within their bodies. Thus, to
apply a substitution $X \mapsto 1$ to $\forall X, P(X)$ it is \emph{not}
correct to give $\forall 1, P(1)$. In addition, consider the problem of 
applying the substitution 
$X \mapsto Y$ to $\forall Y, P(X,Y)$; clearly, one of the $Y$'s will need to 
be renamed. Since the $Y$ in the substitution is most likely bound somewhere
else in the derivation, we choose to rename the $Y$ bound within the $\forall$.










































\subsection{Unification}

The Robinson unification algorithm is presented, in natural deduction style,
 in figure~\ref{unification-rules}. 
 Note that the same algorithm is used, with minor 
modification, in both the Javascript and Prolog implementations (for a direct







|
|







 







>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>







893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
....
1324
1325
1326
1327
1328
1329
1330
1331
1332
1333
1334
1335
1336
1337
1338
1339
1340
1341
1342
1343
1344
1345
1346
1347
1348
1349
1350
1351
1352
1353
1354
1355
1356
1357
1358
1359
1360
1361
1362
1363
1364
1365
1366
1367
1368
1369
1370
1371
1372
1373
1374
1375
1376
1377
1378
    {\Gamma, P(y) |- G}
    {\Gamma, \exists x: P(x) |- G}
\]

% Unification rules
\[
\inference[$=_R$]
    {}
    {\Gamma |- t = t}
\qquad\qquad
\inference[$=_L$]
    {\Gamma_{[t_1 = t_2]} |- G_{[t_1 = t_2]}}
    {\Gamma, t_1 = t_2 |- G}
\]

% Atomic goals
................................................................................
capturing the names $S$ and $T$, respectively, within their bodies. Thus, to
apply a substitution $X \mapsto 1$ to $\forall X, P(X)$ it is \emph{not}
correct to give $\forall 1, P(1)$. In addition, consider the problem of 
applying the substitution 
$X \mapsto Y$ to $\forall Y, P(X,Y)$; clearly, one of the $Y$'s will need to 
be renamed. Since the $Y$ in the substitution is most likely bound somewhere
else in the derivation, we choose to rename the $Y$ bound within the $\forall$.

\subsection{Universal and Existential Quantification}

In the specification language, variables are implicitly quantified: variables
occurring in the head of a clause are universally quantified, while 
variables that occur \emph{only} in the body of a clause are existentially
quantified.\marginnote{This is the same as the implicit quantifications rules
for Prolog.} However, the reasoning language supports both implicit and 
explicit quantification. We wish to preserve compatibility between the two
languages, so that queries which are provable in the specification language,
are also provable in the reasoning language. For this reason, we adopt the
following scheme with regard to implicitly quantified variables in 
reasoning queries:
\begin{itemize}
\item An unquantified variable occurring \emph{to the left} of an implication
    is implicitly $\forall$-quantified.
\item An unqualified variable occurring to the \emph{right} of an implication
    is implicitly $\exists$-quantified. 
\end{itemize}

Note that, if \texttt{:-} is regarded as $\leftarrow$, this is the opposite of
the implicit quantification in the specification. However, these rules match
the normal expectation for proof-style statements. For example:
\begin{itemize}
\item $\mathsf{nat}(X) -> \mathsf{add}(X,a,X)$ is equivalent to 
    $\forall X: \mathsf{nat}(X) -> \mathsf{add}(X,a,X)$.
\item $\mathsf{nat}(X) \land \mathsf{nat}(Y) -> \mathsf{add}(X,Y,Z) \land
    \mathsf{nat}(Z)$ is equivalent to $\forall X,Y: \mathsf{nat}(X) \land 
    \mathsf{nat}(Y) -> \exists Z: \mathsf{add}(X,Y,Z) \land \mathsf{nat}(Z)$.
\end{itemize}

Internally, when processing a proof tree, Arend maintains two sets of 
in-scope variables: \emph{universals} and \emph{existentials}. Universals are
those introduced by the $\forall$-R and $\exists$-L rules; they implicitly
represent fresh \emph{constants} and cannot be bound by unification. 
Existentials are introduced by $\exists$-R and $\forall$-L rules; they are
true variables which have simply not been instantiated yet. In fact, the
behavior of unification is to supply the instantiation of one or more 
existential variables, possibly in terms of the in-scope universal variables.



\subsection{Unification}

The Robinson unification algorithm is presented, in natural deduction style,
 in figure~\ref{unification-rules}. 
 Note that the same algorithm is used, with minor 
modification, in both the Javascript and Prolog implementations (for a direct