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  forallexists 
Files:  files  file ages  folders 
SHA1:  e8532f259168f79209908995035387b5099cdc88 
User & Date:  andy 20150421 21:35:42 
Context
20150422
 
10:29  Presentation work. Added PDF of presentation. Leaf checkin: a24ff57f47 user: andy tags: trunk  
20150421
 
21:35  Started work on better handling of forall/exists in the reasoning language. Leaf checkin: e8532f2591 user: andy tags: forallexists  
19:26  The new clausalexpansion system for goals is complete. ClosedLeaf checkin: d8a8e82a90 user: andy tags: bcsubst  
Changes
Changes to report/arendreport.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{unificationrules}. 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 proofstyle 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 inscope 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 inscope universal variables. \subsection{Unification} The Robinson unification algorithm is presented, in natural deduction style, in figure~\ref{unificationrules}. Note that the same algorithm is used, with minor modification, in both the Javascript and Prolog implementations (for a direct 