Commit acf066de authored by Dennis Müller's avatar Dennis Müller
Browse files

sec 5

parent 6bf086bf
......@@ -103,12 +103,12 @@
\section{Implementation \& Use Case}\label{sec:usecase}
\input{usecase}
\section{Low-hanging Fruit: Currently Unrealized Applications}
\section{Future Work}
\input{applications}
\section{Conclusion}\label{sec:concl}
\paragraph{Future Work} \ednote{term indexing}\ednote{Better normalizing (Norman's thesis)}
% \paragraph{Future Work} \ednote{term indexing}\ednote{Better normalizing (Norman's thesis)}
\paragraph{Acknowledgments}
The authors gratefully acknowledge financial support from the OpenDreamKit Horizon 2020
......
......@@ -36,13 +36,23 @@ The common logical framework used for all the libraries at our disposal -- name
\begin{itemize}
\item Free variables in a term, often occurences of theory parameters as e.g. used extensively in the PVS system, are replaced by holes.
\item For foundations that use product types, we curry function types $(A_1 \times\ldots A_n)\to B$ to $A_1 \to \ldots \to A_n\to B$. We treat lambda-expressions and applications accordingly.
For example: \[f = \lambda (n,m) : \mathbb N \times \mathbb N .\; n + m\text{ becomes } f = \lambda n : \mathbb N.\; \lambda m : \mathbb N .\; n + m\] \[f(\langle a, b\rangle)\text{ becomes }f(a,b).\]
\item Higher-order abstract syntax encodings are eliminated by raising atomic types, function types, applications and lambdas to the level of the logical framework. This eliminates (redundant) implicit arguments that only occur due to their formalization in the logical framework.
This has the advantage that possible differences between the types of the relevant subterms and implicit type arguments (e.g. in the presence of subtyping) do not negatively affect viewfinding.
\item We use the curry-howard correspondence to transform axioms and theorems of the form $\vdash (P\Rightarrow Q)$ to function types $\vdash P \to \vdash Q$. Analogously, we transform judgments of the form $\vdash \forall x : A.\;P$ to $\prod_{x:A}\vdash P$.
\item For classical logics, we afterwards rewrite all logical connectives using their usual definitions using negation and conjunction only. Double negations are eliminated.
For example, the apply-operator in the PVS meta-theory has the LF-type
\[(A : \cn{psvtype}) \to (B : \cn{pvstype}) \to \cn{pvsterm}_{A\Rightarrow B} \to \cn{pvsterm}_A \to \cn{pvsterm}_B \]
Hence every application of a function in pvs -- as \mmt-term: $\oma{\cn{pvsapply}}{A,B,f,a}$ -- has two additional implicit arguments, which we eliminate by replacing this expression by $\oma{f}{a}$.
This prevents false negatives due to mismatching type arguments in the presence of subtyping.
\item Since judgments -- in our imports -- correspond to constants of type $\vdash P$ for some proposition $P$, we can use the curry-howard form, we can use the curry-howard correspondence to equate the type $\vdash (P \Rightarrow Q)$ with the function type $(\vdash P) \to (\vdash Q)$, as well as the judgment $\vdash \forall x : A.\;P$ with the function type $(x:A) \to \vdash P$.
Since both styles of formalization are more or less preferred in different systems, we replace each occurence of the former by the latter.
\item For classical logics, we rewrite all remaining logical connectives using their usual definitions on the basis of negation and conjunction only. Double negations are eliminated.
\item Typed Equalities are transformed to untyped ones; again getting rid of the redundant type argument of the equality.
\item The arguments of conjunctions and equalities are reordered (currently only by their number of subterms).
For example, the typed equality $\oma{\cn{equals}}{\mathbb N,2,1+1}$ becomes $\oma{\cn{equals}}{2,1+1}$, allowing to match the same equation on e.g. the real numbers.
\item The arguments of conjunctions and equalities are ordered (currently only by their number of subterms).
\end{itemize}
\subsection{Implementation}\label{sec:pvs}
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment