Fixed a few typos

README.md

@@ -5,13 +5,13 @@ Abstract Mathematics as Semantics Domains for Complex Computations
 TL;DR
 -----
 
-This repo supports the development and delivery of notes for an early graduate course in computer science at the University Virginia. This course is intended to take early graduate students from a point of having no knowledge of formal reasoning through basics of logic and proof using the Lean proof assistant, and into the realm of formalized mathematics. The thesis underlying this work is that CS can now benefit greatly by taking advantage of rapid advances in the formalization of abstract and advanced mathemtics to provide deep semantic foundations for critical application areas, including robotics, cyberphysical systems more generally, and AI. This work is thus meant to start to close a significant gap between mathematics and computer science research to improve software design, productivity, and dependability, but *not* on a path to formal verification. The evolving notes are [here](https://www.computingfoundations.org). We solicit interest and are open to research community engagement. Feel free to reach out: [email protected].
+This repo supports the development and delivery of notes for an early graduate course in computer science at the University Virginia. This course is intended to take early graduate students from a point of having no knowledge of formal reasoning through basics of logic and proof using the Lean proof assistant, and into the realm of formalized mathematics. The thesis underlying this work is that CS can now benefit greatly by taking advantage of rapid advances in the formalization of abstract and advanced mathematics to provide deep semantic foundations for critical application areas, including robotics, cyberphysical systems more generally, and AI. This work is thus meant to start to close a significant gap between mathematics and computer science research to improve software design, productivity, and dependability, but *not* on a path to formal verification. The evolving notes are [here](https://www.computingfoundations.org). We solicit interest and are open to research community engagement. Feel free to reach out: [email protected].
 
 
 Motivation
 ----------
 
-For millenia, to the present day, abstract mathematics
+For millennia, to the present day, abstract mathematics
 has been an analog, paper-and-pencil, pursuit.  For most
 of that time, there was nothing but paper and pencil, of
 course and that's what it mostly remains.
@@ -31,7 +31,7 @@ This work has been funded in part by the National Science Foundation as part of
 This Repository
 ---------------
 
-This repository is the course development and delivery platform for CS6501, Special Topics in Software Engineering, Abstract Mathemtical Foundations, being taught in the Spring of 2023.
+This repository is the course development and delivery platform for CS6501, Special Topics in Software Engineering, Abstract Mathematical Foundations, being taught in the Spring of 2023.
 
 The rest of this document is entirely for my own use. It presents instructions, mostly for myself, on how to use it.
 
@@ -71,7 +71,7 @@ Manual Processes
 ----------------
 
 The following files are maintained by hand:
-- The file `source/index.rst` should have an entry for each chapter/dicrectory.
+- The file `source/index.rst` should have an entry for each chapter/directory.
 - For each chapter/directory, there should be a `.rst` file in `source`. It should include
   - each of the sections.
   - For each section, there should be a `.lean` file in the appropriate place in `lean_source`.
@@ -100,7 +100,7 @@ From the top-level directory of the cloned repo do this:
 - deploy.sh (TODO: needs to be fixed)
 - instead follow instructions in UPLOAD.md
 
-The script `deploy.sh` KS: FIX deploy everythings (textbook
+The script `deploy.sh` KS: FIX deploy everything (textbook
 and user version of the example and solution files) to an
 arbitrary repository, set up to use the `gh-pages` branch
 to display the html. Note: Avigad uses the following here:

lean_source/A_00_Introduction/A_01_abstract_language_and_thought.lean

@@ -54,8 +54,8 @@ Costs of Concreteness
 
 This ubiquitous approach to programming physical computations
 is problematical in multiple dimensions. First, as mentioned,
-it substitues concrete representations for abstract, adding
-inessesntial complexity to models and computations. Second,
+it substitutes concrete representations for abstract, adding
+inessential complexity to models and computations. Second,
 it generally strips away crucial mathematical properties of
 the abstract representations of objects of interest, making
 it impossible to check programs for consistency with such
@@ -111,7 +111,7 @@ exercise, making it, hard even impossible, to connect code
 to such mathematics. 
 
 Now, with rapidly developing work by a still small set of
-ressearchers in mathematics, the complete formalization and
+researchers in mathematics, the complete formalization and
 mechanization of advanced abstract mathematics is becoming
 a reality. As and example Massot and his colleagues in 2022
 managed to formalize not only a statement, but a proof, of 
@@ -133,7 +133,7 @@ The insight driving this class is that this kind of work
 from the  mathematics community is now making it possible 
 to develop *computable abstract mathematics* for purposes
 of software engineering. Promising application domains for
-such work clearly include divere cyber-physical systems and
+such work clearly include diverse cyber-physical systems and
 might be relevant to deep learning as well, with its basic
 assumption that real-world data have geometric properties, 
 such as lying on high-dimensional manifolds. 
@@ -160,7 +160,7 @@ TEXT. -/
 /-
 The idea of raising the abstraction level of programming
 languages and programs is ages old. But these increases
-in abstration are usually incremental and ad hoc, moving
+in abstraction are usually incremental and ad hoc, moving
 in small steps from the language of the machine closer to
 but never really approaching the richness of the abstract
 mathematics of the domain, using its concepts, notations,
@@ -209,7 +209,7 @@ manifolds.
 
 Linking such abstract mathematics to code has always been
 a manual processes. Now, however, with the automation of
-abstract mathemtics by parts of the mathematics community
+abstract mathematics by parts of the mathematics community
 using constructive logic proof assistants and type theory,
 that has become possible. This course will teach you the
 basic concepts that you will need to start to make such

lean_source/A_00_Introduction/A_02_this_class.lean

@@ -27,14 +27,14 @@ Here, the adjective, abstract, means *being coordinate-free*.
 For the opposite of *abstract*, we'll use *parametric*. The idea 
 is that a mathematical object, such as a vector, can be understood
 simply as such, with no reference to coordinates; or that same abstract
-vector can be represented concretely/parametrically as a struture of
+vector can be represented concretely/parametrically as a structure of
 parameter values expressed relative to some given frame of reference.
 
 Why *abstract* mathematics?
 ---------------------------
 
 A premise of this class is that domain experts (e.g., in the
-physics of terrestrial robotics, or of elemenary particles) speak,
+physics of terrestrial robotics, or of elementary particles) speak,
 model, analyze, and understand the operation of systems in the 
 abstract mathematical language of the domain, and very often not
 in terms of ultimately arbitrarily selected frames of reference . 
@@ -73,7 +73,7 @@ of the domain and with very little custom coding needed also to
 have corresponding verified implementations, even if only used as
 test oracles for production code.  
 
-This is the of abstract specifictions from which concrete 
+This is the of abstract specifications from which concrete 
 implementations are derived. I will not say refined because 
 in practice most derivations are not refinements but rather
 toyish models of semantically rich and complex computations
@@ -84,7 +84,7 @@ This class
 
 The first major part of this class will teach you the fundamentals
 of programming and reasoning in Lean 3. We will mainly use Lean 3, 
-nothwithstaning that Lean 4 is garnering real attention and effort.
+notwithstanding that Lean 4 is garnering real attention and effort.
 Student might wish to explore Lean 4 as an optional class activity.
 
 The second part of the class will focus on how to formalized abstract

lean_source/A_01_Propositional_Logic/A_01_formal_languages.lean

@@ -8,7 +8,7 @@ As a warmup, and to put some basic
 concepts into play, we'll begin by specifying the syntax 
 and semantics of a simple formal language: the language of
 strings of balanced parentheses. Before we do that, we'll
-better explain wht it all menas. So let's get started.
+better explain what it all means. So let's get started.
 
 Formal languages
 ----------------
@@ -34,7 +34,7 @@ natural number, *n*, there is a such a string with nesting
 depth *n*. 
 
 We clearly can't specify the set of strings by exhaustively
-enumerating them expliciitly. There are too many for that. 
+enumerating them explicitly. There are too many for that. 
 Rather, we need a concise, precise, finite, and manageable 
 way to specify the set of all such strings. We will do that
 by defining a small set of *basic rules for building* strings 
@@ -66,13 +66,13 @@ Paper & Pencil Syntax
 What we've basically done in this case is to specify the set of
 strings in our language with a *grammar* or *syntax definition*.
 Such grammars are often expressed, especially in the programming
-worls, using so-called *Backus-Naur Form (BNF)*. 
+world, using so-called *Backus-Naur Form (BNF)*. 
 
 Backus first used BNF notation to define the syntax of the Algol 
 60 programming language. BNF is basically a notation for specifying
 what the linguist, Noam Chomsky, called *context-free grammars*. 
 
-Here's a grammer in BNF for our language of balanced parentheses. 
+Here's a grammar in BNF for our language of balanced parentheses. 
 We can say that the BNF grammar defines the syntax, or permitted
 forms, of strings in our language. Be sure you see how this grammar
 allow larger expressions to be build from smaller ones of the same 
@@ -232,7 +232,7 @@ data types in Lean that you should now understand. First, they
 are *disjoint*. Different constructors *never* produce the same
 value. Second, they are *injective*. A constructor applied to
 different argument values will always produce different terms.
-Finally, they are complete. The langauge they define contains 
+Finally, they are complete. The language they define contains 
 *all* of the strings constructible by any finite number of
 applications of the defined constructors *and no other terms*. 
 For example, our *bal* language doesn't contain any *error* or

lean_source/A_01_Propositional_Logic/A_02_subset_prop_logic.lean

@@ -7,7 +7,7 @@ Simplified Propositional Logic
 
 Our next step toward formalizing abstract mathematics for software 
 engineering, we will specify the syntax and semantics of a simple 
-but important mathatical language, namely *propositional logic*.
+but important mathematical language, namely *propositional logic*.
 
 Propositional logic is isomorphic to (essentially the same thing 
 as) Boolean algebra. You already know about Boolean algebra from 

lean_source/A_01_Propositional_Logic/A_06_prop_logic_algebraic_axioms.lean

@@ -114,7 +114,7 @@ Another Notation
 As we've seen, mathematical theories are often
 augmented with concrete syntactic notations that 
 make it easier for people to read and write such
-mathemantics. We would typically write *3 + 4*,
+mathematics. We would typically write *3 + 4*,
 for example, in lieu of *nat.add 3 4*. For that
 matter, we write *3* for (succ(succ(succ zero))).
 Good notations are important.
@@ -197,7 +197,7 @@ Specialization of Generalizations
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 Observe: We can *apply* these theorems
-to particular objects to specalize the
+to particular objects to specialize the
 generalized statement to the particular
 objects.
 TEXT. -/
@@ -358,7 +358,7 @@ developed into a mathematical library component
 with an emphasis on good design. 
 
 What does that even mean? Good with respect to
-what criteria, deciderata, needs, objectives?
+what criteria, desiderata, needs, objectives?
 
 - data type definitions
 - operation definitions

lean_source/A_01_Propositional_Logic/A_07_prop_logic_inference_rules.lean

@@ -6,7 +6,7 @@ Inference Rules
 
 In this chapter we will present another approach 
 to validating our model of propositional logic: by 
-verifying that it satisifies the *inference rules* 
+verifying that it satisfies the *inference rules* 
 of this logic.
 
 An inference rule is basically a function that takes 

lean_source/A_01_Propositional_Logic/A_08_prop_logic_inference_rules_validation.lean

@@ -17,7 +17,7 @@ The first section of this chapter refactors the partial
 solution we developed in class, grouping definitions of
 the propositions that represent them, and separately a
 proof that each rule expresses in our model is valid.
-These sections also afford opportunities to intruduce
+These sections also afford opportunities to introduce
 a few more concepts in type theory and Lean.
 
 To begin we import some definitions and declare a set
@@ -177,7 +177,7 @@ Identify any rules that fail to be provably valid in the
 presence of the bug we'd injected in bimp. Which rule
 validation proofs break when you re-activate that bug? 
 
-To get you started, the following proof shosws that the
+To get you started, the following proof shows that the
 false elimination inference rule is valid in our logic.
 TEXT. -/
 
@@ -196,12 +196,12 @@ theorem false_elim : false_elim_rule X i :=
 begin
 unfold false_elim_rule pEval,
 assume h,
-cases h,  -- contradiction, can't hppen, no cases!
+cases h,  -- contradiction, can't happen, no cases!
           -- Lean determines tt = ff is impossible
 end
 
 
--- Define the remaning propositions and proofs here: 
+-- Define the remaining propositions and proofs here: 
 
 
 end rule_validation -- section

lean_source/A_01_Propositional_Logic/A_99_06_prop_logic_validation.old.lean

@@ -51,7 +51,7 @@ Algebraic Properties
 First, a propositional logic can be understood as an algebra over
 Boolean-valued terms, variables, and constants. Constants and variables
 are are terms, but terms can also be constructed from smaller terms using
-connectives: ∧, ∨, ¬, and so on. The axioms of propopsitiona logic impose
+connectives: ∧, ∨, ¬, and so on. The axioms of propositional logic impose
 constraints on how these operations behave, on their own and combined. 
 
 The constraints are algebraic, just as the axioms are algebraic that
@@ -91,7 +91,7 @@ and_commutes  -- proof from last chapter
 As we've seen, mathematical theories are often
 augmented with concrete syntax / notations that 
 make it practical for people to read and write 
-such mathemantics. 
+such mathematics. 
 
 A standard notation for a "meaning-of-expression" 
 operator is a pair of *denotation* or *Scoot* 
@@ -131,7 +131,7 @@ to be the same as function arguments.
 
 /-
 Observe: We can *apply* these theorems
-to particular objects to specalize the
+to particular objects to specialize the
 generalized statement to the particular
 objects.
 -/

lean_source/A_01_Propositional_Logic/A_99_ignore_this.lean

@@ -45,7 +45,7 @@ which generate all and only the well formed formulae strings of  in the language
 
 
 The strings are called the *well formed formulae* (or *wffs, 
-terms, or expressions*) of the language. The sematics of a
+terms, or expressions*) of the language. The semantics of a
 formal language is as assignment of meanings to expressions.
 
 It is possible, in general, that only some expressions in a

lean_source/A_02_Constructive_Logic/A_02_Propositions_as_Types.lean

@@ -17,7 +17,7 @@ propositional logic to provide a way to reason about
 the truth of given propositions. In this chapter, we
 will represent propositions as types of a special kind,
 instead, and proofs as values of these types. We will
-then adopt exacty the same inference rules we saw in
+then adopt exactly the same inference rules we saw in
 the last chapter, but generalized to this far more
 expressive logic.   
 
@@ -187,7 +187,7 @@ elements values of type Type 0 is itself a value of type Type 1.
 
 As a final comment, Lean allows one to generalize over these
 type universes. To do so you declare one or more *universe 
-variable* which you can then use in decaring types. Lean can
+variable* which you can then use in declaring types. Lean can
 also infer universe levels.
 TEXT. -/
 

lean_source/A_02_Constructive_Logic/A_04_Inference_Rules.lean

@@ -11,7 +11,7 @@ library of mathematical definitions.
 Your next major task is to know and understand these
 inference rules. For each connective, learn its related
 introduction (proof constructing) and elimination (proof
-consuming) rules. Grasp the sense of each rule clerly.
+consuming) rules. Grasp the sense of each rule clearly.
 And learn how to to compose them, e.g., in proof scripts, 
 to produce proofs of more complex propositions. 
 
