michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Rewrote section on tactics and Hoare logic

Browse source
This commit is contained in:
Wen Kokke 2019-07-14 16:09:07 +01:00
parent 92c250e7d5
commit 038358aad1
2 changed files with 81 additions and 38 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

37
papers/scp/PLFA.bib
View file

@ -374,3 +374,40 @@
Title = {A filter lambda model and the completeness of type assignment}, Title = {A filter lambda model and the completeness of type assignment},
Volume = {48}, Volume = {48},
Year = {1983}} Year = {1983}}
@inproceedings{Kokke-2015,
abstract = {As proofs in type theory become increasingly
complex, there is a growing need to provide better
proof automation. This paper shows how to implement
a Prolog-style resolution procedure in the
dependently typed programming language
Agda. Connecting this resolution procedure to Agda’s
reflection mechanism provides a first-class proof
search tactic for first-order Agda terms. As a
result, writing proof automation tactics need not be
different from writing any other program. },
year = {2015},
month = jun,
isbn = {978-3-319-19796-8},
booktitle = {Mathematics of Program Construction},
volume = {9129},
series = {Lecture Notes in Computer Science},
editor = {Hinze, Ralf and Voigtländer, Janis},
doi = {10.1007/978-3-319-19797-5_14},
title = {Auto in Agda: Programming Proof Search Using Reflection},
url = {https://wenkokke.github.io/pubs/mpc2015.pdf},
publisher = {Springer International Publishing},
author = {Wen Kokke and Wouter Swierstra},
pages = {276-301}}
@thesis{Kidney-2019,
address = {Cork, Ireland},
type = {Bachelor thesis},
title = {Automatically and {Efficiently} {Illustrating} {Polynomial} {Equalities} in {Agda}},
url = {https://doisinkidney.com/pdfs/bsc-thesis.pdf},
abstract = {We present a new library which automates the construction of equivalence proofs between polynomials over commutative rings and semirings in the programming language Agda [20]. It is signi cantly faster than Agda’s existing solver. We use re ection to provide a sim- ple interface to the solver, and demonstrate how to use the constructed proofs to provide step-by-step solutions.},
language = {en},
school = {University College Cork},
author = {Kidney, Donnacha Oisín},
month = apr,
year = {2019}}

82
papers/scp/PLFA.tex
View file

@ -371,28 +371,27 @@ PLFA and SF differ in several particulars. PLFA begins with a computationally
complete language, PCF, while SF begins with a minimal language, simply-typed complete language, PCF, while SF begins with a minimal language, simply-typed
lambda calculus with booleans. PLFA does not include type annotations in terms, lambda calculus with booleans. PLFA does not include type annotations in terms,
and uses bidirectional type inference, while SF has terms with unique types and and uses bidirectional type inference, while SF has terms with unique types and
uses type checking. SF also covers a simple imperative language with Hoare logic, uses type checking. SF also covers a simple imperative language with Hoare
and for lambda calculus covers subtyping, record types, mutable references, and normalisation logic, and for lambda calculus covers subtyping, record types, mutable
---none of which are treated by PLFA. PLFA covers an inherently-typed de Bruijn references, and normalisation---none of which are treated by PLFA. PLFA covers
representation, bidirectional type inference, bisimulation, and an an inherently-typed de Bruijn representation, bidirectional type inference,
untyped call-by-name language with full normalisation---none of which bisimulation, and an untyped call-by-name language with full
are treated by SF. normalisation---none of which are treated by SF.
SF has a third volume, written by Andrew Appel, on Verified Functional SF has a third volume, written by Andrew Appel, on Verified Functional
Algorithms. I'm not sufficiently familiar with that volume to have a view Algorithms. I'm not sufficiently familiar with that volume to have a view on
on whether it would be easy or hard to cover that material in Agda. whether it would be easy or hard to cover that material in Agda. And SF recently
And SF recently added a fourth volume on random testing of Coq specifications added a fourth volume on random testing of Coq specifications using QuickChick.
using QuickChick. There is currently no tool equivalent to QuickChick There is currently no tool equivalent to QuickChick available for Agda.
available for Agda.
There is more material that would be desirable to include in PLFA
which was not due to limits of time. In future years, PLFA may be There is more material that would be desirable to include in PLFA which was not
extended to cover additional material, including mutable references, due to limits of time. In future years, PLFA may be extended to cover
normalisation, System F, and pure type systems. additional material, including mutable references, normalisation, System F, and
We'd especially like to include pure type systems as they pure type systems. We'd especially like to include pure type systems as they
provide the readers with a formal model close to the dependent types provide the readers with a formal model close to the dependent types used in the
used in the book. Our attempts so far to formalise pure type systems book. Our attempts so far to formalise pure type systems have proved
have proved challenging, to say the least. challenging, to say the least.
\section{Proofs in Agda and Coq} \section{Proofs in Agda and Coq}
@ -457,16 +456,25 @@ structurally smaller arguments. We suspect tactics could cut down the
proof significantly. We tried to compare with SF's proof that reduction proof significantly. We tried to compare with SF's proof that reduction
is deterministic, but failed to find that proof. is deterministic, but failed to find that proof.
SF covers an imperative language with Hoare logic, culminating in SF covers an imperative language with Hoare logic, culminating in code that
code that takes an imperative programme suitably decorated with preconditions takes an imperative programme suitably decorated with preconditions and
and postconditions and generates the necessary postconditions and generates the necessary verification conditions. The
verification conditions. The conditions are then verified by a custom conditions are then verified by a custom tactic, where any questions of
tactic, where any questions of arithmetic are resolved by the arithmetic are resolved by the ``omega'' tactic invoking a decision procedure.
``omega'' tactic invoking a decision procedure. The entire The entire exercise would be easy to repeat in Agda, save for the last step, as
exercise would be easy to repeat in Agda, save for the last step: we Agda does not offer support for proof automation out of the box. It is
suspect Agda's automation would not be up to verifying the generated certainly possible to implement proof automation in Agda---see, e.g., the auto
conditions, requiring tedious proofs by hand. However, we had already tactic by \citet{Kokke-2015}, and the collection of tactics in Ulf Norell's
decided to omit Hoare logic in order to focus on lambda calculus. \texttt{agda-prelude}\footnote{\url{https://github.com/UlfNorell/agda-prelude}}.
The standard library comes equipped with solvers for equations on monoids and
rings\footnote{\url{https://agda.github.io/agda-stdlib/Algebra.Solver.Ring.html}},
and a much improved solver for equalities on rings was recently contributed by
\citet{Kidney-2019}.
We suspect that, while Agda's automation would be up to verifying the generated
conditions, some effort would be require to implement the required custom
tactic, and a section would need to be added to the book to cover proof
automation. For the time being, we have decided to omit Hoare logic in order to
focus on lambda calculus.
To give a flavour of how the texts compare, we show the To give a flavour of how the texts compare, we show the
proof of progress for simply-typed lambda calculus from both texts. proof of progress for simply-typed lambda calculus from both texts.
@ -770,15 +778,13 @@ and encourage others to use it too. Please comment!
\paragraph{Acknowledgments} \paragraph{Acknowledgments}
A special thank you to my coauthor, Wen Kokke. For inventing ideas on For inventing ideas on which PLFA is based, and for hand-holding, many thanks to
which PLFA is based, and for hand-holding, many thanks to Conor Conor McBride, James McKinna, Ulf Norell, and Andreas Abel. For showing me how
McBride, James McKinna, Ulf Norell, and Andreas Abel. For showing me much more compact it is to avoid raw terms, thanks to David Darais. For
how much more compact it is to avoid raw terms, thanks to David inspiring my work by writing SF, thanks to Benjamin Pierce and his coauthors.
Darais. For inspiring my work by writing SF, thanks to Benjamin For comments on a draft of this paper, an extra thank you to James McKinna, Ulf
Pierce and his coauthors. For comments on a draft of this paper, an Norell, Andreas Abel, and Benjamin Pierce. This research was supported by EPSRC
extra thank you to James McKinna, Ulf Norell, Andreas Abel, and Programme Grant EP/K034413/1.
Benjamin Pierce. This research was supported by EPSRC Programme Grant
EP/K034413/1.
\section*{References} \section*{References}