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

Rewrote first person in sections 2 and onwards

Browse source
This commit is contained in:
Wen Kokke 2019-07-14 14:21:39 +01:00
parent b6f3363aa1
commit 92c250e7d5
1 changed files with 55 additions and 64 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

119
papers/scp/PLFA.tex
View file

@ -388,10 +388,10 @@ available for Agda.
There is more material that would be desirable to include in PLFA 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 which was not due to limits of time. In future years, PLFA may be
extended to cover additional material, including mutable references, extended to cover additional material, including mutable references,
normalisation, System F, pure type systems, and denotational normalisation, System F, and pure type systems.
semantics. I'd especially like to include pure type systems as they 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 book. My attempts so far to formalise pure type systems used in the book. Our attempts so far to formalise pure type systems
have proved challenging, to say the least. have proved challenging, to say the least.
\section{Proofs in Agda and Coq} \section{Proofs in Agda and Coq}
@ -421,23 +421,16 @@ have proved challenging, to say the least.
\label{fig:sf-progress-2} \label{fig:sf-progress-2}
\end{figure} \end{figure}
% \begin{figure}[t]
% \includegraphics[width=\textwidth]{figures/sf-progress-3.png}
% \caption{SF, Progress (3/3)}
% \label{fig:sf-progress-3}
% \end{figure}
The introduction listed several reasons for preferring Agda over Coq. The introduction listed several reasons for preferring Agda over Coq.
But Coq tactics enable more compact proofs. Would it be possible for But Coq tactics enable more compact proofs. Would it be possible for
PLFA to cover the same material as SF, or would the proofs PLFA to cover the same material as SF, or would the proofs
balloon to unmanageable size? balloon to unmanageable size?
As an experiment, I first rewrote SF's development of simply-typed As an experiment, Philip first rewrote SF's development of simply-typed lambda
lambda calculus (SF, Chapters Stlc and StlcProp) in Agda. I was a calculus (SF, Chapters Stlc and StlcProp) in Agda. He was a newbie to Agda, and
newbie to Agda, and translating the entire development, sticking as translating the entire development, sticking as closely as possible to the
closely as possible to the development in SF, took me about two days. development in SF, took about two days. We were pleased to discover that the
I was pleased to discover that the proofs remained about the same proofs remained about the same size.
size.
There was also a pleasing surprise regarding the structure of the There was also a pleasing surprise regarding the structure of the
proofs. While most proofs in both SF and PLFA are carried out by proofs. While most proofs in both SF and PLFA are carried out by
@ -446,7 +439,7 @@ central proof, that substitution preserves types, is carried out by
induction on terms for a technical reason induction on terms for a technical reason
(the context is extended by a variable binding, and hence not (the context is extended by a variable binding, and hence not
sufficiently ``generic'' to work well with Coq's induction tactic). In sufficiently ``generic'' to work well with Coq's induction tactic). In
Agda, I had no trouble formulating the same proof over evidence that Agda, we had no trouble formulating the same proof over evidence that
the term is well typed, and didn't even notice SF's description of the the term is well typed, and didn't even notice SF's description of the
issue until I was done. issue until I was done.
@ -456,12 +449,12 @@ deterministic. There are 18 cases, one case per line. Ten of the
cases deal with the situation where there are potentially two cases deal with the situation where there are potentially two
different reductions; each case is trivially shown to be different reductions; each case is trivially shown to be
impossible. Five of the ten cases are redundant, as they just involve impossible. Five of the ten cases are redundant, as they just involve
switching the order of the arguments. I had to copy the cases switching the order of the arguments. We had to copy the cases
suitably permuted. It would be preferable to reinvoke the proof on suitably permuted. It would be preferable to reinvoke the proof on
switched arguments, but this would not pass Agda's termination checker switched arguments, but this would not pass Agda's termination checker
since swapping the arguments doesn't yield a recursive call on since swapping the arguments doesn't yield a recursive call on
structurally smaller arguments. I suspect tactics could cut down the structurally smaller arguments. We suspect tactics could cut down the
proof significantly. I 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
@ -470,12 +463,12 @@ and postconditions and generates the necessary
verification conditions. The conditions are then verified by a custom verification conditions. The conditions are then verified by a custom
tactic, where any questions of arithmetic are resolved by the tactic, where any questions of arithmetic are resolved by the
``omega'' tactic invoking a decision procedure. The entire ``omega'' tactic invoking a decision procedure. The entire
exercise would be easy to repeat in Agda, save for the last step: I exercise would be easy to repeat in Agda, save for the last step: we
suspect Agda's automation would not be up to verifying the generated suspect Agda's automation would not be up to verifying the generated
conditions, requiring tedious proofs by hand. However, I had already conditions, requiring tedious proofs by hand. However, we had already
decided to omit Hoare logic in order to focus on lambda calculus. decided to omit Hoare logic in order to focus on lambda calculus.
To give a flavour of how the texts compare, I 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.
Figures~\ref{fig:plfa-progress-1} and \ref{fig:plfa-progress-2} Figures~\ref{fig:plfa-progress-1} and \ref{fig:plfa-progress-2}
are taken from PLFA, Chapter Properties, are taken from PLFA, Chapter Properties,
@ -495,20 +488,19 @@ it easy to use a line of dashes to separate hypotheses from conclusion
in inference rules. The proof of proposition \texttt{progress} (the different in inference rules. The proof of proposition \texttt{progress} (the different
case making it a distinct name) is layed out carefully. The neat case making it a distinct name) is layed out carefully. The neat
indented structure emphasises the case analysis, and all right-hand indented structure emphasises the case analysis, and all right-hand
sides line-up in the same column. My hope as an author is that students sides line-up in the same column. Our hope as authors is that students
will read the formal proof first, and use it as a tabular guide will read the formal proof first, and use it as a tabular guide
to the informal explanation that follows. to the informal explanation that follows.
SF puts the informal explanation first, followed by the formal proof. SF puts the informal explanation first, followed by the formal proof. The text
The text hides the formal proof script under an icon; hides the formal proof script under an icon; the figure shows what appears when
the figure shows what appears when the icon is expanded. the icon is expanded. As teachers, we were aware that students might skip the
As a teacher I was aware that formal proof on a first reading, and we would have to hope the students would
students might skip it on a first reading, and I would have to hope the return to it and step through it with an interactive tool in order to make it
students would return to it and step through it with an interactive intelligible. We expect the students skipped over many such proofs. This
tool in order to make it intelligible. I expect the students skipped over particular proof forms the basis for a question of the mock exam and the past
many such proofs. This particular proof forms the basis for a question exams, so we expect most students will actually look at this one if not all the
of the mock exam and the past exams, so I expect most students will actually others.
look at this one if not all the others.
\newcommand{\ex}{\texttt{x}} \newcommand{\ex}{\texttt{x}}
\newcommand{\why}{\texttt{y}} \newcommand{\why}{\texttt{y}}
@ -569,7 +561,7 @@ recorded. Students may recreate it by commenting out bits of code and
introducing a hole in their place. PLFA contains some prose descriptions introducing a hole in their place. PLFA contains some prose descriptions
of interactively building code, but mainly contains code that students of interactively building code, but mainly contains code that students
can read. They may also introduce holes to interact with the code, but can read. They may also introduce holes to interact with the code, but
I expect this will be rarer than with SF. we expect this will be rarer than with SF.
SF encourages students to interact with all the scripts in the text. SF encourages students to interact with all the scripts in the text.
Trying to understand a Coq proof script without running it Trying to understand a Coq proof script without running it
@ -581,9 +573,9 @@ Understanding the code often requires working out the types, but
head; when it is not easy, students still have the option of head; when it is not easy, students still have the option of
interaction. interaction.
While students are keen to interact to create code, I have found they While students are keen to interact to create code, we have found they
are reluctant to interact to understand code created by others. For are reluctant to interact to understand code created by others. For
this reason, I suspect this may make Agda a more suitable vehicle for this reason, we suspect this may make Agda a more suitable vehicle for
teaching. Nate Foster suggests this hypothesis is ripe to be tested teaching. Nate Foster suggests this hypothesis is ripe to be tested
empirically, perhaps using techniques similar to those of empirically, perhaps using techniques similar to those of
\citet{Danas-et-al-2017}. \citet{Danas-et-al-2017}.
@ -635,7 +627,8 @@ Redex \citep{Felleisen-et-al-2009} and K \citep{Rosu-Serbanuta-2010},
advertise as one of their advantages that they can generate advertise as one of their advantages that they can generate
a prototype from descriptions of the reduction rules. a prototype from descriptions of the reduction rules.
I was therefore surprised to realise that any constructive proof of % TODO: rewrite use of 'Philip' to reflect all authors?
Philip was therefore surprised to realise that any constructive proof of
progress and preservation \emph{automatically} gives rise to such a progress and preservation \emph{automatically} gives rise to such a
prototype. The input is a term together with evidence the term is prototype. The input is a term together with evidence the term is
well-typed. (In the inherently-typed case, these are the same thing.) well-typed. (In the inherently-typed case, these are the same thing.)
@ -659,7 +652,7 @@ improve readability; in addition, the text includes examples of
running the evaluator with its unedited output. running the evaluator with its unedited output.
It is immediately obvious that progress and preservation make it It is immediately obvious that progress and preservation make it
trivial to construct a prototype evaluator, and yet I cannot find such trivial to construct a prototype evaluator, and yet we cannot find such
an observation in the literature nor mentioned in an introductory an observation in the literature nor mentioned in an introductory
text. It does not appear in SF, nor in \citet{Harper-2016}. A plea text. It does not appear in SF, nor in \citet{Harper-2016}. A plea
to the Agda mailing list failed to turn up any prior mentions. to the Agda mailing list failed to turn up any prior mentions.
@ -667,7 +660,7 @@ The closest related observation I have seen in the published
literature is that evaluators can be extracted from proofs of literature is that evaluators can be extracted from proofs of
normalisation \citep{Berger-1993,Dagand-and-Scherer-2015}. normalisation \citep{Berger-1993,Dagand-and-Scherer-2015}.
(Late addition: My plea to the Agda list eventually bore fruit. Oleg (Late addition: Our plea to the Agda list eventually bore fruit. Oleg
Kiselyov directed me to unpublished remarks on his web page where he Kiselyov directed me to unpublished remarks on his web page where he
uses the name \texttt{eval} for a proof of progress and notes ``the uses the name \texttt{eval} for a proof of progress and notes ``the
very proof of type soundness can be used to evaluate sample very proof of type soundness can be used to evaluate sample
@ -688,12 +681,13 @@ expressions'' \citep{Kiselyov-2009}.)
\label{fig:inherent} \label{fig:inherent}
\end{figure} \end{figure}
% TODO: consider rewriting this?
The second part of PLFA first discusses two different approaches to The second part of PLFA first discusses two different approaches to
modeling simply-typed lambda calculus. It first presents raw modeling simply-typed lambda calculus. It first presents raw
terms with named variables and a separate typing relation and terms with named variables and a separate typing relation and
then shifts to inherently-typed terms with de Bruijn indices. then shifts to inherently-typed terms with de Bruijn indices.
Before writing the text, I had thought the two approaches Before writing the text, Philip had thought the two approaches
complementary, with no clear winner. Now I am convinced that the complementary, with no clear winner. Now he is convinced that the
inherently-typed approach is superior. inherently-typed approach is superior.
Figure~\ref{fig:raw} presents the raw approach. Figure~\ref{fig:raw} presents the raw approach.
@ -714,29 +708,25 @@ the types of variables and terms are indexed by a context and a type,
so that $\GG\:{\ni}\:\AY$ and $\GG\:{\vdash}\:\AY$ denote so that $\GG\:{\ni}\:\AY$ and $\GG\:{\vdash}\:\AY$ denote
variables and terms, respectively, that under context $\GG$ have type $\AY$. variables and terms, respectively, that under context $\GG$ have type $\AY$.
The indexed types closely resemble the previous judgments: The indexed types closely resemble the previous judgments:
we now represent a variable or a term by the proof that it is well-typed. we now represent a variable or a term by the proof that it is well typed.
In particular, the proof that a variable is well-typed in the raw approach In particular, the proof that a variable is well typed in the raw approach
corresponds to a de Bruijn index in the inherent approach. corresponds to a de Bruijn index in the inherent approach.
The raw approach requires more lines of code than The raw approach requires more lines of code than the inherent approach. The
the inherent approach. The separate definition of raw separate definition of raw terms is not needed in the inherent approach; and one
terms is not needed in the inherent judgment in the raw approach needs to check that $\ex \not\equiv \why$, while
approach; and one judgment in the raw approach needs to check that the corresponding judgment in the inherent approach does not. The difference
$\ex \not\equiv \why$, while the corresponding judgment in the becomes more pronounced when including the code for substitution, reductions,
inherent approach does not. The difference becomes more pronounced and proofs of progress and preservation. In particular, where the raw approach
when including the code for substitution, reductions, and proofs of requires one first define substitution and reduction and then prove they
progress and preservation. In particular, where the raw approach preserve types, the inherent approach establishes substitution at the same time
requires one first define substitution and reduction and then prove it defines substitution and reduction.
they preserve types, the inherent approach establishes substitution at
the same time it defines substitution and reduction.
Stripping Stripping out examples and any proofs that appear in one but not the other (but
out examples and any proofs that appear in one but not the other (but could have appeared in both), the full development in PLFA for the raw approach
could have appeared in both), the full development in PLFA for the raw approach takes 451 takes 451 lines (216 lines of definitions and 235 lines for the proofs) and the
lines (216 lines of definitions and 235 lines for the proofs) and the development for the inherent approach takes 275 lines (with definitions and
development for the inherent approach takes 275 lines (with proofs interleaved). We have 451 / 235 = 1.64, close to the golden ratio.
definitions and proofs interleaved). We have 451 / 235 = 1.64,
close to the golden ratio.
The inherent approach also has more expressive power. The raw The inherent approach also has more expressive power. The raw
approach is restricted to substitution of one variable by a closed approach is restricted to substitution of one variable by a closed
@ -744,11 +734,12 @@ term, while the inherent approach supports simultaneous substitution
of all variables by open terms, using a pleasing formulation due to of all variables by open terms, using a pleasing formulation due to
\citet{McBride-2005}, inspired by \citet{Goguen-and-McKinna-1997} and \citet{McBride-2005}, inspired by \citet{Goguen-and-McKinna-1997} and
\citet{Altenkirch-and-Reus-1999} and described in \citet{Altenkirch-and-Reus-1999} and described in
\citet{Allais-et-al-2017}. In fact, I did manage to write a variant of \citet{Allais-et-al-2017}. In fact, we did manage to write a variant of
the raw approach with simultaneous open substitution along the lines the raw approach with simultaneous open substitution along the lines
of McBride, but the result was too complex for use in an introductory of McBride, but the result was too complex for use in an introductory
text, requiring 695 lines of code---more than the total for the other text, requiring 695 lines of code---more than the total for the other
two approaches combined. two approaches combined.
% TODO: is this still available somewhere in extra/?
The text develops both approaches because the raw approach is more The text develops both approaches because the raw approach is more
familiar, and because placing the inherent approach first would familiar, and because placing the inherent approach first would
@ -768,12 +759,12 @@ The benefits of the inherent approach
are well known to some. The technique was introduced by are well known to some. The technique was introduced by
\citet{Altenkirch-and-Reus-1999}, and widely used elsewhere, \citet{Altenkirch-and-Reus-1999}, and widely used elsewhere,
notably by \citet{Chapman-2009} and \citet{Allais-et-al-2017}. notably by \citet{Chapman-2009} and \citet{Allais-et-al-2017}.
I'm grateful to David Darais for bringing it to my attention. Philip is grateful to David Darais for bringing it to his attention.
\section{Conclusion} \section{Conclusion}
I look forward to experience teaching from the new text, We look forward to experience teaching from the new text,
and encourage others to use it too. Please comment! and encourage others to use it too. Please comment!