-
Notifications
You must be signed in to change notification settings - Fork 83
/
frap_book.tex
6172 lines (4924 loc) · 375 KB
/
frap_book.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
\documentclass{amsbook}
\usepackage{hyperref,url,amsmath,amssymb,proof,stmaryrd,tikz-cd,mathabx}
\newtheorem{theorem}{Theorem}[chapter]
\newtheorem{lemma}[theorem]{Lemma}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{example}[theorem]{Example}
\newtheorem{xca}[theorem]{Exercise}
\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}
\numberwithin{section}{chapter}
\numberwithin{equation}{chapter}
\makeindex
\begin{document}
\frontmatter
\title{Formal Reasoning About Programs}
\author{Adam Chlipala}
\address{MIT, Cambridge, MA, USA}
\email{[email protected]}
\begin{abstract}
\emph{Briefly}, this book is about an approach to bringing software engineering up to speed with more traditional engineering disciplines, providing a mathematical foundation for rigorous analysis of realistic computer systems. As civil engineers apply their mathematical canon to reach high certainty that bridges will not fall down, the software engineer should apply a different canon to argue that programs behave properly. As other engineering disciplines have their computer-aided-design tools, computer science has proof assistants, IDEs for logical arguments. We will learn how to apply these tools to certify that programs behave as expected.
\emph{More specifically}: Introductions to two intertangled subjects: the Coq proof assistant, a tool for machine-checked mathematical theorem proving; and formal logical reasoning about the correctness of programs.
\end{abstract}
\maketitle
\newpage
For more information, see the book's home page:
\begin{center} \url{http://adam.chlipala.net/frap/} \end{center}
\thispagestyle{empty}
\mbox{}\vfill
\begin{center}
Copyright Adam Chlipala 2015-2021.
This work is licensed under a
Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.
The license text is available at:
\end{center}
\begin{center} \url{https://creativecommons.org/licenses/by-nc-nd/4.0/} \end{center}
\newpage
\setcounter{page}{4}
\tableofcontents
\mainmatter
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\chapter{Why Prove the Correctness of Programs?}
The classic engineering disciplines all have their standard mathematical techniques that are applied to the design of any artifact, before it is deployed, to gain confidence about its safety, suitability for some purpose, and so on.
The engineers in a discipline more or less agree on what are ``the rules'' to be followed in vetting a design.
Those rules are specified with a high degree of rigor, so that it isn't a matter of opinion whether a design is safe.
Why doesn't software engineering have a corresponding agreed-upon standard, whereby programmers convince themselves that their systems are safe, secure, and correct?
The concepts and tools may not quite be ready yet for broad adoption, but they have been under development for decades.
This book introduces one particular tool and a body of ideas for how to apply it to different tasks in program proof.
As this document is in a very early draft stage, no more will be said here, in favor of jumping right into the technical material.
Eventually, there will no doubt be some sort of historical overview here, as part of a general placing-in-context of the particular approach that will come next.
There will also be plenty of scholarly citations (here and throughout the book).
In this early version, you get to take the author's word for it that we are about to learn a promising approach!
However, one overarching element of our strategy is important enough to deserve to be called out here.
We will study a variety of different approaches for formalizing what a program should do and for proving that a program does what it should.
At every step, we will pay close attention to the \emph{common foundation} that underlies everything.
For one thing, we will be proving all of our theorems with the Coq proof assistant\footnote{The author only makes an effort to keep the associated Coq code working with the latest Coq version, which is 8.16 as of this writing.}, a powerful framework for writing and machine-checking proofs.
Coq itself is based on a relatively small set of core features, much like a well-designed programming language, and in both we build up increasingly sophisticated abstractions as libraries.
Those features can be thought of as the core of all mathematical reasoning.
We will also apply a recipe specific to program proof.
When we encounter a new challenge, to prove a new kind of property about a new kind of program, we will generally be considering four broad elements that appear in nearly all techniques.
\begin{itemize}
\item \index{encoding}\textbf{Encoding.}
Every programming language has both \index{syntax}\emph{syntax}, which defines what programs look like, and \index{semantics}\emph{semantics}, which defines how programs behave when run.
Even when these elements seem obvious intuitively, we often find that there are surprisingly subtle choices to be made in defining syntax and semantics at the highest level of rigor.
Seemingly minor decisions can have big impacts on how smoothly our proofs go.
\item \textbf{Invariants.}
Nearly every theorem about a program is stated in terms of a \index{transition system}\emph{transition system}, with some set of states and a relation for stepping from one state to the next, moving forward in time.
Nearly every program proof also works by finding an \index{invariant}\emph{invariant} of a transition system, or a property that always holds of every state reachable from some starting state.
The concept of invariant is very close to being a direct reinterpretation of mathematical induction, that glue of every serious mathematical development, known and loved by all.
\item \index{abstraction}\textbf{Abstraction.}
Often a transition system is too complex to analyze directly.
Instead, we \emph{abstract} it with another transition system that is somehow more tractable, proving that the new system preserves all relevant properties of the original.
\item \index{modularity}\textbf{Modularity.}
Similarly, when a transition system is too complex, we often break it into separate \emph{modules} and use some well-behaved composition operators to reassemble them into the whole.
Often abstraction and modularity go together, as we decompose a system both \index{horizontal decomposition}\emph{horizontally} (i.e., with modularity), splitting it into more manageable parts, and \index{vertical decomposition}\emph{vertically} (i.e., with abstraction), simplifying parts in ways that preserve key properties.
We can even alternate between strategies, breaking a system into parts, abstracting one as a simpler part, further decomposing that part into pieces, and so on.
\end{itemize}
\newcommand{\encoding}[0]{\marginpar{\fbox{\textbf{Encoding}}}}
In the course of the book, we will never quite define any of these meta-techniques in complete formality.
Instead, we'll meet many examples of each, called out by eye-catching margin notes.
Generalizing from the examples should help the reader start developing an intuition for when to use each element and for the common design patterns that apply.
The core subject matter of the book is often grouped under traditional disciplinary headers like \index{semantics}\emph{semantics}, \index{programming-languages theory}\emph{programming-languages theory}, \index{formal methods}\emph{formal methods}, and \index{verification}\emph{verification}.
Often these different traditions have their own competing terminology for shared concepts.
We'll follow one particular set of unified terminology and notation, cherry-picked from the conventions of different communities.
There really is a huge amount of commonality across everything that we'll study, so we don't want to distract by constantly translating between notations.
It is quite important to be literate in the standard notational conventions, which are almost always implemented with \index{\LaTeX{}}\LaTeX{}, and we stick entirely to that kind of notation in this book.
However, we follow another, much less usual convention: while we give theorem and lemma statements, we rarely give their proofs.
The reason is that the author and many other researchers today feel that proofs on paper have outlived their usefulness.
Instead, the proofs are all found in the parallel world of the accompanying Coq source code.
That is, each chapter of this book has a corresponding Coq source file, distributed with the general book source code.
The Coq sources are heavily commented and may even, in many cases, be feasible to read without also reading the book chapters.
More importantly, the Coq sources aren't just meant to be \emph{read}.
They are meant to be \emph{executed}.
We suggest stepping through them interactively, seeing intermediate states of proofs as appropriate.
The book proper can be read without the Coq sources, to learn the standard background material of program proof; and the Coq sources can be read without the book proper, to learn a particular concrete realization of those ideas.
However, they go better together.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\chapter{Formalizing Program Syntax}\label{syntax}
\section{Concrete Syntax}
The definition of a program starts with the definition of a programming language, and the definition of a programming language starts with its \emph{syntax}\index{syntax}, which covers which sorts of phrases are basically well-formed.
In the next chapter, we turn to \emph{semantics}\index{semantics}, which, in the course of saying what programs \emph{mean}, may impose further validity conditions.
Turning to examples, let's start with \emph{concrete syntax}\index{concrete syntax}, which decrees which sequences of characters are acceptable.
For a simple language of arithmetic expressions, we might accept the following strings as valid.
$$\begin{array}{l}
3 \\
x \\
3 + x \\
y * (3 + x)
\end{array}$$
Plenty of other strings might be invalid, like these.
$$\begin{array}{l}
1 + + \; 2 \\
x \; y \; z
\end{array}$$
Rather than appeal to our intuition about grade-school arithmetic, we prefer to formalize concrete syntax with a \emph{grammar}\index{grammar}, following a style known as \emph{Backus-Naur Form (BNF)}\index{Backus-Naur Form}\index{BNF}.
We have a set of \emph{nonterminals}\index{nonterminal} (e.g., $e$ below), standing for sets of allowable strings.
Some are defined by appeal to existing sets, as below, when we define constants $n$ in terms of the well-known set $\mathbb N$\index{N@$\mathbb N$} of natural numbers\index{natural numbers} (nonnegative integers).
\encoding
$$\begin{array}{rrcl}
\textrm{Constants} & n &\in& \mathbb N \\
\textrm{Variables} & x &\in& \mathsf{Strings} \\
\textrm{Expressions} & e &::=& n \mid x \mid e + e \mid e \times e
\end{array}$$
To interpret the grammar in plain English: we assume sets of constants and variables, based on well-known sets of natural numbers and strings, respectively.
We then define expressions to include constants, variables, addition, and multiplication.
Crucially, the last two cases are specified \emph{recursively}: we show how to build bigger expressions out of smaller ones.
Incidentally, we're already seeing how many different formal notations creep into the discussion of formal program proofs.
All of this content is typeset in \LaTeX{}\index{\LaTeX{}}, and it may be helpful to consult the book sources, to see how it's all done.
Throughout the subject, one of our most crucial tools will be \emph{inductive definitions}\index{inductive definition}, explaining how to build up bigger sets from smaller ones.
The recursive nature of the grammar above is implicitly giving an inductive definition.
A more general notation for inductive definitions provides a series of \emph{inference rules}\index{inference rules} that define a set.
Formally, the set is defined to be \emph{the smallest one that satisfies all the rules}.
Each rule has \emph{premises}\index{premise} and a \emph{conclusion}\index{conclusion}.
We illustrate with four rules that together are equivalent to the BNF grammar above, for defining a set $\mathsf{Exp}$ of expressions.
\encoding
$$\infer{n \in \mathsf{Exp}}{
n \in \mathbb N
}
\quad \infer{x \in \mathsf{Exp}}{
x \in \mathsf{Strings}
}
\quad \infer{e_1 + e_2 \in \mathsf{Exp}}{
e_1 \in \mathsf{Exp}
& e_2 \in \mathsf{Exp}
}
\quad \infer{e_1 \times e_2 \in \mathsf{Exp}}{
e_1 \in \mathsf{Exp}
& e_2 \in \mathsf{Exp}
}$$
The general reading of an inference rule is: \textbf{if} all the facts above the horizontal line are true, \textbf{then} the fact below the line is true, too.
The rule implicitly needs to hold for \emph{all} values of the \emph{metavariables}\index{metavariable} (like $n$ and $e_1$) that appear within it; we can model them more explicitly with a sort of top-level universal quantification.
Newcomers to semantics often react negatively to seeing this style of definition, but very quickly it becomes apparent as a remarkably compact notation for expressing many concepts.
Think of it as a domain-specific programming language for mathematical definitions, an analogy that becomes quite concrete in the associated Coq code!
\section{Abstract Syntax}
After that brief interlude with concrete syntax, we now drop all formal treatment of it, for the rest of the book!
Instead, we concern ourselves with \emph{abstract syntax}\index{abstract syntax}, the real heart of language definitions.
Now programs are \emph{abstract syntax trees}\index{abstract syntax tree} (\emph{ASTs}\index{AST}), corresponding to inductive type definitions in Coq or algebraic datatype\index{algebraic datatype} definitions in Haskell\index{Haskell}.
Such types can be defined by enumerating their \emph{constructor}\index{constructor} functions with types.
\encoding
\begin{eqnarray*}
\mathsf{Const} &:& \mathbb{N} \to \mathsf{Exp} \\
\mathsf{Var} &:& \mathsf{Strings} \to \mathsf{Exp} \\
\mathsf{Plus} &:& \mathsf{Exp} \times \mathsf{Exp} \to \mathsf{Exp} \\
\mathsf{Times} &:& \mathsf{Exp} \times \mathsf{Exp} \to \mathsf{Exp}
\end{eqnarray*}
Note that the ``$\times$'' here is not the multiplication operator of concrete syntax, but rather the Cartesian-product operator\index{Cartesian product} of set theory, to indicate a type of pairs!
Such a list of constructors defines the set $\mathsf{Exp}$ to contain exactly those terms that can be built up with the constructors.
In inference-rule notation:
\encoding
$$\infer{\mathsf{Const}(n) \in \mathsf{Exp}}{
n \in \mathbb N
}
\quad \infer{\mathsf{Var}(x) \in \mathsf{Exp}}{
x \in \mathsf{Strings}
}
\quad \infer{\mathsf{Plus}(e_1, e_2) \in \mathsf{Exp}}{
e_1 \in \mathsf{Exp}
& e_2 \in \mathsf{Exp}
}
\quad \infer{\mathsf{Times}(e_1, e_2) \in \mathsf{Exp}}{
e_1 \in \mathsf{Exp}
& e_2 \in \mathsf{Exp}
}$$
Actually, semanticists get tired of writing such verbose descriptions, so proofs on paper tend to use exactly the sort of notation that we associated with concrete syntax.
The trick is mental desugaring of the concrete-syntax notation into abstract syntax!
We will generally not dwell on the particularities of that process.
Instead, we repeatedly illustrate it by example, using Coq code that starts with abstract syntax, accompanied by \LaTeX{}-based ``code'' in this book that applies concrete syntax freely.
Abstract syntax is handy for writing \emph{recursive definitions}\index{recursive definition} of functions.
Here is one in the clausal\index{clausal function definition} style of Haskell\index{Haskell}.
\begin{eqnarray*}
\mathsf{size}(\mathsf{Const}(n)) &=& 1 \\
\mathsf{size}(\mathsf{Var}(x)) &=& 1 \\
\mathsf{size}(\mathsf{Plus}(e_1, e_2)) &=& 1 + \mathsf{size}(e_1) + \mathsf{size}(e_2) \\
\mathsf{size}(\mathsf{Times}(e_1, e_2)) &=& 1 + \mathsf{size}(e_1) + \mathsf{size}(e_2)
\end{eqnarray*}
It is important that we include \emph{one clause per constructor of the inductive type}.
Otherwise, the function would not be \emph{total}\index{total function}.
We also need to be careful to ensure \emph{termination}\index{termination of recursive definitions}, by making recursive calls only on the arguments of the constructors.
This termination criterion, adopted by Coq, is called \emph{primitive recursion}\index{primitive recursion}.
\newcommand{\size}[1]{{\left \lvert #1 \right \rvert}}
It is also common to associate a recursive definition with a new notation.
For example, we might prefer to write $\size{e}$ for $\mathsf{size}(e)$, as follows.
\begin{eqnarray*}
\size{\mathsf{Const}(n)} &=& 1 \\
\size{\mathsf{Var}(x)} &=& 1 \\
\size{\mathsf{Plus}(e_1, e_2)} &=& 1 + \size{e_1} + \size{e_2} \\
\size{\mathsf{Times}(e_1, e_2)} &=& 1 + \size{e_1} + \size{e_2}
\end{eqnarray*}
\newcommand{\depth}[1]{{\left \lceil #1 \right \rceil}}
Let's continue to exercise our creative license and write $\depth{e}$ for the \emph{depth} of $e$, that is, the length of the longest downward path from the syntax-tree root to any leaf.
\begin{eqnarray*}
\depth{\mathsf{Const}(n)} &=& 1 \\
\depth{\mathsf{Var}(x)} &=& 1 \\
\depth{\mathsf{Plus}(e_1, e_2)} &=& 1 + \max(\depth{e_1}, \depth{e_2}) \\
\depth{\mathsf{Times}(e_1, e_2)} &=& 1 + \max(\depth{e_1}, \depth{e_2})
\end{eqnarray*}
\section{Structural Induction Principles}
The main reason to prefer abstract syntax is that, while strings of text \emph{seem} natural and simple to our human brains, they are really a lot of trouble to treat in complete formality.
Inductive trees are much nicer to manipulate.
Considering the name, it's probably not surprising that the main thing we want to do on them is \emph{induction}\index{induction}, an activity most familiar in the form of \emph{mathematical induction}\index{mathematical induction} over the natural numbers.
In this book, we will not dwell on many proofs about natural numbers, instead presenting the more general and powerful idea of \emph{structural induction}\index{structural induction} that subsumes mathematical induction in a formal sense, based on viewing the natural numbers as one simple inductively defined set.
There is a general recipe to go from an inductive definition to its associated induction principle.
When we define set $S$ inductively, we gain an induction principle for proving that some predicate $P$ holds for all elements of $S$.
To make this conclusion, we must discharge one proof obligation per rule of the inductive definition.
Recall our last rule-based definition above, for the abstract syntax of $\mathsf{Exp}$.
To derive an $\mathsf{Exp}$ structural induction principle, we produce a new set of rules, cloning each rule with two key modifications:
\begin{enumerate}
\item Replace each conclusion, of the form $E \in S$, with a conclusion $P(E)$. That is, the obligations involve \emph{showing} that $P$ holds of certain terms.
\item For each premise $E \in S$, add a companion premise $P(E)$. That is, the obligation allows \emph{assuming} that $P$ holds of certain terms. Each such assumption is called an \emph{inductive hypothesis}\index{inductive hypothesis} (\emph{IH}\index{IH}).
\end{enumerate}
That mechanical procedure derives the following four proof obligations, associated with an inductive proof that $\forall x \in \mathsf{Exp}. \; P(x)$.
$$\infer{P(\mathsf{Const}(n))}{
n \in \mathbb N
}
\quad \infer{P(\mathsf{Var}(x))}{
x \in \mathsf{Strings}
}$$
$$\quad \infer{P(\mathsf{Plus}(e_1, e_2))}{
e_1 \in \mathsf{Exp}
& P(e_1)
& e_2 \in \mathsf{Exp}
& P(e_2)
}
\quad \infer{P(\mathsf{Times}(e_1, e_2))}{
e_1 \in \mathsf{Exp}
& P(e_1)
& e_2 \in \mathsf{Exp}
& P(e_2)
}$$
In other words, to establish $\forall x \in \mathsf{Exp}. \; P(x)$, we need to prove that each of these inference rules is valid.
To see induction in action, we prove a theorem giving a sanity check on our two recursive definitions from earlier: depth can never exceed size.
\begin{theorem}
For all $e \in \mathsf{Exp}$, $\depth{e} \leq \size{e}$.
\end{theorem}
\begin{proof}
By induction on the structure of $e$.
\end{proof}
That sort of minimalist proof often surprises and frustrates newcomers.
Our position here is that proof checking is an activity fit for machines, not people, so we will leave out gory details, which are to be found in the accompanying Coq code, for this theorem and many others associated with this chapter.
Actually, even published proofs on paper tend to use ``proofs'' as brief as the one above, relying on the reader's experience to ``fill in the blanks''!
Unsurprisingly, fairly often there are logical errors in such arguments, leading to acceptance of bogus theorems.
For that reason, we stick to machine-checked proofs here, using the book chapters to introduce concepts, reasoning principles, and statements of key theorems and lemmas.
\section{\label{decidable}Decidable Theories}
We do, however, need to get all the proof details filled in somehow.
One of the most convenient cases is when a proof goal fits into some \emph{decidable theory}\index{decidable theory}.
We follow the sense from computability theory\index{computability theory}, where we consider some \emph{decision problem}\index{decision problem}, as a (usually infinite) set $F$ of formulas and some subset $T \subseteq F$ of \emph{true} formulas, possibly considering only those provable using some limited set of inference rules.
The decision problem is \emph{decidable} if and only if there exists some always-terminating program that, when passed some $f \in F$ as input, returns ``true'' if and only if $f \in T$.
Decidability of theories is handy because, whenever our goal belongs to the $F$ set of a decidable theory, we can discharge the goal automatically by running the deciding program that must exist.
One common decidable theory is \emph{linear arithmetic}\index{linear arithmetic}, whose $F$ set is generated by the following grammar as $\phi$.
$$\begin{array}{rrcl}
\textrm{Constants} & n &\in& \mathbb Z \\
\textrm{Variables} & x &\in& \mathsf{Strings} \\
\textrm{Terms} & e &::=& x \mid n \mid e + e \mid e - e \\
\textrm{Propositions} & \phi &::=& e = e \mid e < e \mid \neg \phi \mid \phi \land \phi
\end{array}$$
The arithmetic terms used here are \emph{linear} in the same sense as \emph{linear algebra}\index{linear algebra}: we never multiply together two terms containing variables.
Actually, multiplication is prohibited outright, but we allow multiplication by a constant as an abbreviation (logically speaking) for repeated addition.
Propositions are formed out of equality and less-than tests on terms, and we also have the Boolean negation (``not'') operator $\neg$ and conjunction (``and'') operator $\land$.
This set of propositional\index{propositional logic} operators is enough to encode the other usual inequality and propositional operators, so we allow them, too, as convenient shorthands.
Using decidable theories in a proof assistant like Coq, it is important to understand how a theory may apply to formulas that don't actually satisfy its grammar literally.
For instance, we may want to prove $f(x) - f(x) = 0$, for some fancy function $f$ well outside the grammar above.
However, we only need to introduce a new variable $y$, defined with the equation $y = f(x)$, to arrive at a new goal $y - y = 0$.
A linear-arithmetic procedure makes short work of this goal, and we may then derive the original goal by substituting back in for $y$.
Coq's tactics based on decidable theories do all that hard work for us.
\medskip
Another important decidable theory is of \emph{equality with uninterpreted functions}\index{theory of equality with uninterpreted functions}.
$$\begin{array}{rrcl}
\textrm{Variables} & x &\in& \mathsf{Strings} \\
\textrm{Functions} & f &\in& \mathsf{Strings} \\
\textrm{Terms} & e &::=& x \mid f(e, \ldots, e) \\
\textrm{Propositions} & \phi &::=& e = e \mid \neg \phi \mid \phi \land \phi
\end{array}$$
In this theory, we know nothing about the detailed properties of the variables or functions that we use.
Instead, we must reason solely from the basic properties of equality:
$$\infer[\mathsf{Reflexivity}]{e = e}{}
\quad \infer[\mathsf{Symmetry}]{e_1 = e_2}{
e_2 = e_1
}
\quad \infer[\mathsf{Transitivity}]{e_1 = e_2}{
e_1 = e_3
& e_3 = e_2
}$$
$$\infer[\mathsf{Congruence}]{f(e_1, \ldots, e_n) = f'(e'_1, \ldots, e'_n)}{
f = f'
& e_1 = e'_1
& \ldots
& e_n = e'_n
}$$
\medskip
As one more example of a decidable theory, consider the algebraic structure of \emph{semirings}\index{semirings}, which may profitably be remembered as ``types that act like natural numbers.''
A semiring is any set containing two elements notated 0 and 1, closed under two binary operators notated $+$ and $\times$.
The notations are suggestive, but in fact we have free reign in choosing the set, elements, and operators, so long as the following axioms\footnote{The equations are taken almost literally from \url{https://en.wikipedia.org/wiki/Semiring}.} are satisfied:
\begin{eqnarray*}
(a + b) + c &=& a + (b + c) \\
0 + a &=& a \\
a + 0 &=& a \\
a + b &=& b + a \\
(a \times b) \times c &=& a \times (b \times c) \\
1 \times a &=& a \\
a \times 1 &=& a \\
a \times (b + c) &=& (a \times b) + (a \times c) \\
(a + b) \times c &=& (a \times c) + (b \times c) \\
0 \times a &=& 0 \\
a \times 0 &=& 0
\end{eqnarray*}
The formal theory is then as follows, where we consider as ``true'' only those equalities that follow from the axioms.
$$\begin{array}{rrcl}
\textrm{Variables} & x &\in& \mathsf{Strings} \\
\textrm{Terms} & e &::=& 0 \mid 1 \mid x \mid e + e \mid e \times e \\
\textrm{Propositions} & \phi &::=& e = e
\end{array}$$
Note how the applicability of the semiring theory is incomparable to the applicability of the linear-arithmetic theory.
That is, while some goals are provable via either, some are provable only via the semiring theory and some provable only by linear arithmetic.
For instance, by the semiring theory, we can prove $x(y + z) = xy + xz$, while linear arithmetic can prove $x - x = 0$.
\section{Simplification and Rewriting}
While we leave most proof details to the accompanying Coq code, it does seem important to introduce two key principles that are often implicit in proofs on paper.
The first is \emph{algebraic simplification}\index{algebraic simplification}, where we apply the defining equations of a recursive definition to simplify a goal.
For example, recall that our definition of expression size included this clause.
\begin{eqnarray*}
\size{\mathsf{Plus}(e_1, e_2)} &=& 1 + \size{e_1} + \size{e_2}
\end{eqnarray*}
Now imagine that we are trying to prove this formula.
$$\size{\mathsf{Plus}(e, \mathsf{Const}(7))} = 2 + \size{e}$$
We may apply the defining equation to rewrite into a different formula, where we have essentially pushed the definition of $\size{\cdot}$ through the $\mathsf{Plus}$.
$$1 + \size{e} + \size{\mathsf{Const}(7)} = 2 + \size{e}$$
Another application of a different defining equation, this time for $\mathsf{Const}$, takes us to here.
$$1 + \size{e} + 1 = 2 + \size{e}$$
From here, the goal follows by linear arithmetic.
\medskip
Such a proof establishes a theorem $\forall e \in \mathsf{Exp}. \; \size{\mathsf{Plus}(e, \mathsf{Const}(7))} = 2 + \size{e}$.
We may use already-proved theorems via a more general \emph{rewriting}\index{rewriting} mechanism, applying whenever we know some quantified equality.
Within a new goal we are proving, we find some subterm that matches the lefthand side of that equality, after we choose the proper values of the quantified variables.
The process of finding those values automatically is called \emph{unification}\index{unification}.
Rewriting enables us to take the subterm we found and replace it with the righthand side of the equation.
As an example, assume that, for some $P$, we know $P(2 + \size{\mathsf{Var}(x)})$ and are trying to prove $P(\size{\mathsf{Plus}(\mathsf{Var}(x), \mathsf{Const}(7))})$.
We may use our earlier fact to rewrite the argument of $P$ in what we are trying to show, so that it now matches the argument from what we already know, at which point the proof is trivial to finish.
Here, unification found the assignment $e = \mathsf{Var}(x)$.
\medskip
\encoding
\label{metalanguage}
We close the chapter with an important note on terminology.
A formula like $P(\size{\mathsf{Plus}(\mathsf{Var}(x), \mathsf{Const}(7))})$ combines several levels of notation.
We consider that we are doing our mathematical reasoning in some \emph{metalanguage}\index{metalanguage}, which is often applicable to a wide variety of proof tasks.
We also happen to be applying it here to reason about some \emph{object language}\index{object language}, a programming language whose syntax is defined formally, here the language of arithmetic expressions.
We have $x$ as a variable of the metalanguage, while $\mathsf{Var}(x)$ is a variable expression of the object language.
It is difficult to use English to explain the distinction between the two in complete formality, but be on the lookout for places where formulas mix concepts of the metalanguage and object language!
The general patterns should soon become clear, as they are somehow already familiar to us from natural-language sentences like:
\begin{quote}
The wise man said, ``it is time to prove some theorems.''
\end{quote}
The quoted remark could just as well be in Spanish instead of English, in which case we have two languages nested in a nontrivial way.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\chapter{Data Abstraction}\label{adt}
All of the fully formal proofs in this book are worked out only in associated Coq code.
Therefore, before proceeding to more topics in program semantics and proof, it is important to develop some basic Coq competence.
Several heavily commented examples files are associated with this crucial point in the book.
We won't discuss details of Coq proving in this document, outside Appendix \ref{coqref}.
However, one of the possibilities shown off in the Coq code is worth drawing attention to, as a celebrated semantics idea in its own right, though we don't yet connect it to formalized syntax of programming languages.
That idea is \emph{data abstraction}\index{data abstraction}, one of the most central ideas in program structuring.
Let's consider the mathematical meaning of \emph{encapsulation}\index{encapsulation} in data structures.
\section{Algebraic Interfaces for Abstract Data Types}
\newcommand{\mt}[1]{\mathsf{#1}}
Consider the humble queue\index{queues}, a classic data structure that allows us to enqueue data elements and then dequeue them in the order received.
Perhaps surprisingly, there is already some complexity in efficient queue implementation.
So-called \emph{client code}\index{client code} that relies on queues shouldn't need to know about that complexity, though.
We should be able to formulate ``queue'' as an \emph{abstract data type}\index{abstract data type}, hiding implementation details.
In the setting of pure functional programming, as in Coq, here is our first cut at such a data type, as a set of types and operations, somewhat reminiscent of e.g. interfaces\index{interface} in Java\index{Java}.
Type $\mt{t}(\alpha)$ stands for queues holding data values in some type $\alpha$.
\begin{eqnarray*}
\mt{t}(\alpha) &:& \mt{Set} \\
\mt{empty} &:& \mt{t}(\alpha) \\
\mt{enqueue} &:& \mt{t}(\alpha) \times \alpha \to \mt{t}(\alpha) \\
\mt{dequeue} &:& \mt{t}(\alpha) \rightharpoonup \mt{t}(\alpha) \times \alpha
\end{eqnarray*}
A few notational conventions of note:
We declare that $\mt{t}(\alpha)$ is a type by assigning it the type $\mt{Set}$, which itself contains all the normal types of programming.
An empty queue exists for any $\alpha$, and enqueue and dequeue operations are also available for any $\alpha$.
The type of $\mt{dequeue}$ indicates function partiality\index{partial function} by the arrow $\rightharpoonup$: dequeuing yields no answer for an empty queue.
For partial function $f : A \rightharpoonup B$, we indicate lack of a mapping for $x \in A$ by writing $f(x) = \cdot$.
In normal programming, we stop at this level of detail in defining an abstract data type.
However, when we're after formal correctness proofs, we must enrich data types with \emph{specifications}\index{specifications} or ``specs.''\index{specs}
One prominent spec style is \emph{algebraic}\index{algebraic specifications}: write out a set of \emph{laws}, quantified equalities that use the operations of the data type.
For queues, here are two reasonable laws.
$$\begin{array}{l}
\mt{dequeue}(\mt{empty}) = \cdot \\
\forall q. \; \mt{dequeue}(q) = \cdot \Rightarrow q = \mt{empty} \\
\end{array}$$
Actually, the inference-rule notation from last chapter also makes algebraic laws more readable, so here is a restatement.
$$\infer{\mt{dequeue}(\mt{empty}) = \cdot}{}
\quad \infer{q = \mt{empty}}{\mt{dequeue}(q) = \cdot}$$
One more rule suffices to give a complete characterization of behavior, with the familiar math notation for piecewise functions\index{piecewise functions}.
$$\infer{\mt{dequeue}(\mt{enqueue}(q, x)) = \begin{cases}
(\mt{empty}, x), & \mt{dequeue}(q) = \cdot \\
(\mt{enqueue}(q', x), y), & \mt{dequeue}(q) = (q', y)
\end{cases}}{}$$
\newcommand{\concat}[2]{#1 \bowtie #2}
Now several implementations of this functionality are possible.
Here's one of the two ``obvious'' ones, where we enqueue to list fronts and dequeue from list backs.
We write $\mt{list}(\alpha)$ for the type of lists\index{lists} with data elements from $\alpha$, with $\concat{\ell_1}{\ell_2}$ for concatenation of lists $\ell_1$ and $\ell_2$, and with comma-separated lists inside square brackets for list literals.
\begin{eqnarray*}
\mt{t(\alpha)} &=& \mt{list}(\alpha) \\
\mt{empty} &=& [] \\
\mt{enqueue}(q, x) &=& \concat{[x]}{q} \\
\mt{dequeue}([]) &=& \cdot \\
\mt{dequeue}(\concat{[x]}{q}) &=& ([], x)\textrm{, when $\mt{dequeue}(q) = \cdot$.} \\
\mt{dequeue}(\concat{[x]}{q}) &=& (\concat{[x]}{q'}, y)\textrm{, when $\mt{dequeue}(q) = (q', y)$.}
\end{eqnarray*}
There is also a dual implementation where we enqueue to list backs and dequeue from list fronts.
\begin{eqnarray*}
\mt{t(\alpha)} &=& \mt{list}(\alpha) \\
\mt{empty} &=& [] \\
\mt{enqueue}(q, x) &=& \concat{q}{[x]} \\
\mt{dequeue}([]) &=& \cdot \\
\mt{dequeue}(\concat{[x]}{q}) &=& (q, x)
\end{eqnarray*}
Proofs of the algebraic laws, for both implementations, appear in the associated Coq code.
Both versions actually take quadratic time in practice, assuming concatenation takes time linear in the length of its first argument.
There is a famous, more clever implementation that achieves amortized\index{amortized time} constant time (linear time to run a whole sequence of operations), but we will need to expand our algebraic style to accommodate it.
\section{Algebraic Interfaces with Custom Equivalence Relations}
We find it useful to extend the base interface of queues with a new, mathematical ``operation'':
\begin{eqnarray*}
\mt{t}(\alpha) &:& \mt{Set} \\
\mt{empty} &:& \mt{t}(\alpha) \\
\mt{enqueue} &:& \mt{t}(\alpha) \times \alpha \to \mt{t}(\alpha) \\
\mt{dequeue} &:& \mt{t}(\alpha) \rightharpoonup \mt{t}(\alpha) \times \alpha \\
\mt{\approx} &:& \mathcal P(\mt{t}(\alpha) \times \mt{t}(\alpha))
\end{eqnarray*}
We use the ``powerset''\index{powerset} operation $\mathcal P$ to indicate that $\approx$ is a \emph{binary relation}\index{binary relation} over queues (of the same type).
Our intention is that $\approx$ be an \emph{equivalence relation}, as formalized by the following laws that we add.
$$\infer[\mathsf{Reflexivity}]{a \approx a}{}
\quad \infer[\mathsf{Symmetry}]{a \approx b}{b \approx a}
\quad \infer[\mathsf{Transitivity}]{a \approx c}{a \approx b & b \approx c}$$
Now we rewrite the original laws to use $\approx$ instead of equality.
We implicitly lift $\approx$ to apply to results of the partial function $\mt{dequeue}$: nonexistent results $\cdot$ are related, and existent results $(q_1, x_1)$ and $(q_2, x_2)$ are related iff $q_1 \approx q_2$ and $x_1 = x_2$.
$$\infer{\mt{dequeue}(\mt{empty}) = \cdot}{}
\quad \infer{q \approx \mt{empty}}{\mt{dequeue}(q) = \cdot}$$
$$\infer{\mt{dequeue}(\mt{enqueue}(q, x)) \approx \begin{cases}
(\mt{empty}, x), & \mt{dequeue}(q) = \cdot \\
(\mt{enqueue}(q', x), y), & \mt{dequeue}(q) = (q', y)
\end{cases}}{}$$
What's the payoff from this reformulation?
Well, first, it passes the sanity check that the two queue implementations from the last section comply, with $\approx$ instantiated as simple equality.
However, we may now also handle the classic \emph{two-stack queue}\index{two-stack queue}.
Here is its implementation, relying on list-reversal function $\mt{rev}$ (which takes linear time).
\begin{eqnarray*}
\mt{t(\alpha)} &=& \mt{list}(\alpha) \times \mt{list}(\alpha) \\
\mt{empty} &=& ([], []) \\
\mt{enqueue}((\ell_1, \ell_2), x) &=& (\concat{[x]}{\ell_1}, \ell_2) \\
\mt{dequeue}(([], [])) &=& \cdot \\
\mt{dequeue}((\ell_1, \concat{[x]}{\ell_2})) &=& ((\ell_1, \ell_2), x) \\
\mt{dequeue}((\ell_1, [])) &=& (([], q'_1), x)\textrm{, when $\mt{rev}(\ell_1) = \concat{[x]}{q'_1}$.}
\end{eqnarray*}
The basic trick is to encode a queue as a pair of lists $(\ell_1, \ell_2)$.
We try to enqueue into $\ell_1$ by adding elements to its front in constant time, and we try to dequeue from $\ell_2$ by removing elements from its front in constant time.
However, sometimes we run out of elements in $\ell_2$ and need to \emph{reverse} $\ell_1$ and transfer the result into $\ell_2$.
The suitable equivalence relation formalizes this plan.
\begin{eqnarray*}
\mt{rep}((\ell_1, \ell_2)) &=& \concat{\ell_1}{\mt{rev}(\ell_2)} \\
q_1 \approx q_2 &=& \mt{rep}(q_1) = \mt{rep}(q_2)
\end{eqnarray*}
We can prove both that this $\approx$ is an equivalence relation and that the other queue laws are satisfied.
As a result, client code (and its correctness proofs) can use this fancy code, effectively viewing it as a simple queue, with the two-stack nature hidden.
Why did we need to go through the trouble of introducing custom equivalence relations?
Consider the following two queues.
Are they equal?
(We write $\pi_1$ for the function that projects out the first element of a pair.)
\begin{eqnarray*}
\mt{enqueue}(\mt{empty}, 2) &\stackrel{?}{=}& \pi_1(\mt{dequeue}(\mt{enqueue}(\mt{enqueue}(\mt{empty}, 1), 2)))
\end{eqnarray*}
No, they aren't equal! The first expression reduces to $([2], [])$, while the second reduces to $([], [2])$.
This data structure is \emph{noncanonical}\index{noncanonical}, in the sense that the same logical value may have multiple physical representations.
The equivalence relation lets us indicate which physical representations are equivalent.
\section{Representation Functions}
That last choice of equivalence relations suggests another specification style, based on \emph{representation functions}\index{representation functions}.
We can force every queue to include a function to convert to a standard, canonical representation.
Real executable programs shouldn't generally call that function; it's most useful to us in phrasing the algebraic laws.
Perhaps surprisingly, the mere existence of any compatible function is enough to show correctness of a queue implementation, and the approach generalizes to essentially all other data structures cast as abstract data types.
Here is how we revise our type signature for queues.
\begin{eqnarray*}
\mt{t}(\alpha) &:& \mt{Set} \\
\mt{empty} &:& \mt{t}(\alpha) \\
\mt{enqueue} &:& \mt{t}(\alpha) \times \alpha \to \mt{t}(\alpha) \\
\mt{dequeue} &:& \mt{t}(\alpha) \rightharpoonup \mt{t}(\alpha) \times \alpha \\
\mt{rep} &:& \mt{t}(\alpha) \to \mt{list}(\alpha)
\end{eqnarray*}
And here are the revised axioms.
$$\infer{\mt{rep}(\mt{empty}) = []}{}
\quad \infer{\mt{rep}(\mt{enqueue}(q, x)) = \concat{[x]}{\mt{rep}(q)}}{}$$
$$\infer{\mt{dequeue}(q) = \cdot}{\mt{rep}(q) = []}
\quad \infer{\exists q'. \; \mt{dequeue}(q) = (q', x) \land \mt{rep}(q') = \ell}{\mt{rep}(q) = \concat{\ell}{[x]}}$$
Notice that this specification style can also be viewed as \emph{giving a reference implementation\index{reference implementations of data types} of the data type}, where $\mt{rep}$ shows how to convert back to the reference implementation at any point.
\section{Fixing Parameter Types for Abstract Data Types}
Here's another classic abstract data type: finite sets\index{finite sets}, where we write $\mathbb B$ for the set of Booleans.
\begin{eqnarray*}
\mt{t}(\alpha) &:& \mt{Set} \\
\mt{empty} &:& \mt{t}(\alpha) \\
\mt{add} &:& \mt{t}(\alpha) \times \alpha \to \mt{t}(\alpha) \\
\mt{member} &:& \mt{t}(\alpha) \times \alpha \to \mathbb B
\end{eqnarray*}
A few laws characterize expected behavior, with $\top$ and $\bot$ the respective elements ``true'' and ``false'' of $\mathbb B$.
$$\infer{\mt{member}(\mt{empty}, k) = \bot}{}
\quad \infer{\mt{member}(\mt{add}(s, k), k) = \top}{}
\quad \infer{\mt{member}(\mt{add}(s, k_1), k_2) = \mt{member}(s, k_2)}{k_1 \neq k_2}$$
There is a simple generic implementation of this data type with unsorted lists.
\begin{eqnarray*}
\mt{t} &=& \mt{list} \\
\mt{empty} &=& [] \\
\mt{add}(s, k) &=& \concat{[k]}{s} \\
\mt{member}([], k) &=& \bot \\
\mt{member}(\concat{[k']}{s}, k) &=& k = k' \lor \mt{member}(s, k)
\end{eqnarray*}
However, we can build specialized finite sets for particular element types and usage patterns.
For instance, assume we are working with sets of natural numbers, where we know that most sets contain consecutive numbers.
In those cases, it suffices to store just the lowest and highest elements of sets, and all the set operations run in constant time.
Assume a fallback implementation of finite sets, with type $t_0$ and operations $\mt{empty}_0$, $\mt{add}_0$, and $\mt{member}_0$.
We implement our optimized set type like so, assuming an operation $\mt{fromRange} : \mathbb N \times \mathbb N \to \mt{t}_0$ to turn a range into an ad-hoc set.
\begin{eqnarray*}
\mt{t} &=& \mt{Empty} \mid \mt{Range}(\mathbb N \times \mathbb N) \mid \mt{AdHoc}(\mt{t}_0) \\
\mt{empty} &=& \mt{Empty} \\
\mt{add}(\mt{Empty}, k) &=& \mt{Range}(k, k) \\
\mt{add}(\mt{Range}(n_1, n_2), k) &=& \mt{Range}(n_1, n_2)\textrm{, when $n_1 \leq k \leq n_2$} \\
\mt{add}(\mt{Range}(n_1, n_2), n_1-1) &=& \mt{Range}(n_1-1, n_2)\textrm{, when $n_1 \leq n_2$} \\
\mt{add}(\mt{Range}(n_1, n_2), n_2+1) &=& \mt{Range}(n_1, n_2+1)\textrm{, when $n_1 \leq n_2$} \\
\mt{add}(\mt{Range}(n_1, n_2), k) &=& \mt{AdHoc}(\mt{add}_0(\mt{fromRange}(n_1, n_2), k))\textrm{, otherwise} \\
\mt{add}(\mt{AdHoc}(s), k) &=& \mt{AdHoc}(\mt{add}_0(s, k)) \\
\mt{member}(\mt{Empty}, k) &=& \bot \\
\mt{member}(\mt{Range}(n_1, n_2), k) &=& n_1 \leq k \leq n_2 \\
\mt{member}(\mt{AdHoc}(s), k) &=& \mt{member}_0(s, k)
\end{eqnarray*}
This implementation can be proven to satisfy the finite-set spec, assuming that the baseline ad-hoc implementation does, too.
For workloads that only build sets of consecutive numbers, this implementation can be much faster than the generic list-based implementation, converting quadratic-time algorithms into linear-time.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\chapter{\label{interpreters}Semantics via Interpreters}
That's enough about what programs \emph{look like}.
Let's shift our attention to what programs \emph{mean}.
\section{Semantics for Arithmetic Expressions via Finite Maps}
\newcommand{\mempty}[0]{\bullet}
\newcommand{\msel}[2]{#1(#2)}
\newcommand{\mupd}[3]{#1[#2 \mapsto #3]}
To explain the meaning of one of Chapter \ref{syntax}'s arithmetic expressions, we need a way to indicate the value of each variable.
\encoding
A theory of \emph{finite maps}\index{finite map} is helpful here.
We apply the following notations throughout the book: \\
\begin{tabular}{rl}
$\mempty$ & empty map, with $\emptyset$ as its domain \\
$\msel{m}{k}$ & mapping of key $k$ in map $m$ \\
$\mupd{m}{k}{v}$ & extension of map $m$ to also map key $k$ to value $v$
\end{tabular} \\
As the name advertises, finite maps are functions with finite domains, where the domain may be expanded by each extension operation.
Two axioms explain the essential interactions of the basic operators.
$$\infer{\msel{\mupd{m}{k}{v}}{k} = v}{}
\quad
\infer{\msel{\mupd{m}{k_1}{v}}{k_2} = m(k_2)}{
k_1 \neq k_2
}$$
\newcommand{\denote}[1]{{\left \llbracket #1 \right \rrbracket}}
With these operators in hand, we can write a semantics for arithmetic expressions.
This is a recursive function that \emph{maps variable valuations to numbers}.
We write $\denote{e}$ for the meaning of $e$; this notation is often referred to as \emph{Oxford brackets}\index{Oxford brackets}.
Recall that we allow this kind of notation as syntactic sugar for arbitrary functions, even when giving the equations that define those functions.
We write $v$ for a valuation (finite map).
\encoding
\begin{eqnarray*}
\denote{n}v &=& n \\
\denote{x}v &=& v(x) \\
\denote{e_1 + e_2}v &=& \denote{e_1}v + \denote{e_2}v \\
\denote{e_1 \times e_2}v &=& \denote{e_1}v \times \denote{e_2}v
\end{eqnarray*}
Note how parts of the definition feel a little bit like cheating, as we just ``push notations inside the brackets.''
It's important to remember that plus \emph{inside} the brackets is syntax, while plus \emph{outside} the brackets is the normal addition of math!
\newcommand{\subst}[3]{[#3/#2]#1}
To test our semantics, we define a \emph{variable substitution} function\index{substitution}.
A substitution $\subst{e}{x}{e'}$ stands for the result of running through the syntax of $e$,
replacing every occurrence of variable $x$ with expression $e'$.
\begin{eqnarray*}
\subst{n}{x}{e} &=& n \\
\subst{x}{x}{e} &=& e \\
\subst{y}{x}{e} &=& y \textrm{, when $y \neq x$} \\
\subst{(e_1 + e_2)}{x}{e} &=& \subst{e_1}{x}{e} + \subst{e_2}{x}{e} \\
\subst{(e_1 \times e_2)}{x}{e} &=& \subst{e_1}{x}{e} \times \subst{e_2}{x}{e}
\end{eqnarray*}
We can prove a key compatibility property of these two recursive functions.
\begin{theorem}
For all $e$, $e'$, $x$, and $v$, $\denote{\subst{e}{x}{e'}}{v} = \denote{e}{(\mupd{v}{x}{\denote{e'}{v}})}$.
\end{theorem}
That is, in some sense, the operations of interpretation and substitution \emph{commute} with each other.
That intuition gives rise to the common notion of a \emph{commuting diagram}\index{commuting diagram}, like the one below for this particular example.
\[
\begin{tikzcd}
(e, v) \arrow{r}{\subst{\ldots}{x}{e'}} \arrow{d}{\mupd{\ldots}{x}{\denote{e'}v}} & (\subst{e}{x}{e'}, v) \arrow{d}{\denote{\ldots}} \\
(e, \mupd{v}{x}{\denote{e'}v}) \arrow{r}{\denote{\ldots}} & \denote{\subst{e}{x}{e'}}v
\end{tikzcd}
\]
We start at the top left, with a given expression $e$ and valuation $v$.
The diagram shows the equivalence of \emph{two different paths} to the bottom right.
Each individual arrow is labeled with some description of the transformation it performs, to get from the term at its source to the term at its destination.
The right-then-down path is based on substituting and then interpreting, while the down-then-right path is based on extending the valuation and then interpreting.
Since both paths wind up at the same spot, the diagram indicates an equality between the corresponding terms.
It's a matter of taste whether the theorem statement or the diagram expresses the property more clearly!
\section{A Stack Machine}
As an example of a very different language, consider a \emph{stack machine}\index{stack machine}, similar at some level to, for instance, the Forth\index{Forth} programming language, or to various postfix\index{postfix} calculators.
\encoding
$$\begin{array}{rrcl}
\textrm{Instructions} & i &::=& \mathsf{PushConst}(n) \mid \mathsf{PushVar}(x) \mid \mathsf{Add} \mid \mathsf{Multiply} \\
\textrm{Programs} & \overline{i} &::=& \cdot \mid i; \overline{i}
\end{array}$$
Though here we defined an explicit grammar for programs, which are just sequences of instructions, in general we'll use the notation $\overline{X}$ to stand for sequences of $X$'s, and the associated concrete syntax won't be so important.
We also freely use single instructions to stand for programs, writing just $i$ in place of $i; \cdot$.
\newcommand{\push}[2]{#1 \rhd #2}
Each instruction of this language transforms a \emph{stack}\index{stack}, a last-in-first-out list of numbers.
Rather than spend more words on it, here is an interpreter that makes everything precise.
Here and elsewhere, we overload the Oxford brackets $\denote{\ldots}$ shamelessly, where context makes clear which language or interpreter we are dealing with.
We write $s$ for stacks, and we write $\push{n}{s}$ for pushing number $n$ onto the top of stack $s$.
\encoding
\begin{eqnarray*}
\denote{\mathsf{PushConst}(n)}(v,s) &=& \push{n}{s} \\
\denote{\mathsf{PushVar}(x)}(v,s) &=& \push{\msel{v}{x}}{s} \\
\denote{\mathsf{Add}}(v,\push{n_2}{\push{n_1}{s}}) &=& \push{(n_1 + n_2)}{s} \\
\denote{\mathsf{Multiply}}(v,\push{n_2}{\push{n_1}{s}}) &=& \push{(n_1 \times n_2)}{s}
\end{eqnarray*}
The last two cases require the stack have at least a certain height.
Here we'll ignore what happens when the stack is too short, though it suffices, for our purposes, to add pretty much any default behavior for the missing cases.
We overload $\denote{\overline{i}}$ to refer to the \emph{composition} of the interpretations of the different instructions within $\overline{i}$, in order.
Next, we give our first example of what might be called a \emph{compiler}\index{compiler}, or a translation from one language to another.
Let's compile arithmetic expressions into stack programs, which then become easy to map onto the instructions of common assembly languages.
In that sense, with this translation, we make progress toward efficient implementation on commodity hardware.
\newcommand{\compile}[1]{{\left \lfloor #1 \right \rfloor}}
Throughout this book, we will use notation $\compile{\ldots}$ for compilation, where the floor-based notation suggests \emph{moving downward} to a lower abstraction level.
Here is the compiler that concerns us now, where we write $\concat{\overline{i_1}}{\overline{i_2}}$ for concatenation of two instruction sequences $\overline{i_1}$ and $\overline{i_2}$.
\encoding
\begin{eqnarray*}
\compile{n} &=& \mathsf{PushConst}(n) \\
\compile{x} &=& \mathsf{PushVar}(x) \\
\compile{e_1 + e_2} &=& \concat{\compile{e_1}}{\concat{\compile{e_2}}{\mathsf{Add}}} \\
\compile{e_1 \times e_2} &=& \concat{\compile{e_1}}{\concat{\compile{e_2}}{\mathsf{Multiply}}}
\end{eqnarray*}
The first two cases are straightforward: their compilations just push the obvious values onto the stack.
The binary operators are just slightly more tricky.
Each first evaluates its operands in order, where each operand leaves its final result on the stack.
With both of them in place, we run the instruction to pop them, combine them, and push the result back onto the stack.
The correctness theorem for compilation must refer to both of our interpreters.
From here on, we consider that all unaccounted-for variables in a theorem statement are quantified universally.
\begin{theorem}
$\denote{\compile{e}}(v, \cdot) = \denote{e}v$.
\end{theorem}
Here's a restatement as a commuting diagram.
\[
\begin{tikzcd}
e \arrow{r}{\compile{\ldots}} \arrow{dr}{\denote{\ldots}} & \compile{e} \arrow{d}{\denote{\ldots}} \\
& \denote{e}
\end{tikzcd}
\]
As usual, we leave proof details for the associated Coq code, but the key insight of the proof is to strengthen the induction hypothesis via a lemma.
\begin{lemma}
$\denote{\concat{\compile{e}}{\overline{i}}}(v, s) = \denote{\overline{i}}(v, \push{\denote{e}v}{s})$.
\end{lemma}
We strengthen the statement by considering both an arbitrary initial stack $s$ and a sequence of extra instructions $\overline{i}$ to be run after $e$.
\section{A Simple Higher-Level Imperative Language}
\newcommand{\repet}[2]{\mathsf{repeat} \; #1 \; \mathsf{do} \; #2 \; \mathsf{done}}
The interpreter approach to semantics is usually the most convenient one, when it applies.
Coq requires that all programs terminate, and that requirement is effectively also present in informal math, though it is seldom called out with the same terms.
Instead, with math, we worry about whether recursive systems of equations are well-founded, in appropriate senses.
From either perspective, extra encoding tricks are required to write a well-formed interpreter for a Turing-complete\index{Turing-completeness} language.
We will dodge those complexities for now by defining a simple imperative language with bounded loops, where termination is easy to prove.
We take the arithmetic expression language as a base.
\encoding
$$\begin{array}{rrcl}
\textrm{Command} & c &::=& \mathsf{skip} \mid x \leftarrow e \mid c; c \mid \repet{e}{c}
\end{array}$$
Now the implicit state, read and written by a command, is a variable valuation, as we used in the interpreter for expressions.
A $\mathsf{skip}$ command does nothing, while $x \leftarrow e$ extends the valuation to map $x$ to the value of expression $e$.
We have simple command sequencing $c_1; c_2$, in addition to the bounded loop $\repet{e}{c}$, which executes $c$ a number of times equal to the value of $e$.
\newcommand{\id}[0]{\mathsf{id}}
To give the semantics, we need a few commonplace notations that are worth reviewing.
We write $\id$ for the identity function\index{identity function}, where $\id(x) = x$; and we write $f \circ g$ for composition of functions\index{composition of functions} $f$ and $g$, where $(f \circ g)(x) = f(g(x))$.
We also have iterated self-composition\index{self-composition}, written like \emph{exponentiation} of functions\index{exponentiation of functions} $f^n$, defined as follows.
\begin{eqnarray*}
f^0 &=& \id \\
f^{n+1} &=& f^n \circ f
\end{eqnarray*}
From here, $\denote{\ldots}$ is easy to define yet again, as a transformer over variable valuations.
\encoding
\begin{eqnarray*}
\denote{\mathsf{skip}}v &=& v \\
\denote{x \leftarrow e}v &=& \mupd{v}{x}{\denote{e}v} \\
\denote{c_1; c_2}v &=& \denote{c_2}(\denote{c_1}v) \\
\denote{\repet{e}{c}}v &=& \denote{c}^{\denote{e}v}(v)
\end{eqnarray*}
To put this semantics through a workout, let's consider a simple \emph{optimization}\index{optimization}, a transformation whose input and output programs are in the same language.
There's an additional, fuzzier criterion for an optimization, which is that it should improve the program somehow, usually in terms of running time, memory usage, etc.
The optimization we choose here may be a bit dubious in that respect, though it is related to an optimization found in every serious C\index{C programming language} compiler.
In particular, let's tackle \emph{loop unrolling}\index{loop unrolling}.
When the iteration count of a loop is a constant $n$, we can replace the loop with $n$ sequenced copies of its body.
C compilers need to work harder to find the iteration count of a loop, but luckily our language includes loops with very explicit iteration counts!
To define the transformation, we'll want a recursive function and notation for sequencing of $n$ copies of a command $c$, written $^nc$.
\begin{eqnarray*}
^0c &=& \mathsf{skip} \\
^{n+1}c &=& c; {^nc}
\end{eqnarray*}
\newcommand{\opt}[1]{{\left | #1 \right |}}
Now the optimization itself is easy to define.
We'll write $\opt{\ldots}$ for this and other optimizations, which move neither down nor up a tower of program abstraction levels.
\encoding
\begin{eqnarray*}
\opt{\mathsf{skip}} &=& \mathsf{skip} \\
\opt{x \leftarrow e} &=& x \leftarrow e \\
\opt{c_1; c_2} &=& \opt{c_1}; \opt{c_2} \\
\opt{\repet{n}{c}} &=& ^n\opt{c} \\
\opt{\repet{e}{c}} &=& \repet{e}{\opt{c}}
\end{eqnarray*}
Note that, when multiple defining equations apply to some function input, by convention we apply the \emph{earliest} equation that matches.
Let's prove that this optimization preserves program behavior; that is, we prove that it is \emph{semantics-preserving}\index{semantics preservation}.
\begin{theorem}\label{unroll}
$\denote{\opt{c}}v = \denote{c}v$.
\end{theorem}
It all looks so straightforward from that statement, doesn't it?
Indeed, there actually isn't so much work to do to prove this theorem.
We can also present it as a commuting diagram much like the prior one.
\[
\begin{tikzcd}
c \arrow{r}{\opt{\ldots}} \arrow{dr}{\denote{\ldots}} & \opt{c} \arrow{d}{\denote{\ldots}} \\
& \denote{c}
\end{tikzcd}
\]
The statement of Theorem \ref{unroll} happens to be already in the right form to do induction directly, but we need a helper lemma, capturing the interaction of $^nc$ and the semantics.
\begin{lemma}
$\denote{^nc} = \denote{c}^n$.
\end{lemma}
Let us end the chapter with the commuting-diagram version of the lemma statement.
\[
\begin{tikzcd}
c \arrow{r}{^n\ldots} \arrow{d}{\denote{\ldots}} & ^nc \arrow{d}{\denote{\ldots}} \\
\denote{c} \arrow{r}{\ldots^n} & \denote{c}^n
\end{tikzcd}
\]
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\chapter{Inductive Relations and Rule Induction}\label{rule_induction}
We should pause here to consider another crucial mathematical tool that is not in common use outside the study of semantics but which will be essential for almost all language semantics we define from here on.
That tool is similar to the inductive \emph{set} or \emph{type} definitions we met in Chapter \ref{syntax}.
However, now we define \emph{relations}\index{inductive relations} (and \emph{predicates}\index{inductive predicates}, the colloquial name for single-argument relations) inductively.
Let us take some time to work through simple examples before moving on to cases more relevant to semantics.
\section{Finite Sets as Inductive Predicates}
\newcommand{\favs}[1]{\mathsf{favorites}(#1)}
Any finite set is easy to define as a predicate, with a set of inference rules that include no premises.
For instance, say my favorite numbers are 17, 23, and 42.
We can define a predicate $\mathsf{favorites}$ as follows.
$$\infer{\favs{17}}{}
\quad \infer{\favs{23}}{}
\quad \infer{\favs{42}}{}$$
As we defined inductive sets as the \emph{smallest} sets satisfying given inference rules, we now define inductive predicates as the \emph{least} predicates satisfying the rules.
The rules given here require acceptance of 17, 23, and 42 and no more, so those are exactly the values accepted by the predicate.
Any inductive predicate definition has an associated induction principle\index{inductive principle}, which we can derive much as we derived induction principles in Chapter \ref{syntax}.
Specifically, when we defined $P$ inductively and want to conclude $Q$ from it, we want to prove $\forall x. \; P(x) \Rightarrow Q(x)$.
We transform each rule into one obligation within the induction, by replacing $P$ with $Q$ in the conclusion, in addition to taking each premise $P(e)$ and pairing it with a new premise $Q(e)$ (an \emph{induction hypothesis}\index{induction hypothesis}).
Our example of $\mathsf{favorites}$ is a degenerate inductive definition whose principle requires no induction hypotheses. Thus, to prove $\forall x. \; \favs{x} \Rightarrow Q(x)$, we must establish the following.
$$\infer{Q(17)}{}
\quad \infer{Q(23)}{}
\quad \infer{Q(42)}{}$$
That is, to prove that a predicate holds of all elements of a finite set, it suffices to check the predicate for each element.
In general, induction on proofs of relations is called \emph{rule induction}\index{rule induction}.
A simple example:
\begin{theorem}
All of my favorite numbers are below 50, i.e. $\forall x. \; \favs{x} \Rightarrow x < 50$.
\end{theorem}
\begin{proof}
By induction on the proof of $\favs{x}$, i.e. with $Q(x) = x < 50$.
\end{proof}
Note how it is quite natural to see rule induction as induction on proof trees, as if they were just any other tree data structure!
Indeed, data and proofs are unified in Coq's mathematical foundation.
\section{Transitive Closure of Relations}
Let $R$ be some binary relation. We define its \emph{transitive closure}\index{transitive closure} $R^+$ by:
$$\infer{x \; R^+ \; y}{
x \; R \; y
}
\quad \infer{x \; R^+ z}{
x \; R^+ \; y
& y \; R^+ \; z
}$$
That is, $R^+$ is the \emph{least} relation satisfying these rules.
It should accept argument pairs only if the rules force them to be accepted.