What you could have learned in this class
Congratulations on having mastered this course. From Swinburn’s “Picture Logic”, first published in 1875.
Lectures
Evaluator again, and project notes
Project is due† the 21st, presentations also due† the 21st.
Types, and type systems.
Preliminaries
Implementing a language evaluator
Preliminaries
Write you a Kanren for great good!
Implementing our own Kanren
Our first Kanren
Logic Programming in miniKanren
A Whole New World
Transition
SAT, DIMACS, DPLL
Every one of your groups should be meeting w/1 of the designated staff members!!!
SAT v. SMT v. CP “Rat’s eye view”
Project Submissions
Accs, ADTs, New Topics
Recap Accumulator Reasoning
Reasoning with accumulators
Introduction 1: For and against accumulators
Induction like a Pro
Induction like a pro: not so hard!
The trinity
The data-function-induction (DFI)trinity:
Proving Properties w/ Induction
Big in-class examples:
Induction Schemes
Induction: more complicated in ACL2
More Halting, More Undecidability Results
Continuation
Halting Problem; Undecidability Results
Exam: How’d you all go?
Common Recursion Schemes
Recap yesterday, do again.
Measure functions 101
Let’s check on our reading! How’s this going?
Definition and Termination
Let’s check on our reading! How’s this going?
More Pen-and-paper proofs
We do more of these proofs in class, using the proof checking tool, as well as just working in an editor and uploading.
Pen-and-paper proofs
How to Prove it:
Equivalences of programs, extra axioms, (derived) context viz. theorems
Where we last left.
The Proving Ground
Today’s topics
Limitations of Boolean Algebra
A first example: 536 + 487 = 586 + 437
Decision problems, Complexity; P ?= NP; Reductions, Boolean logic in ACL2s; normal forms; set theory;
Decision Problems
Substitutions, case-match, reductions
Valid formulae =_df tautologies
Property-based testing, and the utility.
Discussion Property-based testing: a kind of testing you likely haven’t seen before PBT vs. other kinds of testing How to do it, how to think about t...
(Remainder) of the Dirty Dozen
More bits of syntax
Starting ACL2 in Earnest
PollEverywhere Q
A first dose of ACL2
Topics
About the course
Headlines