@@ -510,7 +510,7 @@ TEXT. -/
 
 
 -- QUOTE:
--- A proof of 0 = 0 by contradition 
+-- A proof of 0 = 0 by contradiction 
 example : 0 = 0 :=
 begin
 by_contradiction, -- applies ¬¬P → P
@@ -559,7 +559,7 @@ that for any given proposition, P, there is a proof of P ∨ ¬P.
 
 This axiom then enables proof by contradiction. That's an easy
 proof. We need to prove that if *P ∨ ¬ P* then *¬¬P → P*. The
-proof is by case analysis on an assumped proof of *P ∨ ¬ P*.
+proof is by case analysis on an assumed proof of *P ∨ ¬ P*.
 In the first case, we assume a proof of P, so the implication
 is true trivially. In the case where we have a proof of ¬P, we
 have a contradiction between ¬P and ¬¬P, and so this case can't
@@ -746,7 +746,7 @@ In this section you've encountered analogs in
 higher-order logic of the reasoning principles 
 that you saw (in weaker forms) in propositional
 logic, but now as rules for and expressed in a 
-higher-order predicae logic itself embedded in
+higher-order predicate logic itself embedded in
 the higher-order logic of Lean. 
 
 Just as we ourselves specified an embedding

lean_source/A_02_Constructive_Logic/A_99_ingore_this.lean

