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

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