@@ -18,7 +18,7 @@ You already have a reasonable intuitive grasp of the
 meanings of the connectives in propositional logic.
 Predicate logic uses the same connectives to compose
 given propositions into new ones, with the same basic
-meanings. For example, we still have one introdcution
+meanings. For example, we still have one introduction
 (construction) rule for ∧ and two elimination rules. 
 
 Key differences, already discussed in class, are that
@@ -30,7 +30,7 @@ terms of proof/type judgments rather than in terms of
 For example, instead of *P* and *Q* being of type
 *prop_expr*, we now have them being of type *Prop*.
 They are types that encode logical propositions. And
-whereas the *and_intro* rule in proposital logic is
+whereas the *and_intro* rule in propositional logic is
 (⟦P⟧ i = tt) → (⟦Q⟧ i = tt) → (⟦P ∧ Q⟧ i = tt), now it
 is *∀ (P Q : Prop), P → Q → and P Q*. ∧ is notation
 for *and.* 

lean_source/A_03_Recursive_Types/A_02_natural_numbers.lean

@@ -131,7 +131,7 @@ def plus : nat → nat → nat
 #eval plus 3 4
 
 -- multiplication adds the second argument
--- to itself the first argumen number of times
+-- to itself the first argument number of times
 def times : nat → nat → nat
 | 0 m := 0
 | (n'+1) m := plus m (times n' m)
@@ -140,7 +140,7 @@ def times : nat → nat → nat
 #eval times 1 20
 
 
--- substraction illustrates case analysis on 
+-- subtraction illustrates case analysis on 
 -- multiple (here two) arguments at once
 def subtract :  nat → nat → nat
 | 0 _ := 0

lean_source/A_03_Recursive_Types/A_03_polymorphic_lists.lean

@@ -126,7 +126,7 @@ is empty.
 When we defined pred, above, we defined pred of zero to be 
 zero (rather than to be undefined). Doing that makes the 
 function total and easily represented as a function (lambda 
-abstractraction) in Lean. However, in a different application
+abstraction) in Lean. However, in a different application
 we really might want to define pred 0 to be undefined, not 0.
 
 A similar set of issues arises when we consider head and
@@ -183,7 +183,7 @@ fully to an empty list, in which case (3) no real result has
 to be specified to "prove the return type" because such a case 
 can't happen. It would be a contradiction if it did, and so it
 can be dismissed as an impossibility. Magic: It *is* a total 
-function, but it can never be fully appied to an empty list
+function, but it can never be fully applied to an empty list
 because a required proof argument, for *that* list, can never
 be given; so one can dismiss this case by false elimination,
 without having to give an actual proof of the conclusion.