CSC 208: Discrete Mathematics (Fall 2024)

• Instructor: Peter-Michael Osera
• Office Hours: Science 2811, by appointment
• Course Mentor: Peter Versh
• Meeting Times: MWF 3:00–3:50, Science 3815

What are the mathematical foundations of computer science? How does mathematical formalism relate to the pragmatics of computer science? In this course, we study discrete mathematics, broadly the branches of mathematics that study discrete objects, and their applications towards computer science.

By understanding discrete mathematics deeply, we, in turn, gain an understanding of how mathematics informs our studies as computer scientists, namely:

• We solve problems in computer science by modeling domains of problems, a process that is, at its core, mathematical.
• The interpretation of the syntax and semantics of mathematics is identical to the interpretation of a programming language, so we can leverage our understanding of programming to learn mathematics rapidly.
• There is a spectrum of reasoning between absolute mathematical formalism and informal reasoning, a spectrum that we must move across at will as competent programmers.

Finally, by studying discrete mathematics in depth and relating it to our experiences as computer programmers, we also gain expertise and comfort in studying mathematics as a discipline of modeling and problem-solving.

Discrete Structures (Fall 2024)

Overview

What are the mathematical foundations of computer science? How does mathematical formalism relate to the pragmatics of computer science? In this course, we study discrete mathematics, broadly the branches of mathematics that study discrete objects, and their applications towards computer science.

By understanding discrete mathematics deeply, we, in turn, gain an understanding of how mathematics informs our studies as computer scientists, namely:

• We solve problems in computer science by modeling domains of problems, a process that is, at its core, mathematical.
• The interpretation of the syntax and semantics of mathematics is identical to the interpretation of a programming language, so we can leverage our understanding of programming to learn mathematics rapidly.
• There is a spectrum of reasoning between absolute mathematical formalism and informal reasoning, a spectrum that we must move across at will as competent programmers.

Finally, by studying discrete mathematics in depth and relating it to our experiences as computer programmers, we also gain expertise and comfort in studying mathematics as a discipline of modeling and problem-solving.

Course Learning Outcomes

• Mathematical Literacy
  • Reading: read and comprehend mathematical text involving both symbols and prose.
  • Writing: author arguments of varying mathematical rigor with fundamental proof techniques (i.e., constructive, inductive, contradictory, and equivalence-based arguments).
  • Analyzing: critically analyze rigorous mathematical arguments for latent assumptions and missing detail.
  • Problem-solving: employ the concrete-to-abstract method to efficiently solve mathematical problems.
• Mathematical Modeling
  • Objects: model real-world phenomena using relevant objects drawn from discrete mathematics (i.e., sets, relations, random variables, and graphs).
  • Properties: formally state and prove relevant properties of mathematical models using propositional and first-order logic.
• Mathematical Computation
  • Combinatorics: count the number of elements in a finite algebraic structure using combinatorial principles.
  • Probability: compute the probability of an event using combinatorial principles.
  • Graphs: carry out the execution of fundamental graph algorithms by hand, e.g., traversals, spanning trees, and paths.
• Program Reasoning
  • Operational correctness: state and reason about formal properties of programs using operational semantics.
  • Complexity: count the number of relevant operations a (potentially recursive) program performs.
  • Algorithmic correctness: state and reason about formal properties of algorithms (specified in pseudocode) using tools drawn from discrete mathematics.
  • Constructive design: translate between a (constructive) proof of a property and a program that enjoys that property by design.
• Mathematical Soft Skills
  • Collaboration: employ appropriate collaborative strategies to productively solve problems with peers.
  • Practice: habitualize learning mathematics through self-driven, hands-on exploration and problem-solving practice.

Core Outcomes

Core learning outcomes are the fundamental skills that you should be able to confidentially perform quickly and efficiently by the end of the course. They are asssessed via the core exams we conduct throughout the semester:

• Weeks 1–4
  • Author a formal proof of a property of a pure program.
  • Author a formal proof by structural induction.
  • Author a formal proof by mathematical induction.
  • Model propositions rigorously in terms of first-order logic.
  • Author a formal proof of a abstract proposition in propositional/first-order logic.
• Weeks 5–9
  • Author a rigorous proof of the equality of two sets.
  • Author a rigorous proof utilizing classical reasoning (“proof by contradiction”).
  • Model real-world phenomena using the fundamental definitions of relations.
  • Model real-world phenomena using the formal definitions of graphs and trees.
  • Author rigorous proofs of properties of graphs and their associated algorithms.
• Week 10–13
  • Count the number of elements in an algebraic structure using combinatorial principles.
  • Accurately count the number of relevant operations that a (recursive) program performs.
  • Compute the probability of an event using fundamental combinatorial principles.
  • Apply random variables and expectation to model a probabilistic phenomena.
  • Interpret a combinatorial formula as an algorithm for constructing an object when choice is involved.

Textbook, Software, and Connectivity

There is no required textbook for this course. Required readings for the course will be distributed electronically as a work-in-progress textbook. The course webpage and readings contain suggestions for supplementary texts that give alternative takes on topics or go into more depth.

In this course, we will use the following software packages and services:

• Python: a general-purpose scripting programming language.
• Overleaf: online editing and collaboration of LaTeX documents.
• Gradescope: deliverable submission and feedback reporting.
• Microsoft Teams: communication and Q&A.

You will receive invitations to Gradescope and Teams at the beginning of the semester. Please let me know if you do not receive access to this site. The course webpage also contains additional software resources, e.g., Python and LaTeX tutorials and other utilities, that you might find useful in this course.

Diversity, Inclusion, and Accommodations

I am committed to fostering an inclusive classroom environment that allows you try, fail, and succeed, all in the service of mastering the learning outcomes of the course. In turn, I expect you to fully engage with the course through class attendance and timely submissions of work. If anything precludes you from doing so, e.g., illness, sports event, or religious observance, the golden rule is to let me know as early as possible. I will do what I can to help you succeed in the course. However, this requires that I have advanced notice, at least a week in advances, when appropriate and possible, so that we have an appropriate time frame to develop and implement a plan of action based on your needs.

I particularly encourage students with disabilities to meet with me and discuss how our classroom and course activities could impact their work and what accommodations would be essential. As part of this process, you should contact the Office of Disability Resources for further guidance and instructions.

Title IX

Grinnell College is committed to compliance with Title IX and to supporting the academic success of pregnant and parenting students and students with pregnancy related conditions. If you are a pregnant student, have pregnancy related conditions, or are a parenting student (child under one-year needs documented medical care) who wishes to request reasonable related supportive measures from the College under Title IX, please email the Title IX Coordinator at titleix@grinnell.edu. The Title IX Coordinator will work with Disability Resources and your professors to provide reasonable supportive measures in support of your education while pregnant or as a parent under Title IX.

Course Work and Evaluation

My grading philosophy comes from the grading for growth movement described in such texts as Nilson’s Specifications Grading, Feldman’s Grading for Equity, and Blum’s Ungrading. I believe that:

1. The stated learning outcomes are achievable by anyone that enrolls in this course.
2. Mastery of the learning outcomes is obtained via exploration, experimentation, and failure.
3. Eventual mastery should be valued as highly as “getting it right” the first time.
4. Your final course grade should reflect your mastery of the course’s learning goals at the end of the term.

To this end, the course is structured around several deliverables that, when taken together, indicate your mastery of the course’s learning outcomes outlined in the Overview section of the syllabus.

Deliverables

The main activities of our course are centered around four kinds of deliverables:

• Daily drills: introductory practice problems tied to each reading due the day before each class period.
• Lab exercises: collaborative practice and exploration-style problems worked on during class.
• Demonstration exercises: individually completed weekly homework sets that apply the weekly concepts to substantial tasks aligned with the themes of the course.
• Core exams: in-class exams that directly assess mastery of the core skills of the course.

Daily Drills

In each course reading, you will find a small number of practice problems that reinforce the concepts introduced in the reading. As the old saying goes, “Mathematics is not a spectator sport,” so these drills are designed to help you begin putting the day’s topics into practice.

• Each class period's daily drill is due at 10 PM the day before class.
• Daily drills are graded on a binary satisfactory (S)/non-satisfactory (N) scale. If it is clear that you have put effort into your responses by completing the drill with mostly positive results, you can expect to receive a satisfactory grade.
• There is a 24 hour grace period for turning in daily drills, e.g., if you forget to press the submit button. Otherwise, late daily drills will not be accepted! Note that you can miss several daily drills without penalty to your final grade; see how your overall letter grade is calculated for details.
• You are expected to bring your completed daily drills to class every day. We will frequently use the daily drills to begin our class discussion.

Lab Exercises

The bulk of your practice and exploration of the course learning goals come through lab exercises. These lab exercises will allow you to gain familiarity and eventual fluency with the course concepts by exploring and working through problems. Lab exercises are completed in small groups so that you can take advantage of the benefits of collaborative learning.

• Each set of labs is due the Saturday of the week that the lab is assigned. For example, if labs are assigned on Monday, Wednesday, and Friday, they are due the same week on Saturday.
• Like daily drills, labs are graded on a binary satisfactory (S)/non-satisfactory (N) scale.
• There is a 48 hour grace period to turn in labs, e.g., if you need more time to coordinate with your partner. Like daily drills, late labs will not be accepted, and you can miss several labs without penalty to your final grade; see how your overall letter grade is calculated for details.
• While labs are graded on a binary scale, you are expected to read the detailed feedback given by the course staff. This feedback will help you self-assess your mastery of the course content.

Demonstration Exercises

The demonstration exercises, i.e., weekly homework, allows you to demonstrate mastery of the course's learning outcomes through problems that put the course concepts into more practical, real-world contexts.

Demo responses will be graded in more depth than the other deliverables, specifically along two dimensions:

• Is the response correct? Does the response correctly answer the question(s) posed? Does it meet the specification outlined in the problem description?
• Is the response well-designed? Does it follow the design requirements and conventions appropriate to the medium? Is the deliverable clear, and does it communicate a proper understanding of both the problem and its solution?

Rather than using a point-based system that obscures these two dimensions, we codify these requirements with an EMRN rubric (an adaption of the “EMRF” rubric designed by Stutzman and Race). Demonstration responses are graded on a four-point scale:

• Excellent (E)
  • Complete understanding of the material is evident.
  • Exhibits, at worst, a few minor design errors and can serve as an exemplary solution for the course.
• Meets Expectations (M)
  • Complete understanding of the material is evident without the need for further revision.
  • Exhibits minor correctness or design errors that can improve the submission significantly if revised.
• Needs Revision (R)
  • One or more misunderstandings of the material are evident from the work.
  • Exhibits many minor errors or one or more major errors that necessitate revision.
• Not Completed (N)
  • Not completed to a degree where understanding is evident.

Note that excellent ratings represent work that reflects mastery of the material and mindfulness towards producing quality work. To obtain excellent ratings, you should dedicate ample time to review and revise your work—just like writing a paper—before the deadline.

Each week, normally on Mondays, you are allowed turn in up to two demonstration exercises for grading, whether they are new submissions or revisions. This includes the Monday of finals week. Additionally, you may turn in a final two demos for grading by final deadline for all work.

If you are turning in a revision of a demonstration exercise, you must fill out the revision request form in addition to turning your work in to Gradescope to notify the course staff. If you do not fill out the revision request form, the course staff will be unable to grade your revision for that week.

Core Exams

Some of the course's learning outcomes are core outcomes, demonstrable skills that you should be confident performing by the end of the semester. To directly assess your mastery of these skills, we will conduct a series of core exams during the semester. Core exams are in-class exams inspired by mastery-based testing practices found in mathematics.

Core exams consist of one problem for each core learning outcome of the course covered so far at the time of the exam. This includes all learning outcomes covered in previous core exams, allowing you reattempt problems if you missed them on previous exams!

Core problems are graded on a binary satisfactory (S)/non-satisfactory (N) scale where a satisfactory answer is completely correct (modulo minor flaws that are understandable given the timed, in-class nature of the exam). Note that, unlikely the demos, core problems more closely resemble the daily drills in terms of their scope and complexity.

Once you receive an S on a problem tied to a particular core outcome, you do not need to attempt additional problems connected to that outcome in subsequent exams, i.e., you have demonstrated mastery of that outcome, so you are done with it!

The final core exam period of the course, held during finals week, is a revision core exam. No new learning outcomes are introduced so that you have a final opportunity to demonstrate mastery of any core outcomes you have missed throughout the semester.

Final Deadline for All Work

Note that all work must be submitted by Friday, December 20, 5:00 PM CST . This is College policy and cannot be waived for any reason. If you find yourself needing to turn in work past this deadline, you must consult with me as soon as possible beforehand to submit an incomplete request for the course. Regarding incompletes:

• Incomplete requests are not automatically granted; make sure you have a backup plan in case your incomplete request is denied.
• The only work we will allow during the incomplete period are demonstration exercises.

Overall Letter Grades

Major letter grades for the course are determined by tiers, a collection of required grades from your demonstration exercises and core exams. You will receive the grade corresponding to the tier for which you meet all of the requirements. For example, if you qualify for the A tier in one category and the C tier in another category, then you qualify for the C tier overall as you only meet the requirements for a C among all the categories.

Note that I reserve the right to update the requirements for grades as circumstances dictate during the semester, e.g., if a deliverable is cut. However, I will always update the requirements so that they are no stricter than they were previously.

• D: exactly one of the requirements of a C are met.
• F: no requirements for a C are met.

Plus/minus grades

To earn a plus/minus grade, you must have completed one tier’s requirements and partially meet the next tier’s requirements. This will arise in two situations: C/B and B/A. For example, you may completely meet the requirements of a C and meet the requirements of a B for demos, but not for core exams. In these situations, you will earn a minus grade for the higher tier, i.e., a B- if you are between a C and B and an A- if you are between a B and an A.

Be aware that if you are at an A tier for one deliverable category but at a C tier for another, then you fully qualify for the C tier and partially meet the requirements of the B tier and thus would earn a B-.

Daily drill and lab grades

You may miss turning in at most three daily drills and at most three lab exercises without penalty. After the first three missing drill or lab exercises, your overall letter grade will lower by one-third of a letter grade (i.e., A becomes A-, B- becomes a C+, C becomes a D) for every two additional deliverables you miss from that category. The following table summarizes this policy for concrete numbers of missed daily drills and labs through 9 although the policy extends to any number of missing assignments.

Course Breakpoints

Our grading system offers flexibility, but at the cost of giving the illusion that if you fall behind in your work, there is always an opportunity to catch up. While this is true in theory, in practice, it is difficult to do so in many situations because of personal issues, competing courses, extracurricular obligations, etc. This flexibility also makes it difficult—for both you and myself—to determine when you have fallen behind in the course and need external help such as the course staff, tutors, or academic advising.

I encourage you to preemptively come to me for help and guidance if you feel like you are falling behind. However, to be more clear about when you might be falling behind in the course, I am tracking the following course breakpoints in your progress. When one of the following situations occurs:

• You have missed more than two classes in a row.
• You have used up either your “free” daily drill or lab assignments.
• You receive an N on a demo.
• You do not turn in any demos during a revision window in which you have outstanding demos that need revision.
• After a core examination, your total completed outcomes among all outstanding core outcomes is below 60%.
• You are otherwise at substantial risk of earning below a C in the course.

I will follow up with you and academic advising (via an academic alert) to check in, provide guidance, and develop a plan for getting back on track.

Help, Collaboration, and Academic Honesty

There are several resources—course staff, your peers, and external sources—that you can use to expedite your learning in the course. However, you must balance your use of external resources with the need to produce original work, so that we can assess your learning appropriately. To this end, we have several policies that describeou resources are permissible to use depending on the deliverable you are using them on.

The Instructor and Course Staff

Please use each course staff member’s preferred means of communication, e.g., email or Microsoft Teams DM, to communicate with them about individual issues concerning logistics, grades, demos, or core exam questions. Regardless of the medium, note that the course staff will generally not respond immediately to messages. However, we will check our messages at fixed times throught the day.

Peer Learning and Outside Resources

Utilizing discussion with peers and outside learning to facilitate your learning is a critical skill for success in computer science. However, at the same time, you must be aware that getting stuck and pushing through challenging problems is essential for robust learning. To this end, we allow the following forms of collaboration.

• You are encouraged to collaborate with your peers on daily drills and the labs. You may also consult the course staff, other people, and external resources, including AI-based completion tools. In all cases, you (or your group in the case of group work) should independently write up your solutions and cite all the resources you used in authoring your work.
• You may only discuss the demonstration exercises and core exam questions with the course staff. When completing these, you may only consult the course website and book when developing your solutions. You may not collaborate with peers, consult external resources, or share information about assignments with others.

Keep in mind that adaptation of pre-existing code or solutions whether it comes from a peer, myself, or the Internet, requires a citation in the cases where it is allowed.

In all cases, the work that you produce should be your own. The golden rule is that you should be capable of reproducing your deliverable on the spot with minimal effort if it was accidentally deleted.

If you feel that the stress and pressure of the course are compelling you to violate the academic honesty policies of the course and the college as explained in the student handbook, please talk to me as soon as possible. The course’s grading policies are designed to help you manage your time in light of the different stressors in your life. I will do my best to work with you to figure out how to help you better manage your time relative to your learning goals and desired achievement level for the course.

Sharing of Course Materials

While you retain copyright of the work you produce, we must still uphold the academic integrity of this course. To this end, you may not share copies of your assignments with others (unless otherwise allowed by the course policies) or upload your assignments to third-party websites unless substantial changes are made to the assignment (e.g., significant extensions and improvements to your code). Ultimately, it must be clear that the end product is significantly different from what was asked in the original assignment. I do recognize that there are times when you want to do this, e.g., uploading projects to Github for your resume, and so I encourage you to talk to me in advance so that we can ensure that you upload a meaningful project that does not run afoul of this policy.

Course Tools

We will use two tools in this course:

• The Python programming language as a subject for our study of program correctness.
• The LaTeX documentation preparation system to author mathematical prose.

Python is available via straightforward installers on all operating systems:

• https://www.python.org/downloads/

Additionally, it is available through most platform's package managers, e.g., Homebrew on Macs.

To develop Python code, I recommend using Visual Studio Code which features robust support for developing Python programs. Although, any editor of your choice will work!

LaTeX can similarly be installed directly on most platform:

• https://www.latex-project.org/get/

However, the raw edit-and-compilation experience for LaTeX is lacking. I recommend using the Overleaf online service for authoring LaTeX documents. Overleaf has a full-featured, in-browser LaTeX IDE that smooths away many of the warts when developing in LaTeX. A free Overleaf account is sufficient for both this course and most people's needs.

Additionally, Overleaf provides an excellent introductory tutorial to LaTeX. I highly recommend you work through it and come back to it as a reference for this course:

• https://www.overleaf.com/learn/latex/Learn_LaTeX_in_30_minutes

We'll introduce the parts of Python that you need for this course. However, you should certainly use this time to dig deeper into the language. I recommend using a comparison resource like Learn X in Y minutes:

• https://learnxinyminutes.com/docs/python/

That provides a succinct, practical reference for the language as an initial guide and, later, reference when picking up the language.

Solutions to the labs

• Exploring Python
• Program Equivalence Proofs
• Assumptions in Proofs
• Recursion to Induction
• Mathematical Induction Practice
• Strong Mathematical Induction
• Modeling with Logic
• Logical Reasoning
• More Logical Reasoning
• Artificial Examples and Sets
• A Plethora of Definition
• Graph Problems
• Spanning Trees and Shortest Paths
• Verification of State Machines

Demonstration Exercise #1

Demonstration exercises are your opportunity to showcase your mastery of the week's material. In lab, you gain practice employing the fundamental skills we introduce in class. In contrast, the demos are integrative in nature, requiring to put those skills into context as well as mix different skills together to solve problems that are more like the ones you find in the real world.

Formatting and Submitting Your Work

Create a LaTeX document for each demonstration exercise, using the csc208_template.tex template file to format your document. Your write-ups for each problem should reflect good writing principles and mathematical style:

• Grammatically correct English prose and mathematics.
• Structure of the prose made obvious through subheadings, paragraphs, and lists.
• Math appropriately integrated into the prose as needed.

To achieve this, you will need to set aside ample time for revision and editing of your work before the deadline. Approach the demonstration exercises not like a one-and-done problem set, but as a writing assignment where you are putting in work that you eventually refine into a polished, complete product.

When you are done, you should compile your LaTeX file to a PDF and then submit that PDF to Gradescope when you are done. Please do not submit your LaTeX source (in textual or PDF format); we would like to only work with a complete, rendered document!

Problem 1: Tracing

Consider the following Python program mystery that performs a more complicated recursive computation:

def mystery(l):
    if len(l) == 0:
        return []
    elif len(l) == 1:
        return l
    else:
        x = head(l)
        y = head(tail(l))
        t = tail(tail(l))
        return cons(y, cons(x, mystery(t)))

1. Give the step-by-step evaluation of the following expressions. In your work, whenever you need to write down a conditional statement, you can elide the branches of the conditional with ellipses. In other words, instead of:

   if len(l) == 0:
       return []
   elif len(l) == 1:
       return l
   else:
       x = head(l)
       y = head(tail(l))
       t = tail(tail(l))
       return cons(y, cons(x, mystery(t)))
   

   You should write instead:

   if len(l) == 0: ...
   

   • mystery([])
   • mystery(0, 1)
   • mystery("a", "b", "c", "d")

   When giving your evaluation traces, please use a verbatim block, placing each step of the derivation on its own line, separated by a long arrow (-->), e.g.,

   \begin{verbatim}
       1 + 2 * 3
   --> 1 + 6
   --> 7
   \end{verbatim}
   

2. In a sentence, describe what the mystery function does.

Problem 2: Blasting Booleans

Consider the following Python functions over booleans that give implementations of the standard boolean operations not, and, and or:

def my_not(b):
    if b:
        return False
    else:
        return True

def my_and(b1, b2):
    if b1:
        return b2
    else:
        return False

def my_or(b1, b2):
    if b1:
        return True
    else:
        return b2

Prove the following claims of program equivalence about these definitions:

Make sure not to skip any steps in your derivations!

Course Tools

We will use two tools in this course:

• The Python programming language as a subject for our study of program correctness.
• The LaTeX documentation preparation system to author mathematical prose.

Python is available via straightforward installers on all operating systems:

• https://www.python.org/downloads/

Additionally, it is available through most platform's package managers, e.g., Homebrew on Macs.

To develop Python code, I recommend using Visual Studio Code which features robust support for developing Python programs. Although, any editor of your choice will work!

LaTeX can similarly be installed directly on most platform:

• https://www.latex-project.org/get/

However, the raw edit-and-compilation experience for LaTeX is lacking. I recommend using the Overleaf online service for authoring LaTeX documents. Overleaf has a full-featured, in-browser LaTeX IDE that smooths away many of the warts when developing in LaTeX. A free Overleaf account is sufficient for both this course and most people's needs.

Additionally, Overleaf provides an excellent introductory tutorial to LaTeX. I highly recommend you work through it and come back to it as a reference for this course:

• https://www.overleaf.com/learn/latex/Learn_LaTeX_in_30_minutes

We'll introduce the parts of Python that you need for this course. However, you should certainly use this time to dig deeper into the language. I recommend using a comparison resource like Learn X in Y minutes:

• https://learnxinyminutes.com/docs/python/

That provides a succinct, practical reference for the language as an initial guide and, later, reference when picking up the language.

Concrete Evaluation

We begin our journey into the foundations of computer science by first studying one of its key applications to computer programming: program correctness. Rigorously stating and proving program properties will require us to deep-dive into mathematical logic, the sub-field of mathematics devoted to modeling deductive reasoning. Deductive reasoning is the foundation for virtually all activities in computer science, whether you are designing an algorithm, verifying the correctness of a circuit, or assessing a program's complexity. In this manner, this initial portion of our investigation of the foundations of computer science is, quite literally, the cornerstone of everything you do in this field moving forward.

Why Functional Programming?

In this course, we'll use the Python programming language as our vehicle for studying program correctness. In particular, we'll focus on a pure, functional subset of Python that corresponds to other function languages such as the Scheme we introduce in CSC 151. We do this because, as we will see shortly, pure, functional languages admit for a simple, substitution-based model of computation. By "pure," we mean that the language does not allow functions to produce side-effects. A side-effect is some behavior observable to the caller of the function beyond the function's return value.

The canonical example of a side-effect is the mutation of global variables. For example, in Python:

glob = 0    # a global variable

def increment_global():
    # in Python, we have to declare a global variable as
    # locally accessible with a `global` declaration
    global glob
    glob = glob + 1

def main():
    print(glob)           # 0
    increment_global()
    print(glob)           # 1
    increment_global();
    print(glob)           # 2
    increment_global();
    increment_global();
    print(glob)           # 4

The increment_global function takes no parameters and produces no output. Its sole task is to produce a side-effect: change the state of global by incrementing its value. Since the function does not return a value, main can only use increment_global for its side-effect by calling the function and observing the change to global.

We'll have more to say about side-effects and their relationship with the substitutive model of computation we introduce later in this reading. For now, note that ultimately it is not the language that is important here. What is important is whether we are considering a pure fragment of that language, instead. Indeed, the lessons we learn here regarding program correctness apply to any program that behaves in a pure manner, i.e., has no side-effects. For example, we can easily translate our model of computation to the pure fragment Python!

This fact supports a general maxim about programming you have hopefully heard at some point:

Minimize the number of side-effects in your code.

Intuitively, complicated code with side-effects is frequently tricky to reason about, e.g., explicit pointer manipulation in C. Our study of program correctness in this course will give us concrete reasons why this is indeed the case.

Program Correctness

Program correctness is a particularly topical application of logic to start with because every developer cares that their programs are correct. However, what do we mean by correctness?

For this example, we'll first introduce several functions so that we can operate on Python lists like Scheme lists. These functions give common names to common list indexing and access tricks that we would use in Python to achieve the same effect.

# returns the head (first element) of list l
def head(l):
    return l[0]

# return the tail of l, a list that is l but without its first element
def tail(l):
    return l[1:]

# return true iff list l is empty
def is_empty(l):
    return len(l) == 0

# return a new list that is the result of consing x onto the front of l
def cons(x, l):
    return [x, *l]

With these functions in mind, consider the following Python function that appends two lists together recursively:

def list_append(l1, l2):
    if is_empty(l1, l2):
        return l2
    else:
        return cons(head(l1), list_append(tail(l1), l2))

What does it mean for list_append to be "correct"? Of course, we have a strong intuition about how list_append should behave: the result of list_append should be a list that "glues" l2 onto the end of l1. But being more specific about what this means without saying the word "append" is tricky! As we try to crystallize what it means for list_append to be correct, we run into two issues:

Generality

A natural way to specify the correctness of list_append is through a test suite. For example, in Python, we can write a simple collection of tests using the unittest module:

import unittest

class list_appendTest(unittest.TestCase):
    def test(self):
      self.assertEqual(list_append([1, 2], [3, 4, 5]), [1, 2, 3, 4, 5])
      self.assertEqual(list_append([], [1, 2, 3, 4 ,5]))
      self.assertEqual(list_append([1, 2, 3, 4, 5], []))

unittest.main()

Note that these tests exemplify very specific properties about the behavior of list_append. A test case demands that when a function is given a particular set of inputs, e.g., [1, 2] and [3, 4, 5], that the function must produce the output [1, 2, 3, 4, 5]. You can't get more specific about the behavior of list-append than that!

However, are these tests enough? While they cover a wide variety of the potential behavior of list_append, they certainly don't cover every possible execution of the function. For example, the tests don't cover when list-append is given two empty ([]) lists. They also don't cover the case where the expected output is not [1, 2, 3, 4, 5]! In this sense, while tests are highly specific, they do not necessarily generalize to the full behavior of the function. This always leaves us with an inkling of doubt that our functions are truly correct.

Specificity

How might we arrive at a more general notion of program correctness? Rather than thinking about concrete test cases, we might consider more abstract propositions about the behavior of the function. Such abstract propositions are typically framed in terms of relationships between the inputs and outputs of the function. With list_append, we might think about the lengths of the input and output lists and how we might phrase our intuition about the function "gluing" its arguments together. This insight leads to the following property that we might check of the function:

For all lists l1 and l2, len(l1) + len(l2) $=$ len(list_append(l1, l2)).

To put another way, the lengths of l1 and l2 are preserved through list_append. That is, list_append doesn't (a) add any elements to the output beyond those found in the input, and (b) does not remove any elements.

By virtue of its statement, this property applies to all possible inputs to list_append. So if we were able to prove that this property held, we knew that it holds for the function, irrespective of the inputs that you pass to the function (assuming that the inputs are lists, of course). This stands in contrast to test cases where we make claims over individual pairs of inputs and outputs.

However, unlike a test case which is highly indicative of our intuition of correctness for this function, this property is only an approximation of our intuition. To put it another way, even if we know this property holds of every input to list_append, it doesn't mean that the function is correct! Here is an example implementation of list_append where the property holds, but the function is not "correct":

define bad_list_append(l1, l2):
    if is_empty(l1):
        return l2
    else:
        cons(0, bad_list_append(tail(l1), l2))

The lengths of the input lists are preserved with bad_list_append. However, the output is not the result of gluing together the input lists!

bad_list_append([1, 2, 3], [4, 5])
> [0, 0, 0, 4, 5]

Every element of l1 is replaced with 0! In this sense, our length-property of list_append is general---it applies to every possible set of inputs to the function---but not specific---the property only partially implies correctness.

Balancing Generality and Specificity

In summary, we've seen that test cases and general program properties sit on opposite ends of the generality-specificity spectrum. When we think about program correctness and verifying the behavior of programs, we are always trying to find the balance between generality and specify in our verification techniques. Ultimately, you can never be 100% sure that your program works in all cases---after all, a stray gamma ray can ruin whatever verification you have done about your program. So when employing program verification techniques---testing, automated analysis, or formal proof---you must ultimately make an engineering decision based on context, needs, and available time and resources. We won't have time to dedicate substantial time to these pragmatic concerns in this course, but keep them in the back of your mind as we introduce formal reasoning for program correctness in the sections that follow.

A Substitutive Model of Computation

In order to rigorously prove that a property holds of a program, we must first have a rigorous model of how a program executes. You likely have some intuition about how Python programs operate. For example, try to deduce what this poorly named function does:

def foo(bar):
    if is_empty(bar):
        return 0
    else:
        1 + foo(tail(bar))

How might you proceed? You might imagine taking an example input, e.g., [9, 1, 2], and predicting how the function processes that input. With a few examples and prior knowledge of how conditionals and recursion work, you can likely deduce that this function calculates the length of the input list given to it. Our first goal, therefore, is to formalize this intuition, namely, explicate the rules that govern how Python programs operate.

For a pure, functional programming language like the subset of Python that we work with, we can use a simple substitutive model of computation that extends how we evaluate arithmetic expressions. While simple, this model is capable of capturing the behavior of most Python programs we might consider in this course.

Review: Arithmetic Expressions

First, let's recall the basic definitions and rules surrounding arithmetic expressions. We can divide these into two sorts:

• Syntactic definitions and rules that govern when a collection of symbols is a well-formed arithmetic expression.
• Semantic definitions and rules that give meaning to a well-formed arithmetic expression. "Meaning," in this case, can be thought of as "how the arithmetic expression computes."

Syntax

Here is an example of a well-formed arithmetic expression:

$$8\times (10-5÷2)$$

In contrast, here is an ill-formed arithmetic expression:

$$\begin{gathered} (4+5)-( \\ ;\times 9) \end{gathered}$$

In this ill-formed arithmetic expression, the multiplication operator (×) is missing a left-hand argument.

We can formalize this intuition about how to create a well-formed arithmetic expression with a grammar. Similarly to natural language, grammars concisely define syntactic categories as well as rules of formation for various textual objects. Here is a grammar for arithmetic expressions:

e ::= <number> | e1 + e2 | e1 - e2 | e1 × e2 | e1 ÷ e2 | (e)

To the left of the ::= symbol is a variable, e, that represents a particular syntactic category. To the right are the rules for forming an element of that category. Here, the syntactic category is "arithmetic expressions," traditionally represented with the variable e. The rules are given as a collection of possible forms or alternatives, separated by pipes (|). The grammar says that a well-formed expression is either:

• A number (<number> is a placeholder for any number), or
• An addition of the form e1 + e2 where e1 and e2 are expressions, or
• A subtraction of the form e1 - e2 where e1 and e2 are expressions, or
• A multiplication of the form e1 × e2 where e1 and e2 are expressions, or
• A division of the form e1 ÷ e2 where e1 and e2 are expressions, or
• A parenthesized expression of the form (e) where e is an expression.

Importantly, the grammar is recursive in nature: the various alternatives contain expressions inside of them. This allows us to systematically break down an arithmetic expression into smaller parts, a fact that we leverage when we evaluate expressions. For example:

• $8\times (10-5÷2)$ is an expression.
• $8$ is an expression.
• $(10-5÷2)$ is an expression.
• $10-5÷2$ is an expression.
• $10$ is an expression.
• $5÷2$ is an expression.
• $5$ is an expression.
• $2$ is an expression.

Note that when interpreting symbols, there is sometimes ambiguity as to how different symbols group together. For example, consider the sub-expression from above:

$$10-5÷2.$$

Should we interpret the expression as $10$ and $5÷2$ as in the example or alternatively $10-5$ and $2$. Our knowledge of arithmetic tells us that the first interpretation is correct because the $(÷)$ operator takes precedence over the $(-)$ operator. Rules of precedence are, therefore, additional syntactic rules that we must consider in some cases. There also exist rules of associativity for some grammars that govern the order in which we group symbols when the same operator is invoked multiple times. For example, we traditionally interpret subtraction as left-associative. That is $1-2-3$ is understood to be $(1-2)-3$ rather than $1-(2-3)$, i.e., $1-2$ goes first rather than $2-3$.

Semantics

Once we have established what a well-formed expression looks like, we then need to define what it means. In general, the meaning of a well-formed object is dependent entirely on the purpose of said object. For arithmetic expressions, we care about computing the result of such an expression, so we take that to be the meaning or semantics of an expression.

Traditionally, we define the rules for computing or evaluating an arithmetic expression as follows:

1. Find the next sub-expression to evaluate using the rules of associativity and precedence to resolve ambiguity.
2. Substitute the value that the sub-expression evaluates to for that sub-expression in question.
3. Repeat the process until you are left with a final value.

A value is simply an expression that can not be evaluated or simplified any further. For arithmetic expressions, any number is a value.

By repeating this process, we obtain a series of evaluation steps that an arithmetic expression takes before arriving at a final value. For example, here are the steps of evaluation taken for our sample expression from above:

    8 × (10 - 5 ÷ 2)
--> 8 × (10 - 2.5)
--> 8 × 7.5
--> 60

Note that at each step, the resulting expressions are equivalent, e.g., $8\times (10-5÷2)$ and $8\times 7.5$ are equivalent; both of these expressions are also equivalent to the value $60$.

Core Python and the Substitutive Model

Our substitutive computational model for Python extends the rules for evaluating arithmetic expressions. Like arithmetic expressions, we will think of Python programs as an expression that evaluates to a final value. And like arithmetic, programs operate by stepwise evaluation, where we find the next sub-expression to evaluates and substitute. Python's rules for precedence mirror those from arithmetic. So we only need to consider precedence for Python's additional constructs beyond arithmetic.

Expressions

For our purposes, well-formed Python expressions can be defined by the following grammar:

e ::= x                         (variables)
    | <number>                  (numbers)
    | True                      (true)
    | False                     (false)
    | lambda (x1, ..., xk): e   (lambdas)
    | e(e1, ..., ek)            (function application)

In other words, a Racket expression is either:

• A variable x.
• A number.
• The true value True.
• The false value False.
• A Lambda with arguments x1, ..., xk and a body expression e.
• A function application applying arguments e1, ..., ek to function e.

As an example, the following expression taken from our definition of list_append above:

cons(head(l1), list_append(tail(l1), l2))

Is a well-formed expression that is a function application of two arguments to the function bound to the variable cons. Each argument is, itself, a function application.

Values

In arithmetic, numbers were our only kind of value. In Racket, we have multiple kinds of values corresponding to the different types of Racket:

• Numbers are still values (of type int or float depending on whether number is integral or floating-point).
• True and False are values (of bool type)
• lambda (x1, ..., xk): e is also a value (of function type).

Statements

In addition to expressions, Python also has statements defined by the following grammar:

s ::= s1                    (sequenced statements)
      s2
    | x = e                 (variable declaration/assignment)
    | def f(x1, ..., xk):   (function declaration)
          s
    | return e              (returns)
    | if e1:                (conditional statements)
          s1
      else:
          s2

The sequenced statement looks syntactically odd on its own. But it captures idea that wherever one statement is expected, multiple statements can appear by placing them one line after the other at the same indentation level. For example:

def f(x):
    y = x + 1
    z = y + 1
    return x + y + z

Here, the body of f can be thought of as three statements or a single sequenced statement (y = x + 1) that, itself, precedes a single sequenced statement (z = y + 1), that, itself, precedes a final statement (return x + y + z).

In contrast to expression, statements do not produce values. Instead, they have some kind of effect on the execution of our program. For example:

• Variable and function declarations introduce new variables into scope.
• Return statements causes the program to return from a function with a specified value.
• Conditional statements transfer the flow of execution into one of several possible branches.

Reviewing our list_append definition, we see that it is a function declaration. The body of list_append is a single conditional and inside each branch of the conditional is a return statement.

Substitutive Evaluation for Python

The heart of Python evaluation is function application. Function application directly generalizes arithmetic evaluation for operators: In arithmetic evaluation:

1. We first evaluate the left- and right-hand arguments to the operator to values.
2. We then apply the operator to those values.

For example, for $e_1+e_2$, we first evaluate $e_1$ to a value, call it $v_1$ and then evaluate $e_2$ to a value, call it $v_2$. We then carry out the addition of $v_1$ and $v_2$.

To evaluate a function application, we first evaluate each of the sub-expressions of the function application to values. For example, consider the inc function defined to be:

def inc(n):
    return n + 1

if we have the expression, inc(3 + (5 * 2)), it evaluates as follows:

    inc(3 + (5 * 2))
--> inc(3 + 10)
--> inc(13)

Once we arrive at this point, we need to evaluate the actual function application itself. In the case of primitive operations, we just carry them out directly and substitute their resulting values into the overall expression. However, arbitrary functions will perform arbitrary operations, so we cannot simply just "substitute the result"; we must calculate it by hand!

To do this, we want to perform the following steps:

1. We substitute the body of the function be applied to for the overall function application.
2. We substitute the actual arguments passed to the function for each of its parameters.
3. We then continue evaluation of the resulting expression like normal.

However, you may have noticed in the Python grammar we presented earlier that the body of functions are statements and not expressions. This poses a conundrum for our evaluation model because we want each step to be a valid expression in our language. In other words, we don't want to an expression to step to a statement; that doesn't make sense!

To reconcile this fact, we will introduce one additional expression form that only appears in our step-by-step evaluative model. The statement-expression, written {s1; ...; sk} represents a series of statements that are currently executing that must end in a return statement. The value that this return statement evaluates to is what this statement-expression evaluates to when it is done executing.

For example, with our inc expression above:

1. We substitute the statement-expression {return n + 1} for the function call inc(13).
2. We substitute 13 for n everywhere it occurs in this new statement-expression: {return 13 + 1}.
3. We continue evaluation of the resulting expression like normal.

To evaluate a statement-expression, we execute the first statement in the list of statements left to execute. In our example, this means we must evaluate return 13 + 1. Evaluating a return statement is straightforward: we evaluate the return's expression to a value and then substitute this value for the entire statement-expression.

This results in the following steps of evaluation:

    (inc 13)
--> {return 13 + 1}
--> {return 14}
--> 14

Observe how the body of inc took two steps to evaluate: one to evaluate the return's argument and one to return from the function call.

These rules apply to functions of multiple arguments as well. For example, consider the following definition of a function that averages three numbers:

def avg3(x1, x2, x3):
    return (x1 + x2 + x3) / 3

Then the expression avg3(2 * 5, 8, 1 + 2) evaluates as follows:

    avg3(2 * 5, 8, 1 + 2)
--> avg3(10, 8, 1 + 2)
--> avg3(10, 8, 3)
--> {return (10 + 8 + 3) / 3}
--> {return (18 + 3) / 3}
--> {return 21 / 3}
--> 7

Note that we evaluate the arguments to avg3 in left-to-right order, one argument at a time.

def f(x, y):
    return x + y

def g(a, b):
    return f(a, a) - f(b, b)

Return Statements

As described above, to evaluate a return statement:

1. Evaluate the return's argument to a value.
2. Substitute this value for the return statement's immediate surrounding statement-expression.

In other words, {return v} --> v for any value v.

Statement-expressions can be nested because functions call other functions. In these situations, we simply evaluate the innermost statement-expression. This corresponds to evaluating the most recent function call!

For example, consider the following example:

def f(n):
    return n + 1

def g(a, b)
    return f(a) + f(b)

And consider the step-by-step evaluation of g(8, 2):

    g(8, 2)
--> {return f(8) + f(2)}
--> {return {return 8 + 1} + f(2)}
--> {return {return 9} + f(2)}
--> {return 9 + f(2)}
--> {return 9 + {return 2 + 1}}
--> {return 9 + {return 3}}
--> {return 9 + 3}
--> {return 12}
--> 12

Conditionals

Recall that conditional statements have the form:

if e:
    s1
else:
    s2

To evaluate a conditional:

1. We first evaluate the guard e to a value. This value ought to be a boolean value, i.e., True or False.
2. If the guard evaluates to True, we substitute statement s1 for the entire conditional.
3. Otherwise, the guard must have evaluated to False. We, therefore, substitute s2 for the entire conditional.
4. We then continue evaluating the resulting expression.

Here is an example of a conditional within our substitutive model.

    1 + { if 3 < 5:
              return 2
          else:
              return 5 * 5 }
--> 1 + { if False:
              return 2
          else:
              return 5 * 5 }
--> 1 + { return 2 }
--> 1 + 2
--> 3

Note that it is sometimes quite onerous to write a conditional statement over multiple lines. When it is more prudent to do so, we will collapse everything onto a single line, e.g.,

{if 3 < 5: return 2 else: return 5 * 5}

Variable Declarations

Variable declarations allow us assign names to intermediate computations for the purposes of readability or performance (i.e., to avoid redundant work). To evaluate a variable declaration of the form x = e:

1. We evaluate e to a value v.
2. We substitute every occurrence of x for v in the immediate statement-expression that encloses this assignment.
3. Finally, we remove this variable declaration from the statement-expression that we are evaluating.

Consider the following function that declares local variables:

def f():
    x = 1 + 1
    y = x * 2
    z = x * y
    return x + y + z

Here's an example of the step-by-step evaluation of a call to this no-argument function:

    f()
--> { x = 1 + 1
      y = x * 2
      z = x * y
      return x + y + z }
--> { x = 2
      y = x * 2
      z = x * y
      return x + y + z }
--> { y = 2 * 2
      z = 2 * y
      return 2 + y + z }
--> { y = 4
      z = 2 * y
      return 2 + y + z }
--> { z = 2 * 4
      return 2 + 4 + z }
--> { z = 8
      return 2 + 4 + z }
--> { return 2 + 4 + 8 }
--> { return 6 + 8 }
--> { return 14 }
--> 14

Additional Exercises

def compute3(x, y, z):
    intermediate = x + y
    return z * intermediate + intermediate

def triple(n):
    return compute3(n, n, n)

Exploring Python

Today, we'll explore our first mathematical model, a substitutive semantics for Python programs.

LaTeX and the CSC208 Package

For each lab and demonstration exercise, you will submit a final LaTeX-generated PDF with your solutions. To help format your files, we've created a LaTeX template template for you to use. You can download the template here:

• csc208_template.tex

The template includes a number of standard packages and formats the document to look like a more traditional document, i.e., not in narrow column format.

To get started, simply download the file and import it into a new Overleaf project. Make sure to fill in the \title, \author, and \grinnellusername macros at the top of the file with the appropriate information!

For each problem, you should use the \begin{problem} ... \end{problem} environment to format your solutions by problem. Note that the environment puts each problem on a new page!

Problem 1: What's in a name?

A strength of possessing an explicit computation model is explaining tricky corner cases in the language's design. In this problem, we'll look at some of the issues arising with names in Python.

Consider the following function definitions.

def f1(x, y):
    return x + y + x

def f2(n):
    return n * 3

def f3(n):
    return f2(4) + f2(n) + n

1. Give execution traces for each of the following expressions. Try to let each member of your group take the lead on writing down the derivation, so everyone gets their practice in. The remaining members of the group should check their work.

   When formatting your traces, use the \begin{verbatim} ... \end{verbatim} environment. Importantly, verbatim will allow a chunk of text to leak off the page if it is too big. If this is the case, please properly format your document by introducing newlines and/or breaking up your trace into multiple verbatim blocks!

   • f1(1+2, 7)
   • f2(f2(f3(5)))
   • f3(11)

2. Consider an alternative definition of f2 given below:

   def f2(x):
       return x * 3
   

   Compare the second expression's execution from the last part (f2(f2(f5(5)))) with the old and new definitions of f2. In a few sentences:

   • Comment on the behavior of both versions of f2. Do they behave the same or differently?
   • From this example, what can you say about the choice of names of function parameters between different functions. Does it matter what names you choose? Why or why not?

3. Now consider the following top-level declarations:

   value = 12              # A
   
   print(value)            # 1
   
   def f(value):           # B
       x = value           # 2
       value = 5           
       return x + value    # 3
   
   f(value)                # 4
   print(value)            # 5
   

   Give an execution trace for the expression on line 4. Double-check your final result in Python.

4. Based on your derivation, determine which definitions of value (points labeled A--C) are used for each usage of value in f, i.e., the points labeled 1--5.

5. Give a rule for determining which of the definitions of a variable applies to some use of that variable. Once you have a candidate rule, check your answer with a member of the course staff.

Problem 2: Loop the Loop

Another corner case in the evaluation of Python programs concerns non-termination. Consider the following recursive function:

# Returns a new list that is l with x in head position
def cons(x, l):
    return [x, *l]

def mystery(n, x)
    if n == 0:
        return []
    else:
        return cons(x, mystery(n - 1), x)

1. Give execution traces for each of the following expressions. Again, let every group member take lead on at least one of the expressions. Note that we didn't talk about recursion in the reading! However, there is nothing new to say here—recursion "just works" in this model, so follow your nose!

   • mystery(0, 10)
   • mystery(1, "a")
   • mystery(3, False)

   In a sentence or two describe what this function does.

2. Now, trace the execution of this expression. What happens to your execution trace for this expression? Give enough of your trace to explain what is going on.

   • mystery(-1, "q")

3. Run this expression in Python. What happens? Try to reconcile explain the behavior of Python in terms of how your trace played out.

4. Try tracing this curious expression:

   • (lambda x: x(x))(lambda x: x(x))

   Be very careful about variable names and substitution here! What happens to your execution trace for this expression? Give enough of your trace to explain what is going on.

Propositions and Proofs

Our formal model of computation allows us to reason about the behavior of programs. But to what ends can we apply this reasoning? Besides merely checking our work, we can also use our formal model to prove propositions about our programs.

Another word for a proposition is a claim. Here are some example propositions over programs that we could consider:

• len("hello world!") is equivalent to 12.
• There exists a list l for which len(l) is 0.
• insertion_sort(l) performs more comparison operations than mergesort(l) for any list l.
• For any number n, 2 * n is greater than n.

The first proposition is a fully concrete proposition of the sort we have previously considered. The second is an abstract proposition because it involves a variable, here l.

Ultimately, the first two propositions involve equivalences between expressions. But propositions do not need to be restricted to equivalences. The third proposition talks about the number of operations that one expression performs relative to another.

Furthermore, propositions don't even need to be provable! For example, the final proposition is not provable. A counterexample to this proposition arises when we consider n = -1. 2 * -1 evaluates to -2, and -2 is not greater than -1!

Equivalences Between Expressions

Of the many sorts of propositions possible, we will work exclusively with equivalences in our discussion of program correctness.

Recall that $e⟶e^{\prime }$ ("steps to", LaTeX: \longrightarrow) means that the Python expression $e$ takes a single step of evaluation to $e^{\prime }$ in our mental model of computation. The notation $e{⟶}^{\ast }{e}^{\prime }$ ("evaluates to", LaTeX: \longrightarrow^*) means that $e$ takes zero or more steps to arrive at $e^{\prime }$. With this in mind, the formal definition of equivalence amounts to saying the following:

Two expressions are equivalent if they evaluate to identical values.

Thus, we can prove a claim of program equivalence by using our mental model to give a step-by-step derivation (an execution trace) of an expression to a final value. If both sides of the equivalence evaluate to the same value, then we know they are equivalent by our definition! The execution trace itself is a proof that the equivalence holds.

For example, consider the following recursive definition of factorial:

def factorial(n):
    if n == 0:
        return 1
    else:
        n * factorial(n-1)

and subsequent claim about its behavior:

We can prove this claim by evaluating the left-hand side of the equivalence and observing that it is identical to the right-hand side:

    factorial(3)
--> {if 3 == 0: return 1 else: return 3 * factorial(3-1)}
--> {if False: return 1 else: return 3 * factorial(3-1)}
--> {return 3 * factorial(3-1)}
--> {return 3 * factorial(2)}
--> {return 3 * { if 2 == 0: return 1 else: return 2 * factorial(2-1)}}
--> {return 3 * { if False: return 1 else: return 2 * factorial(2-1)}}
--> {return 3 * { return 2 * factorial(2-1)}}
--> {return 3 * { return 2 * factorial(1)}}
--> {return 3 * { return 2 * {if 1 == 0: return 1 else: return 1 * factorial(1-1)}}}
--> {return 3 * { return 2 * {if False: return 1 else: return 1 * factorial(1-1)}}}
--> {return 3 * { return 2 * {return 1 * factorial(1-1)}}}
--> {return 3 * { return 2 * {return 1 * factorial(0)}}}
--> {return 3 * { return 2 * {return 1 * {if 0 == 0: return 1 else: return 0 * factorial(0-1)}}}}
--> {return 3 * { return 2 * {return 1 * {if True: return 1 else: return 0 * factorial(0-1)}}}}
--> {return 3 * { return 2 * {return 1 * {return 1}}}}
--> {return 3 * { return 2 * {return 1 * 1}}}
--> {return 3 * { return 2 * {return 1}}}
--> {return 3 * { return 2 * 1}}
--> {return 3 * { return 2}}
--> {return 3 * 2}
--> {return 6}
--> 6

This precise step-by-step analysis of the behavior of the expression rigorously proves our claim!

Formatting Proofs

We will use this standard format for writing formal proofs for the remainder of the course. In summary, we write:

Symbolic Execution

Previously, we introduced a model of computation for the Racket programming language. This model allows us to prove program properties when concrete values are involved. However, we frequently wish to prove properties where the values are unknown. For example, we might consider a proposition about the standard list_append function:

For all lists l1 and l2, len(l1) + len(l2) = len(list_append(l1, l2))

This proposition ranges over unknown, rather than concrete, lists. We, therefore, need to upgrade our mental model to work with these unknown quantities.

Abstract Propositions

Up to this point, we have considered concrete expressions, i.e., expressions that do not contain variables. What happens if we allow expressions to contain variables. As an example, consider the following implementation of the boolean and function:

# N.B. non-short-circuiting version of `and`
def my_and(b1, b2):
    if b1:
        return b2
    else:
        return False

Now, let's consider the following equivalence claim:

Claim: my_and(True, b) ≡ False

Here, b is a variable, presumed to be of boolean type. However, how do we interpret b? It turns out there are two interpretations we might consider:

• Does there exist a boolean value to b so that the proposition is provable?
• Is the proposition provable for all possible boolean values that b can take on?

The former interpretation is called an existential quantification of b. We alternatively say that b is existentially quantified or is an "existential." Quantification refers to the fact that our interpretation tells us "how many" values of b to consider in the proposition. In existential quantification, we consider a single value.

In contrast, the latter interpretation is called a universal quantification of b. In universal quantification, we mean that the proposition holds for all possible values of b. Note that the above proposition is provable if b is interpreted existentially: if we let b be #f then:

    my_and(True, b)
--> my_and(True, False)
--> { if True: return False else: return False }
--> { return False }
--> False

However, the proposition does not hold when b is universally quantified. More specifically, while it holds when b is False, it does not hold when b is True.

    my_and(True, b)
--> my_and(True, True)
--> { if True: return False else: return False }
--> { return False }
--> False

Because of this, we must be explicit when introducing variables into our proposition. For each such variable, we must declare whether it is existentially quantified and universally quantified. To do so, we can use the words:

• For all for universal quantification, e.g., "for all lists l …" and
• There exists for existential quantification, e.g., "there exists a number n …".

Furthermore, we reason about the variable differently depending on its quantification, as we see in the following sections.

Existential Propositions

If a variable $x$ appears as an existential in a proposition, we interpret that variable as: there exists a value for $x$ such that the proposition holds. In other words, the proposition is provable if we can give a single value to substitute for $x$ so that the resulting proposition is provable. Thus, to prove an existential claim, we can choose such a value, substitute for the existential variable, and then use concrete evaluation as before.

As an example, let's formally prove the existential version of the my_and claim that we introduced above:

    my_and(True, False)
--> my_and(True, False)
--> { if True: return False else: return False }
--> { return False }
--> False

Note how our proof has changed now that our proposition is abstract:

1. In our claim, we explicitly quantify the variable b by declaring it existential by using "there exists" to describe it.
2. In our proof, we explicitly choose a value for the existentially quantified variable ("Let b be False").

We can also existentially quantify over multiple variables. In these situations, we provide instantiations for each variable but otherwise proceed as normal.

    list_append([], [1, 2, 3])
--> { if is_empty([]):
          return [1, 2, 3]
      else:
          return cons(head([]), list_append(tail([]), [1, 2, 3]))
    }
--> { if True:
          return [1, 2, 3]
      else:
          return cons(head([]), list_append(tail([]), [1, 2, 3]))
    }
--> { return [1, 2, 3] }
--> [1, 2, 3]

Universal Quantification

When a variable is universally quantified, it stands for any possible value. Let's take a look at a simple squaring function:

def square(n):
    return n * n

And a simple universal claim about this function:

Because the claim holds for all possible values of n, we can't choose a n like with existentials. Instead, we must hold n abstract, i.e., consider it to be an arbitrary number, and then proceed with the proof. In effect, because n is universally quantified, we treat n like a constant, yet unknown, quantity in our reasoning.

When we use our mental model of computation, we immediately arrive at a problem: both square(n) and n * n cannot take any evaluation steps! square(n) cannot step because n needs to be a value before we perform the function application, and we said that values were numbers, boolean constants, or lambdas. n * n cannot step because since we don't know what n is, we don't know what concrete value the multiplication will produce. We say that both expressions are stuck: they are not values, but they cannot take any additional evaluation steps.

We can't reconcile the n * n case. Without knowing what n is, we cannot carry out the multiplication. However, if we treat the constant-yet-unknown n as a value, then we can proceed with the function application:

    square(n)
--> n * n

Even though the left- and right-hand sides of the equivalence are not values, they are identical. This fact is sufficient to conclude that the two original expressions are equivalent according to our definition of program equivalences! Let's put these ideas together into a complete proof of the proposition:

In summary, when we encounter a universally quantified variable in a proposition, we:

1. Consider the variable to be a constant, yet unknown value. For convenience, we keep the name of this constant to be the same as the (universally quantified) variable, but we understand that the two are different objects!
2. When reasoning about the constant, we assume that it is a value for the purposes of our mental model of computation.

Case Analysis

Sometimes when we work with universally quantified variables, we can get away without thinking about their actual values. However, more often or not, our reasoning must consider their possible values. This reasoning will ultimately depend on the types of values involved, and this is where our proofs get more intricate in their design!

As an introduction to these concepts, let's consider the case where we know the type in question only allows for a finite set of values. At present, only the boolean type has this property. Booleans only allow for two values, True and False, whereas there are an infinite number of numbers and functions to choose from!

To see how we can take advantage of the finiteness of the boolean type in our proofs, let's consider the following simple claim, again using the my_and function:

If we let b be arbitrary, we can begin evaluating the left-hand expression.

    my_and(b, False)
--> { if b: return False else: return False }

We can see pretty readily that no matter how the conditional evaluates, we will return False. Be careful, though; this intuition is not sufficient for formal proof! We must instead rely on our evaluation model directly to ultimately show that this intuition is correct. However, if b is unknown, we don't know which branch the conditional will produce.

Thankfully, we assumed that b was a boolean, so it must either be True or False. Therefore, we can proceed by case analysis: we will consider two separate cases, b is True and b is False, and show that the claim holds in both cases. If the claim holds for both cases, we know that the claim holds for every possible value of b and, thus, have completed the proof.

    my_and(b, False)
--> { if b: return False else: return False }

\begin{proof}
  Because \code{b} is a boolean, either \code{b} is \code{True} or \code{b} is \code{False}.

  \begin{itemize}
  \item \textbf{\code{b} is \code{True}}.
    Then \code{ \{ if True: return False else: return False \} --> \{ return False \} --> False }
  \item \textbf{\code{b} is \code{False}}.
    Then \code{ \{ if False: return False else: return False \} --> \{ return False \} --> False }`
  \end{itemize}

  In both cases, the left-hand side steps to \code{#f}, precisely the right-hand side of the equivalence.
\end{proof}

def my_of(b1, b2)
    if b1:
        True
    else:
        b2

Program Equivalence Proofs

Problem 1: Equivalence Propositions

Exploring a model for interesting corner cases and behavior is one thing. However, we are ultimately interested in using our model to formally prove properties of programs. We call such properties propositions, statements about the world that are (potentially) provable. A proof is a logical argument that the proposition is indeed true.

There are many kinds of propositions we might consider when we think about program correctness. The most fundamental of these is program equivalence, asserting that two programs produce the same value.

Let's try writing our first proof and writing it down in LaTeX. Here is a recursive function definition over lists:

def is_empty(l):
    return len(l) == 0

def head(l):
    return l[0]

def tail(l):
    return l[1:]

def cons(x, l)
    return [x, *l]

def list_length(l):
    if is_empty(l):
        return 0
    else:
        return 1 + list_length(tail(l))

We will prove the following claim:

The equivalence symbol (≡) (LaTeX: \equiv) acts like equality in that it asserts that the left- and right-hand sides of the symbol are equivalent. We say that two programs are equivalent if they evaluate to the same final value.

1. Before we write anything, we must prove the claim first! To show that an equivalence between two expressions holds, it is sufficient to show that both sides evaluate to identical values. The right-hand side of the equivalence is already a value, 3, so we need to show that the left-side of the equivalence evaluates to this same value. Use our mental model of computation to give an evaluation trace of list_length([21, 7, 4]).

2. Now, let's write the proof in your lab write-up. When writing proofs, we will always:

   • Restate the claim.
   • Give the proof.

   For example, here is a proof of a simple arithmetic equivalence in this style:

   Sample Proof

   Claim: `5 * pow(2, 3) - 1` ≡ `39`.
   

   Proof. The left-hand side of the equivalence evaluates as follows:

       5 * pow(2, 3) - 1
   --> 5 * 8 - 1
   --> 40 - 1
   --> 39
   

   □

Problem 2: Symbolic Reasoning with Xor

Consider the following definition of the boolean xor function:

def xor(b1, b2):
    if b1:
        return not b2
    else:
        b2

Prove the following claims about this function:

For this final equivalence, you may evaluate individual calls to and, or, and not, in a single step of evaluation.

Demonstration Exercise 2

Problem 1: Verified Grades

1. Write a function calculate_grade(num_n, num_r, num_m, num_e, num_core) that takes five arguments, the number of Ns, Rs, Ms, Es, and core LOs earned by a student in this course and returns a string corresponding to the major letter grade they earned, i.e., "A", "B", "C", "D", or "F". The calculation for overall grades in the course can be found in the course syllabus. Include your source code for this function in your demo write-up, ideally in a \begin{lstlisting} ... \end{lstlisting} source code block.

2. State a property about calculate_grade that implies its correctness and formally prove that the property holds of your implementation. Your property must universally quantify over at least three of the parameters to calculate_grade. Otherwise, you are free to state any property of calculate_grade that could reasonably imply that your implementation is correct.

Problem 2: What's Wrong?

Consider the following erroneous implementation of a map_add(n, l) function which ought to add n to every element of a list of numbers l.

def cons(x, l):
    return [x, *l]

define map_add(n, l):
    match l:
        case []:
            return []
        case [head, *tail]
            return map_add(n, tail)

Part 1: Debug

In a sentence or two, describe what is wrong with this implementation.

Part 2: Debunk

Consider the following erroneous "proof" of the correctness of map_add.

Analyze the proof and in a sentence or two describe the error in the proof that allows the proof to go through.

Part 3: Deal With

Finally, replicate the proof, fixing the error identified in the previous step, and attempt to carry the proof to completion. Describe in a sentence or two where you get "stuck" in the proof and cannot proceed forward.

Problem 3: Zero Is The Hero

Part 1: Implement

Implement a recursive Python function dropzeroes(l) that takes a list l of numbers as input and returns l but with all 0s. For example dropzeroes([1, 3, 0, 1, 0, 2]) -->* [1, 3, 1, 2]. Make sure to test your code in Python and add your code to this write-up using a code block.

Part 2: Prove

Prove the following property of dropzeroes:

(Hint: be precise with your program derivations and every step you make! In particular, make sure that every step is justified, and you consider all possibilities of evaluation.)

Preconditions and Proof States

With quantified variables, we can write rich equality propositions over functions. However, there is an essential detail in our claims that we have glossed over until now. Recall our list_append claim from the previous readings:

We snuck under the radar that we assumed that l1 and l2 were lists! This fact is essential because Python is happy to let us call our functions with any values that we want. The only caveat is that we may not like the results!

>>> list_append("banana", 7)
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
  File "<stdin>", line 5, in list_append
  File "<stdin>", line 5, in list_append
  File "<stdin>", line 5, in list_append
  [Previous line repeated 3 more times]
TypeError: Value after * must be an iterable, not int

Sometimes we might get lucky and get a runtime error indicating that our assumption was violated. However, in other cases, we aren't so lucky:

>>> list_append([], "wrong")
'wrong'

Here we feed list_append a string for its second argument. Recall that list_append performs case analysis on its first argument. When that first argument is empty, then the second argument is returned immediately. So even though the second argument had an incorrect type, the function still "works."

Nothing stops the user of list_append from passing inappropriate arguments. list_append assumes that the arguments passed obey specific properties, in this particular case, that the arguments are lists. These assumptions are integral to the correct behavior of the function. Consequently, when we analyze a program, we will also need to track and utilize these assumptions in our reasoning. This realization will lead us to a formal definition of proof that will guide our remaining study of the foundation of mathematics.

Review: Preconditions and Postconditions

In CSC 151, we captured assumptions about our functions' requirements and behavior as preconditions and postconditions.

Preconditions and post-conditions form a contract between the caller of the function and the function itself, also called the callee. The caller agrees to fulfill the preconditions of the function. In return, the callee fulfills its post-conditions under the assumption that the preconditions have been fulfilled.

Preconditions and post-conditions are an integral aspect of program design. They formalize the notion that while a function, in theory, can guard against every possible erroneous input, it is impractical to do so. For example, recall that mergesort relies on a helper function merge that takes two lists and combines them into a single sorted list:

def merge(l1, l2):
    '''merge(l1, l2) merges lists l1 and l2 into a sorted list.'''
    # ...
    pass

The post-condition of merge is that the list it returns is sorted, i.e., using our language of propositions:

is_sorted is a custom function that takes a list l as input and returns True if and only if l is sorted.

However, what preconditions do we place upon the inputs, l1 and l2?

• l1 and l2 must both be lists.
• The elements of l1 and l2 must all be comparable to each other (presumably with the (<) operator).
• l1 and l2 must be sorted.

If the implementor of merge was paranoid, they might consider implementing explicit checks for these three preconditions. However, imagine what these checks might look like in code. All the checks require that we either:

1. Scan the lists l1 and l2 multiple times, once for each precondition we wish to check.
2. Integrate all three checks into the merging behavior of the function.

The former option is modular---we can write one helper function per check---but inefficient. The latter option is more efficient but highly invasive to the merge function and leads to an unreadable implementation.

Both options are undesirable. This fact is why we usually choose a third option: make the preconditions documented assumptions about the inputs of the function.

Preconditions as Assumptions During Proof

When we reason about concrete propositions, preconditions are unnecessary because we work with actual values. However, with abstract propositions, preconditions become assumptions about (universally quantified) variables.

We initially obtain these assumptions as part of the proposition we are verifying. For example, in our list_append claim:

The text "for any lists …" introduces the precondition that l1 and l2 are lists.

As another example, consider the post-condition of merge now realized as a proposition:

In addition to the assumptions we have about the type of the variables, we can also have arbitrary properties about these variables.

Our claim is of the form "if … then …" where the preconditions sit between the "if" and "then" We assume these preconditions and then go on to prove the claim which follows the "then." In this example, the additional preconditions are that:

• is_sorted(l1) ≡ True
• is_sorted(l2) ≡ True

And then the claim we prove with these assumptions is:

• is_sorted(merge(l1, l2)).

Short-hand for Propositions Involving Booleans

As we discuss preconditions throughout this reading and beyond, we will frequently work with preconditions that assert an equivalence between two expressions of boolean type. For example, to state the proposition that x is less than y, we would declare that it is equivalent to True:

• x < y ≡ True

This notation is quite taxing to write where we have many preconditions in our reasoning. Instead, we'll use shorthand, taking advantage of the similarities between boolean expressions and propositions. When we write the following proposition:

• x < y

We really mean the complete equivalence x < y ≡ True. With this notation, we can rewrite the above claim above more elegantly as:

def index_of(x, l):
    '''Returns the (0-based) index of element x in list l'''
    # ...
    pass

Tracking and Utilizing Assumptions

Assumptions about our variables initially come from preconditions we write into our claims. How do we use these assumptions in our proofs of program correctness? It turns out we have been doing this already without realizing it!

For example, in our analysis of the boolean my_and function from our previous reading, we said the following:

Because b is a boolean, either b is True or b is False.

This line of reason is only correct because we assumed via a precondition:

That b is indeed a boolean. If we did not have such a precondition, this line of reasoning would be invalid!

When we have an assumption that asserts the type of a universally quantified variable, we can use that assumption to conclude that the variable is of a particular shape according to that type. For example:

• A variable that is a natural number is zero or a positive integer.
• A variable that is a function is bound to a lambda value, e.g., (lambda (n) (+ n 1)).
• A variable that is a boolean is either #t or #f.

Furthermore, if an operation requires a value of a particular type as a precondition, a type assumption about a variable allows us to conclude that the variable fulfills that precondition. For example, if we know that x is a number then we know that x > 3 will produce a boolean result instead of potentially throwing an error.

Utilizing General Assumptions

Besides type assumptions, we can also assert general properties about our variables as preconditions. In our merge example, we assumed that the input lists satisfied the is_sorted predicate, i.e., were sorted. We can then use this fact to deduce other properties of our lists that will help us ascertain correctness, e.g., that the smallest elements of each list are at the front.

Because these properties are general, we have to reason about them in a context-specific manner. Let's look at a simple example of reasoning about one common kind of assumption: numeric constraints. Consider the following simple numeric function:

def double(n):
    return n * 2

And suppose we want to prove the following claim about this function:

Employing our symbolic techniques, we first assume that n is an arbitrary number. However, the claim that follows the quantification of n includes a precondition---it is of the form "if … then … ". Therefore, in addition to n, we also gain the assumption that n > 0, i.e., n is positive.

When we go prove that double(n) > 0, we know from our model of computation that:

double(n) > 0 --> n * 2 > 0

This resulting expression is not always true. In particular, if n is non-negative, then n * 2 will be negative and thus less than 0. However, our assumption that n > 0) tells us this is not the case!

Here is a complete proof of the claim that employs this observation.

double(n) > 0 --> n * 2 > 0.

Being Explicit When Invoking Assumptions

In the above proof, I was explicit about:

1. When I used an assumption in a step of reasoning, and
2. How I used that assumption to infer new information.

At this stage of your development as a mathematician, you should do the same for any other assumption you employ in a proof. As an example of what not to do, here is the same proof but without the explicit call-out of the assumption:

double(n) > 0 --> n * 2 > 0.

This proof is valid. The steps presented and the conclusion are sound. However, this is a less formal proof because it has left some steps of reasoning implicit. In this course, we aim for rigorous, formal proof, and so we should not leave any steps implicit in our reasoning.

That being said, we will quickly find that dogmatically following this guidance will lead us to ruin. Analogous to programming, if we write our proofs at too low of a level, we will get lost in the weeds with low-level details and lose sight of the bigger picture.

For now, let's be ultra-explicit about our reasoning and follow the formula above whenever we invoke an assumption. However, because reasoning about type constraints, e.g., happens so frequently, it is okay if you elide when you use a type assumption in your proofs. For example, instead of saying:

By our assumptions, we know b is a boolean. Therefore, b must either be True or False.

You can, instead, say:

b is either True or False.

However, you should still be clear when you are assuming the type of a variable using a "let"-style statement, e.g.,

Let b be a boolean.

Assumptions that Arise During Analysis

Assumptions arise not only when we initially process our claim. We also gain new assumptions during the proving process. For example, let's consider the following simple function:

def nat_sub(x, y):
    if x < y:
        return 0
    else:
        return x - y

And the following claim about this function:

Here is a partial proof of this claim:

    nat_sub(x, y)
--> { if x < y: return 0 else: return x - y }

But now, we're stuck! We need to evaluate the guard to proceed, but we don't know how the expression x < y will evaluate. However, we do know the following:

• x and y are numbers.
• x < y will produce a result because x and y are numbers.
• The result of x < y is either True or False because the expression has boolean type.

Because of this, we can proceed by case analysis on the result of x < y: it evaluates to either True or False. Let us consider each case in turn:

Here, we seem to be stuck again. We don't know how to proceed with the subtraction since x and y are held abstract. However, we must remember that in this case, we are assuming that x < y is False. Therefore, we know that x is greater than or equal to y. Because we know the difference between a larger number and a smaller number is positive, we can conclude that x - y <= 0 as desired.

Let's see this reasoning together in a complete proof of our claim.

    nat_sub(x, y)
--> { if x < y: return 0 else: return x - y }

In summary, we can obtain assumptions from places other than our claims, e.g., through case analysis or the post-condition of an applied function. We can then use these newly acquired facts to complete our proofs.

if x < 0:
    return e1
elif x <= 3:
    return e2
elif x == 5:
    return e3
elif x <= 8:
    return e4
else
    return e5

For each branch expressions e1 through e5 above, describe the assumptions about x you can make by entering that branch of the cond.

(Hint: make sure you account for the fact that to reach a branch, all the previous branches must have returned false.)

Proof States and Proving

In summary, we have introduced assumptions into our proofs of program correctness. These assumptions come from preconditions or through analysis of our code. We use these assumptions to prove our claim. Because our claim evolves throughout the proof, e.g., it is more accurate to say that we use assumptions to prove a goal proposition where the initial goal proposition is our original claim.

Surprisingly, it turns out that all mathematical proofs can be thought of in these terms!

When either reading or writing a mathematical proof, we should keep these definitions in mind. In particular, we have to be aware at every point of the proof:

• What is our set of assumptions?
• What are we trying to prove?

def calculate_price(day_of_week, age, is_park_hopper):
    return 115 + \
           -5 if age < 10 else 0 + \
           14 if is_friday_or_weekend(day_of_week) else 0 + \
           65 if is_park_hopper else 0

Assumptions in proofs

Shorthand for Program Derivations

Most of the functions we will encounter from this point forward are simple conditionals, but our mental model can be quite verbose in these situations. Consider the following toy function:

def f(x):
    if 0 < x + 2:
        return "hello"
    else:
        return "goodbye"

For example, in our model, the function call f(1) evaluates as follows:

--> f(1)
--> { if 0 < 1 + 2:
         return "hello"
      else:
         return "goodbye" }
--> { if 0 < 3
         return "hello"
      else:
         return "goodbye" }
--> { if True
         return "hello"
      else:
         return "goodbye" }
-->  { return "hello" }
--> "hello"

While precise, these steps will obscure the broader argument we are trying to make for our program.

To make our program derivations more readable, we will use shorthand for this lab when evaluating function calls:

You are free to evaluate a function call directly to the returned expression that ultimately executed by the function.

If the statement-expression above came about from a function call, say f(1), we would write the evaluation of that call as:

     f(1) 
-->* "hello"

Skipping over the explicit execution of the statement-expression that the function call evaluates to in our model. We use the notation -->* (LaTeX: \longrightarrow^*, Unicode: ⟶*) to mean that multiple evaluation steps happened between the two lines of the derivation.

Be aware that whenever we skip steps, we introduce the possibility of making an error in our reasoning! So double-check your work whenever you skip steps in this manner!

Problem: Narrowing Down the Possibilities

Consider the following Python functions:

def f1(name):
    if name == "Alice":
        return 0            # Point A
    elif name == "Bob":
        return 1            # Point B
    elif name == "Carol":
        return 2            # Point C
    elif name != "Daniel":
        return 3            # Point D
    elif name != "Emily":
        return 4            # Point E

def f2(x, y):
    if y >= 1:
        return 0            # Point A
    elif x >= 1: 
        return 1            # Point B
    elif x == -1:
        return 2            # Point C
    elif x <= -5 or y >= 3:
        return 3            # Point D
    elif x == 0:
        return 4            # Point E
    elif x == y:
        return 5            # Point F

For each of the functions:

1. Identify the types of each of the parameters
2. Describe the set of assumptions we know are true about the parameters inside each branch at each labeled point, i.e., when that branch's guard is True.
3. Are each of the conditionals exhaustive? If not, describe what values are not covered by the if-else statements.

Problem: Capture

Consider the following Python function that computes a report for a student given their current grades in a course:

def report(hw_avg, quiz1, quiz2, quiz3):
    if hw_avg > 90 and quiz1 > 90 and quiz2 > 90 and quiz3 > 90:
        return "excelling"
    elif: hw_avg > 75 and quiz1 <= quiz2 and quiz2 <= quiz3:
        return "progressing"
    elif: hw_avg < 60 or quiz1 < 60 or quiz2 < 60 or quiz3 < 60:
        return "needs help"
    else:
        return "just fine"

1. Describe the preconditions (both in terms of types and general constraints) on the parameters.
2. Describe the conditions under which report(hw_avg, quiz1, quiz2, quiz3) will return "just fine". Describe them in terms of properties that ought to hold on each parameter to the function.
3. Are there any conditions under which the function reports an inappropriate string, given the arguments and your interpretation of the function's intended behavior?

Problem: Looking Ahead

In this problem, we'll motivate our discussion for next period on recursion and induction. Consider the standard append function for lists.

# Our standard list helper functions...
def is_empty(l):
    return len(l) == 0

def head(l):
    return l[0]

def tail(l):
    return l[1:]

def cons(x, l):
    return [x, *l]

def append(l1, l2):
    if is_empty(l1):
        return l2
    else:
        return cons(head(l1), append(tail(l1), l2))

Part 1: Simple Reasoning About Append

While the function is recursive, our substitutive model of computation is capable of modeling the behavior of this function. Thus, we can prove properties about append just like any other function. Prove this one as an exercise:

Part 2: (Not) Commutativity

We say that an operation is commutative if we can swap the order of the objects involved, i.e., if x ≡ y then y ≡ x and vice versa. This is true for some operations, e.g., integers and addition, but not other, e.g., integers and subtraction. It turns out that append is not commutative for lists! Prove this fact by way of a counterexample:

Part 3: A Humble Attempt

Because append is not commutative, this means that just because the empty list is an identity on the left-hand side of the function, it is not necessarily an identity on the right-hand side. With a little bit of thought, though, we can convince ourselves this ought to be the case. However, proving this fact is deceptively difficult! Attempt to prove this claim:

(Hint: you can perform case analysis on each new list you encounter in your proof, even the tail of the original list!)

At some point, you will get stuck, ideally at a point where you start seeing that your reasoning will go on infinitely. Check with an instructor that you have indeed gotten stuck at the "right point."

Part 4: Reflection

Finally, reflect on your experience. Answering the following questions in a few sentences each:

• Why were you able to directly prove the left-identity claim?
• Why is the right-identity claim more difficult to prove?
• What information do you need in order to break the chain of infinite reason that you found in the previous proof?

Inductive Reasoning

Review of Recursive Design

The workhorse of functional programming is recursion. Recursion allows us to perform repetitive behavior by defining an operation in terms of a smaller version of itself. However, recursion is not just something you learn in Racket and summarily forget about for the rest of your career. Recursion is pervasive everywhere in computer science, especially in algorithmic design.

Because of this, we must know how to reason about recursive programs. Our model of computation is robust enough to trace the execution of recursive programs. However, our formal reasoning tools fall short in letting us prove properties of these programs. We introduce induction one of the foundational reasoning principles in mathematics and computer science, to account for this disparity.

A Review of Lists

Lists are a common data structure found in most modern programming languages. Python is no exception!

Like numbers, there are an infinite number of possible lists, e.g.,

• []
• [3, 5, 8]
• ["Hi", "goodbye", "!"]
• [1, 2, 3, 4, 5, 6, 7, 8, 9, 10].

However, our recursive definition of a list categorizes these infinite possibilities into a finite set of cases.

This definition is similar to that of a boolean, where we define a boolean as one of two possible values: True or False. However, the definition of a list is recursive because the non-empty case includes a component that is also a list.

Accessing Lists Recursively

In Python, we typically operate over lists much like an array with indexing operations and mutation. However, we can easily write functions that allow us to operate on lists according to our recursive definition, similarly to Scheme.

def is_empty(l):
    '''is_empty(l) returns true if list l is empty'''
    return len(l) == 0

def head(l):
    '''head(l) returns the element at the front of (non-empty) list l'''
    return l[0]

def tail(l):
    '''tail(l) returns (non-empty) list l, but without its head element'''
    return l[1:]

The implementation of the tail function, in particular, takes advantage of Python's list slicing expressions. l[n:m] returns a list containing the elements of l starting at index n, ending at index m (exclusive). When we elide m in a list slice, m becomes len(l), i.e., the last index of the list.

We can create lists explicitly with list literal notation, e.g., [1, 2, 3, 4, 5]. Additionally, we can write a "cons" function:

def cons(x, l):
    '''cons(x, l) returns list l but with element x at the front'''
    return [x, *l]

That allows us to add an element to the front of a list. The implementation of cons uses Python's sequence unpacking expression where *l takes the elements of list l and, effectively, injects them into a context where a sequence is expected. Here, the elements of l become the remaining elements of the list literal that cons returns.

Recursive Design with Lists

Because lists are defined via a finite set of cases, we define operations over lists using a combination of the is_empty function to determine which kind of list we have and head and tail to access parts of the list. For some simple operations, this is enough to get by, e.g., a function that retrieves the second element of a list:

def second(l):
    if is_empty(l):
        raise ValueError('empty list given')
    elif is_empty(tail(l)):
        raise ValueError('singleton list given')
    else:
        return head(tail(l))

We can translate this code to a high-level description:

• If the list is empty, throw an error (via Python's raise statement).
• If the list contains one element, throw an error.
• If the list has at least two elements, retrieve the second element.

However, mere case analysis doesn't allow us to write more complex behavior. Consider the prototypical example of a recursive function: computing the length of a list. Let's first consider a high-level recursive design of the operation of this function, call it length(l). Because a list is either empty or non-empty, this leads to straightforward case analysis. The empty case is straightforward:

• If the list is empty, its length is 0.

However, in the non-empty case, it isn't immediately clear how we should proceed. We can draw the non-empty case of a list l with head element v and tail tl as follows:

l = [v][ ?? tl ?? ]

Besides knowing that tl is a list, we don't know anything about it---it is an arbitrary list. So how can we compute the length of l in this case? We proceed by decomposing the length according to the parts of the lists we can access:

length =  1 + length t
l      = [h][ ?? t ?? ]

We know that the head element h contributes 1 to the overall length of l. How much does the tail of the list t contribute? Since t is, itself, a list, t contributes whatever length(t) produces. But this is a call to the same function that we are defining, albeit with a smaller list than the original input!

Critically, as long as the call to length(t) works, the overall design of length is correct. This assumption that we make---that the recursive call "just works" as long as it is passed a "smaller" input---is called the recursive assumption, and it is the distinguishing feature of recursion compared to simple case analysis.

In summary, we define length recursively as follows:

The length of a list l is:

• 0 if l is empty.
• 1 plus the length of the tail of l if l is non-empty.

In the recursive case of the definition, our recursive assumption allows us to conclude that the "length of the tail of l" is well-defined.

Our high-level recursive design of length admits a direct translation into Racket using our list functions:

def length(l):
    if is_empty(l):
        return 0
    else:
        return 1 + length(tail(l))

Because the translation is immediate from the high-level recursive design, we can be confident our function is correct provided that the design is correct.

Pattern Matching with Lists

Recall that one of our design goals is to write programs that are correct from inspection. In particular, when we have a recursive design, we want our code to look like that design. Let's see how our recursive definition of length fares in this respect. Below, we have replicated the definition of length with the recursive design in-lined in comments:

def length(l):
    if is_empty(l):             # A list is either empty or non-empty.
        return 0                # + The empty list has zero length.
    else:                       # + A non-empty list has...
        hd = head(l)            #     - A head element hd and
        tl = tail(l)            #     - A tail element tl.
        return 1 + length(tl)   #   The length of a non-empty list is
                                #   plus the length of the tail.

In this version of the code, we explicitly bind the head and tail of l to be clear where these components of l are manipulated.

Overall, this isn't too bad! Like our design, the code is clearly conditioned on whether l is empty or non-empty. Furthermore, the results of the cases clearly implement the cases of our design, so we can believe our implementation is correct as long as we believe our design is correct.

Is there anything we can improve here? Yes—some subtle, yet important things, in fact:

• We need to make sure that the guard of our conditional accurately reflects the cases of our data structure. Here, our list is either empty or non-empty which is captured by an is_empty check.
• We know that in the recursive case that our non-empty list is made up of a head and tail which we need to manually access using head and tail, respectively. We locally bind names to these individual pieces so that we don't interchange head and tail calls in our code, but these bindings add additional complexity to our implementation.

To fix these issues, we'll use the pattern matching facilities of Python to express our recursive design directly without the need for a guard expression or let-binding. Note that when we talk about pattern matching here, we don't mean regular expression matching but instead a separate facilities of Python for writing code that looks at the shape of a data type.

First, we'll revise our list definition slightly based on the functions we use to construct lists.

A list is either:

• [], the empty list.
• cons(v, l), a non-empty list constructed that consists of a head element v and a list l.

Remember, in this recursive scheme, a list is ultimately composed of repeated cons calls ending in []. For example:

>>> [1, 2, 3, 4, 5]
[1, 2, 3, 4, 5]
> cons(1, cons(2, cons(3, cons(4, cons(5, []))))) 
[1, 2, 3, 4, 5]

Because of this, we know that our constructive definition of a list covers all possible lists. Now, we'll use pattern matching to directly express length in terms of this constructive definition:

def length(l):
    match l:
        case []:
            return 0
        case [hd, *tl]:
            return 1 + length(tl)

This version of length behaves identically to the previous version of the code but is more concise, directly reflecting our constructive definition of a list.

The pattern matching statement in Python allows us to directly perform a case analysis on data:

1. After the match keyword is the scrutinee or subject of the pattern match, l.
2. Following the scrutinee are branches, each one corresponding to a particular shape of the data we're analyzing.
   • Following the case keyword is a pattern, a particular value shape that the scrutinee must match in order for this branch to be selected.
   • On the next line after each case is the body of the pattern match that is evaluated when the scrutinee matches the branch's pattern.

Importantly, patterns may contain variables that are bound to parts of the scrutinee on a successful match. The first pattern, the empty list [], does not contain any such variables. But the second pattern, a list literal pattern combined with an unpacking operator, binds the first element of the list to hd and the tail of the list to tl. By using pattern matching, we no longer need to bind locals to name the subcomponents of a list!

A Recursive Skeleton for Lists

Ultimately, the recursive design of a function contains two parts:

• Case analysis over a recursively-defined structure.
• A recursive assumption allowing us to use the function recursively on a smaller object than the input.

When we fix the structure, e.g., lists, we arrive at a skeleton or template for defining recursive functions that operate on that structure. This skeleton serves as a starting point for our recursive designs. The skeleton always mimics the recursive definition of the structure:

Note that this skeleton is only a starting point in our recursive design. We may need to generalize or expand the skeleton, e.g., by adding additional base cases depending on the problem.

>>> list_intersperse(0, [1, 2, 3, 4, 5])
[1, 0, 2, 0, 3, 0, 4, 0, 5]
>>> list_intersperse(0, [])
[]
>>> list_intersperse(0, [1])
[1]

Inductive Reasoning with Lists

Now that we've discussed how we write recursive programs over lists, we'll develop our primary technique for reasoning about recursive structures, structural induction.

Reasoning About Recursive Functions

Let's come back to the proposition about append that we used to start our discussion of program correctness:

To prove this claim, we need the definitions of both length and append.

def length(l)
    match l:
        case []:
            return 0
        case [head, *tail]:
            return 1 + length(tail)

def append(l1, l2):
    match l1:
        case []:
            return l2
        case [head, *tail]:
            return cons(head, append(tail))

The proof proceeds similarly to all of our symbolic proofs so far: assume arbitrary values for the universally quantified variables and attempt to use symbolic evaluation.

    length(l1) + length(l2)
--> { match l1:
          case []:
              return 0
          case [head, *tail]:
              return 1 + length(tail) } + length(l2)

    length(append(l1, l2))
--> length({ match l1:
                 case []:
                     return l2
                 case [head, *tail]:
                     return cons(head, append(tail, l2)) })

At this point, both sides of the equivalence are stuck. However, we know that because l1 is a list, it is either empty or non-empty. Therefore, we can proceed with a case analysis of this fact!

So the empty case works out just fine. What about the non-empty case?

Note that this evaluation is a bit trickier than the previous ones that we have seen. In particular, we have to observe that the tail of cons(x, y) is simply y! Nevertheless, if we push through accurately, we can persevere!

At this point, our equivalence in the non-empty case is:

1 + length(tail) + length(l2) ≡ 1 + length(append(tail, l2))

tail is still abstract, so we can't proceed further. One way to proceed is to note that tail itself is a list. Therefore, we can perform case analysis on it---is tail empty or non-empty?

Note that when tail is empty, the original list l1 only contains a single element. Therefore, it should not be surprising that the equivalence boils down to demonstrating that both sides evaluates to 1 + length(l2).

Again, while the empty case works out, the non-empty case runs into problems.

tail2 here is the tail of tail, i.e., tail(tail(l1))!

Notice a pattern yet? Here is where our case analyses have taken the left-hand side of the equivalence so far:

     length(l1) + length(l2)
-->* <... l1 is non-empty ...>
-->* 1 + length(tail) + length(l2)
-->* <... tail of l1 is non-empty ...>
-->* 1 + 1 + length(tail2) + length(l2)

We could now proceed with case analysis on tail2. We'll find that the base/empty case is provable because in that case, we assume that l1 has exactly two elements. But then, we'll end up in the same situation we are in, but with one additional (+ 1 ... at the front of the expression! Because the inductive structure is defined in terms of itself, and we are proving this property over all possible lists, we don't know when to stop our case analysis!

1 + 1 + length(append(tail2, l2))

Inductive Reasoning

How do we break this seemingly infinite chain of reasoning? We employ an inductive assumption similar to the recursive assumption we use to design recursive functions. The recursive assumption is that our function "just works" for the tail of the list. Our inductive assumption states that our original claim holds for the tail of the list!

Recall that our original claim stated:

Our inductive assumption is precisely the original claim but specialized to the tail of the list that we perform case analysis over. We also call this inductive assumption our inductive hypothesis.

While we are trying to prove the claim, the inductive hypothesis is an assumption we can use in our proof.

Let's unwind our proof back to the case analysis of l1. The case where l1 was empty was provable without this inductive hypothesis, so let's focus on the non-empty case. Recall that before we performed case analysis, we arrived at a proof state where our goal equivalence to prove was:

1 + length(tail) + length(l2) ≡ 1 + length(append(tail, l2))

Compare this goal equivalence with our induction hypothesis above. We see that the left-hand side of the induction hypothesis equivalence, length(tail) + length(l2), is contained in the left-hand side of the goal equivalence. Because our induction hypothesis states that this expression is equivalent to length(append(tail, l2)), we can rewrite the former expression to the latter expression in our goal! This fact allows us to finish the proof as follows:

We call a proof that uses an induction hypothesis a proof by induction or inductive proof. Like recursion in programming, inductive proofs are pervasive in mathematics.

In summary, here is a complete inductive proof of the append claim. In this proof, we'll step directly from a call to length or append directly to the branch of the match that we would have selected. We'll take this evaluation shortcut moving forward to avoid cluttering our proof.

Note in our proof that we declare that we "proceed by induction on l1" and then move into a case analysis. This exemplifies how we should think of inductive proof moving forward:

Recursion to Induction

Now we'll gain first-hand experience proving properties of our recursive designs.

Problem 1: The Structure of Inductive Proof

We use inductive reasoning to prove properties of programs involving recursion. In this problem, we'll incrementally develop all the pieces of an inductive proof concerning the append function over lists:

def cons(x, l):
    return [x, *l]

def append(l1, l2):
    match l1:
        case []:
            return l2
        case [head, *tail]:
            return cons(head, append(tail, l2))

In the reading, we explored these two claims regarding append:

You noted that the right-null-append claim requires more proof machinery than just symbolic execution. We need induction to prove it! Like recursion, inductive proof also has a skeleton we can use as a starting point in understanding this technique. Below is our inductive proof skeleton for claims involving lists with places you should fill in indicated with italicized parentheses: (FILL ME IN!).

Some notes about this skeleton:

• Because induction is ultimately a case analysis, we must do induction on some object and thus must explicitly identify it. In our case, this is a list, but generally speaking, we can perform induction on any inductively-defined object that we can get our hands on.

• The proof of the base case, when the list is empty, is usually straightforward. We know the list is empty, so we typically evaluate the goal equivalences to final values and observe that they are identical.

• In the inductive case, we explicitly name (a) the induction hypothesis and (b) the proof goal. We do as a point of presentation---we want to be clear what we are assuming in our induction hypothesis and how that differs from the proof goal. Recall that the induction hypothesis is the original claim but specialized to the tail of the list we are performing induction over.

• Finally, in the inductive case, we will likely need to use our induction hypothesis. Like other assumptions, we should be explicit in our prose when we invoke and how we use it to update our proof state.

  Use this skeleton to author a proof of the right-null-append claim.

Problem 2: On Your Own

Consider the following Python function:

def any(f, l):
    match l:
        case []:
            return False
        case [head, *tail]:
            if f(head):
                return True
            else:
                return any(f, tail)

For the following claim, write a formal proof of the claim.

Mathematical Induction

So far, we have applied induction exclusively to lists. However, are there other structures that are inductive? It turns out that the natural numbers are the most common structure to perform induction over in mathematics. Now that we have some experience with inductive proof, let's explore this foundational application of the technique in detail.

The Natural Numbers

Recall that we can apply induction to any inductively-defined structure, that is, a structure defined in terms of a finite set of (potentially recursively-defined) cases. How can we define the natural numbers, i.e., non-negative integers, in this manner? One natural choice is to start at zero, the smallest natural number, and work our way up.

Since it is the smallest natural number, zero seems to serve as a base case, similar to the empty list. However, how can we characterize a non-zero natural number in terms of another natural number? Consider the number seven, written in unary, i.e., tally marks:

 1111111
\_______/
    |
    7

Do we see a smaller natural number nested somewhere inside of seven? The unary representation makes this explicit:

 1   111111
    \______/
        |
        6

Seven can be thought of as six but with one extra mark! In general, any non-zero natural number $k$ is one more than $k-1$. This fact leads to the following definition of the natural number as an inductive structure:

With lists, we can use list functions list to query and break apart the structure:

• is_empty allows us to test if a list is empty.
• head lets us extract the head of an empty list.
• tail lets us extract the tail of an empty list.
• cons lets us construct a list from a head and tail.

We do the same thing with natural numbers, albeit with functions that you have seen before but may not have thought of in this context:

• (==) allows us to test if a natural number is zero.
• (-) allows us to retrieve the smaller natural number from a larger one.
• (+) allows us to build up larger natural numbers from smaller ones.

Induction Over the Natural Numbers

Now that we have an inductive definition of the natural numbers, we can:

1. Perform recursive operations over the natural numbers, and
2. Prove properties involving natural numbers by using inductive reasoning.

Of course, not having a formal inductive definition didn't stop us from writing recursive functions over the natural numbers. Similarly, with lists, having this definition in-hand can give us more confidence that we are doing the right thing when we begin programming.

With that being said, let us focus on the second activity for the remainder of this section: writing inductive proofs with natural numbers. Induction over the natural numbers is so common that we give it a generic name: mathematical induction. Consider the following canonical recursive function over the natural numbers:

def factorial(n):
    if n == 0:
        return 1
    else
        return n * factorial(n-1)

And the following claim about factorial asserts that factorial produces only positive, non-negative, non-zero results.

Note that the definition of factorial reflects the structure of the inductive definition of a natural number. This strongly suggests that we ought to prove this claim using induction. Let's go ahead and try it, following the same style of proof introduced for lists, but instead invoking the inductive definition of natural numbers.

The case analysis of our inductive is similar to that of lists. The "base case" for a natural number is when that number is zero. The "inductive case" for a natural number is when that number is non-zero. Note that because a natural number cannot be negative and the inductive case number is not zero, this number must be a positive integer. If we call that natural number k, then we know that k-1 is well-defined (since k is at least 1).

The proof of the base case follows from evaluation:

The proof of the recursive case also follows from evaluation, invoking the induction hypothesis, and collecting assumed constraints about the different pieces of the inequality.

Note that in the inductive case, we acquire the following assumptions:

• n is non-zero because we are in the inductive case.
• 0 < factorial(n-1) from our induction hypothesis.

These two facts combined with the knowledge that two multiplying two positive numbers produces a positive number tell us that the body of factorial produces a strictly positive result.

def sum(n)
    if n == 0:
        return 0
    else:
        return n + sum(n-1)

Structural Versus Mathematical Induction

Now, we have two objects that can be the subject of induction: lists and numbers. In some situations, we might have both types available as candidate subjects of inductive analysis. Does it matter which one that we pick? Naturally, it depends on the operation we are analyzing! However, here are some general considerations when choosing one kind of induction over the other:

You can only perform induction on things you have

For example, let's consider the function replicate(n, v) which produces a list of n copies of v. And consider the following claim about this function:

Since our claim is ultimately about the length of a list and replicate produces a list, it is tempting to say that we will prove this claim by induction on a list. However, note that our assumptions don't give us a list! As part of quantifying our variables, we assume the existence of some natural number n and a value (of arbitrary type) v. We do not have an actual list to perform induction over.

Perform induction on the object your function performs case analysis over

In other cases, we have multiple objects, say, for example, a natural number and a list, available to us. Which one should we perform induction over? We should likely perform induction on the object that our function is performing case analysis over. That way, the cases allow us to make progress in evaluating the function call.

For example, consider the function list_inc(l, n), which increments every element of l by n. Both l and n are inductively defined. However, the implementation of list_inc:

def list_inc(l, n):
    match l:
        case []:
            return []
        case [head, *tail]:
            return cons(n+head, list_inc(tail, n))

Relies on a case analysis on l, not n! Thus, it is likely that we should analyze the function by structural induction on l rather than mathematical induction on n.

That being said, mathematical induction can be applied in any context where we have access to a natural number, even if it is not part of the immediate goal. For example, consider a claim over lists we've seen previously:

While there is no natural number variable introduced by the claim, we do have access to one number: length(l) produces a natural number since l is assumed to be a list! In other words, we could try to proceed by induction on the length of l rather than its structure.

It turns out that the proof works out, but our reasoning is a lot more complicated!

• We have to continually conclude that the input list l is either empty or non-empty from its length. Note that we shouldn't assume this fact is true---we ought to prove it true as an auxiliary claim or lemma.
• Our induction hypothesis is far more complicated to state and utilize. We'll talk more about the specifics of what it says when we discuss logic in detail. But intuitively, the induction hypothesis says that our original claim holds for a list that has length one less than the original list. Because we assume that the induction hypothesis is true, we get to choose an instantiation for l1 that benefits our reasoning, here the tail of the list.

In short, when we can perform structural induction on an object, we can frequently figure out a way to also perform mathematical induction on that same object, e.g., through some notion of "length." However, when possible, we should use structural induction because it allows us to work directly with the object's definition rather than indirectly through that "length."

Mathematical Induction Beyond Program Correctness

As a final note, mathematical induction also serves as a bridge between our current focus on program correctness and the wider world of formal mathematics. We can perform induction on natural numbers that appear at the level of mathematics, not just programs! The mechanics are identical, although the domain of proof may be different, something we'll discuss in the coming weeks. We close by highlighting how we can directly translate our proof of the positivity fact for factorial-the-Racket-function to factorial-the-math-function.

First, we define factorial in mathematical notation as follows:

$$\begin{array}{rl}0!=& 1\\ n!=& n\times (n-1)!\end{array}$$

And then we can state and prove our positivity claim as follows:

Compare the proof of positive for factorial versus $n!$ and note how they are identical save for the fact that we use program simplification for factorial and arithmetic for $n!$. Notably, while the domains---programs versus arithmetic---are different, the proof technique---mathematical induction---remains the same!

Mathematical Induction Practice

Now, we'll practice writing inductive proofs, but this time, over the natural numbers. We'll also begin to test our understanding of proof mechanics by exploring incorrect proofs of correct propositions. As we shall see, writing proofs is one thing, but identifying where proofs go wrong is quite tricky!

Problem 1: Mathematical Induction Practice

Consider the following Python definitions:

def cons(x, l):
    return [x, *l]

def length(l):
    match l:
        case []:
            return 0
        case [_, *tail]:
            return 1 + length(tail)

def replicate(v, n):
    if n == 0:
        return []
    else:
        return cons(v, replicate(v, n-1))

Prove the following claim using mathematical induction.

Problem 2: More Mathematical Induction Practice

Consider the following claim regarding the distribution of powers and multiplication.

Prove this claim by mathematical induction on $n$. In your proof, you may only rely on the following mathematical facts:

• For any numbers $x$ and $n$, $x\cdot x^{n-1}=x^n$
• Commutativity of multiplication: for any numbers $x$ and $y$, $xy=yx$.
• Associativity of multiplication: for any numbers $x$, $y$, and $z$, $x(yz)=(xy)z$.

Problem 3: Problem Proof

Here is a bogus claim about replicate and a corresponding "proof" of that claim:

1. In a sentence or two, describe what the claim is saying and why it is incorrect.
2. In a sentence or two, describe the error in the "proof."
3. Correct the error and attempt to finish the proof. You should get stuck, i.e., a point where you are unable to move further in the proof. Show your work to get to this point and describe in a sentence or two why you cannot proceed forward with the proof.

Problem 4: Even More Mathematical Induction Practice

We can formally define the $i$th odd number to be $d_i=2i-1$ (where $d_1$ is the first odd number: $d_1=2\cdot 1-1=1$). Prove the following claim using mathematical induction on $n$:

(Hint: where does the induction hypothesis appear in the left-hand side summation?)

Problem 5: Another Problem Proof (Optional)

Here is yet another bogus claim and "proof" of that claim:

1. In a sentence or two, describe what the claim is saying and why it is incorrect.
2. In a sentence or two, describe the error in the "proof."
3. Correct the error and attempt to finish the proof. You should get stuck, i.e., a point where you are unable to move further in the proof. Show your work to get to this point and describe in a sentence or two why you cannot proceed forward with the proof.

Demonstration Exercise 3

Problem 1: Down By More Than One

Consider the following recursive Python definitions:

def is_even(n):
    if n == 0:
        return True
    elif n == 1:
        return False
    else:
        return is_even(n-2)

def iterate(f, x, n):
    if n == 0:
        return x
    else:
        return iterate(f, f(x), n-1)

For this problem, you may take the shortcut of evaluating any function call directly to the expression that it returns in a single step.

First prove the following auxiliary claim about even:

Then, consider the following claim about iterate:

In a sentence or two, describe at a high-level why this claim is correct.

Finally, formally prove this claim using the auxiliary claim.

Problem 2: Translation

Consider the following parameterized atomic propositions:

• $A(x,y,z)=$ "$x$ knows that $y$ owes $z$ money"
• $B(x,y)=$ "$x$ owes $y$ money"
• $D(x,y)=$ "$x$ will pay $y$"
• $C(x)=$ "$x$ is an honest person"

First, translate each of the following English propositions into a formal propositional statement, using the parameterized atomic propositions above. Make sure to make maximal use of the logical connectives, in particular, negation, in your formal statements.

• Either Sam owes the store money or the store owes Sam money.
• If Henry knows that Io owes Mateo money and Io is honest, then Io will pay Mateo.
• For all people $x$, if $x$ is not honest, then $x$ will not pay Tina.
• There exists people $x$ and $y$ such that for any person $z$, $x$ owes $y$ money but $z$ does not know that $x$ owes $y$ money.

Now consider the following formal propositional statements. Give English propositions that are equivalent to these formal statements.

• $D(\text{"Laura"},\text{"Roberto"})\to C(\text{"Laura"})$.
• $\forall x,y.C(x)\to D(x,y)$.
• $\forall x.\neg C(x)\to \exists y,z.A(y,x,z)\to \neg D(x,z)\wedge D(x,y)$.

Problem 3: Objection!

A logical fallacy is a misconception due to an erroneous step of logical reasoning. In this problem, we'll explore some common logical fallacies, their formal representation in propositional logic, and their refutation.

For each of the propositions below:

• Translate the proposition into a formal propositional statement, representing atomic propositions with fresh propositional variables. Make sure (a) state which variables correspond to which atomic propositions and (b) make maximal use of the logical connectives in your formal statement.
• In a few sentences, argue why the resulting formal proposition is not provable using your intuition of the semantics of the logical connectives of propositional logic.

(Hint: recall that logical implication $(\to )$ captures the idea that we assume that a proposition is true and go on to prove another proposition true using that assumption. Whenever a situation describes a proposition that you are supposed to assume is true, you should use implication to represent this fact.)

1. If I buy you a present, you will like me. I did not buy you a present, therefore you will not like me.
2. We know that this drug will cure cancer or kill the patient. We observe that the drug cures the patient. Therefore, the drug will not kill the patient.
3. Suspect A claims that suspect B was the thief. We showed that suspect A is a liar. Therefore, we know that suspect B is not a thief.
4. It has been proven that if you run, you will get into shape. I got into shape, therefore, I must have run.
5. I claim that there are mole people underground that are plotting to take over the world. There exists no evidence that implies there are not mole people underground. Therefore, my claim about mole people is correct.

Variations of Inductive Proof

We have learned that operations and proofs over inductively-defined objects follow from their inductive definitions. For example, recall the inductive definition of a list:

But this isn't the only way of sorting the infinite possible lists into a finite set of cases. For example, here is an alternative definition:

This definition differs from the previous one because it explicitly calls out the singleton list case. Both definitions are equivalent---every possible list is described by exactly one of the cases in each definition. But in some situations, using an alternative inductive definition is appropriate to better fit the operation we are describing or reasoning about.

We'll look at an inductive proof that takes advantage of this alternative definition. This is just one example of the variations we might encounter when performing inductive proof. There are many others out there, more than we can cover in the brief time we have in this course. However, be aware that these variations exist, but they all ultimately rest on our basic definition of inductive reasoning:

Case Study: Intersperse

Previously, we introduced the intersperse function takes an element x and a list l and returns a new list that puts x between each element of l.

def intersperse(v, l):
    match l:
        case []:
            return []
        case [x]:
            return [x]
        case [h, *tail]:
            return [h, v, *intersperse(v, tail)]

Suppose we want to prove the following claim:

Note that intersperse is defined according to our alternative, singleton-based definition of a list. Our proof, therefore, follows the cases outlined by this definition. If the cases include recursive sub-structure, i.e., tails of lists drawn from the subject of the inductive proof, then we gain the induction hypotheses for all of these sub-structures. These are our inductive cases whereas cases with no recursive sub-structures are called base cases.

Here is a formal proof the claim as an exemplar of the concepts we've learned so faralong with some of these additional concerns we've introduced such as using an alternative definition of lists. Study this proof carefully, paying attention to its structure and formatting.

Note that our claim is the form of a conditional: "if … then … ." This means that our induction hypothesis must also be of this form! This form of proposition is called a logical implication. When trying to prove an implication, we assume the "if" portion (the premise) and go on the prove the "then" portion (the conclusion). However, if we assume that an implication is true, we must first prove the "if" portion and then we can go on to assume the "then" portion. We will learn more about logical implication and, more generally, mathematical logic soon!

def intersperse(v, l):
    match l:
        case []:
            return []
        case [head, *tail]:
            return [head, v, *intersperse(v, tail)]

Lab: Strong Mathematical Induction

Consider the following classic numeric problem regarding making change:

Suppose that you live in a country where currency only comes in 3¢ and 10¢ denominations. Show that you can form any amount of money $n$ from 3¢ and 10¢ pieces as long as $n\ge 18$.

Let us attempt to prove this claim by induction. Really, the claims says that we can choose $x$ and $y$, such that $3x+10y=n$ as long as $n\ge 18$. $x$ and $y$ here are the number of 3¢ and 10¢ pieces, respectively.

1. Attempt to prove this claim by mathematical induction. Push the proof through as much as possible until you get stuck. Identify you get stuck and why you cannot make any more progress.

2. Since the proof did not work out, you might be tempted to believe that the claim is actually false; not an unreasonable conclusion. However, it turns out this claim is actually true. Develop a series of examples for $n=18$ through $n=26$ (9 examples in all) to convince yourself that this is the case.

3. Sometimes, a particular proof technique is not strong enough to prove a proposition. In these situations, we must resort to a different proof technique better suited for the situation at hand.

   Rather than using regular mathematical induction, we'll invoke a variant of mathematical induction, strong induction, to prove this claim.

   Definition (Strong Induction): strong induction is a proof principle that is like mathematical induction, i.e., induction over a natural number $n$, except that we assume that our induction hypothesis holds for any natural number $k<n$.

   Regular mathematical induction allows us to handle situations where our recursive definitions decrease by one on each step. Strong induction allows us to handle situations where our recursive definitions steps by more than just one and more generally, in irregular patterns.

   Practically speaking, to use the strong induction principle:

   • We state that we are using strong induction instead of regular induction.
   • We change our induction hypothesis to reflect the fact that the hypothesis holds for any natural number $k<n$ rather than just $n-1$.
   • Finally, we also may need to include additional base cases to account for the potentially irregular pattern that our inductive object decreases by.

   Change your original, incomplete inductive proof to a strong induction proof and complete it.

   (Hint 1: now your induction hypothesis holds for any number less than $n$. Don't overthink this part! Choose a convenient target value that is less than $n$ that you can apply your induction hypothesis to.)

   (Hint 2: now think about how much you decrease $n$ by in each inductive step. A single base case of $n=18$ is no longer sufficient because you are no longer decreasing by one. What additional base cases do you need?)

4. Once you are done, you might think this proof feels "too simple!" In some sense it is because the corresponding algorithm for making change implied by this proof is also straightforward! In a sentence or two, describe the algorithm for making change that is suggested by your reasoning. This final bit highlights the connection between proving and algorithmic design. We can design an algorithm with correctness in mind; dually, we often can derive an algorithm from our reasoning!

Have you ever been in an argument where the other person "just wasn't being reasonable?" What were they doing that was "without reason?"

• Making "facts" up out of thin air?
• Forming connections between claims without appropriate evidence?
• Jumping between unrelated arguments?
• Not addressing the problem at hand?

How do you know that you were being reasonable and your partner was the unreasonable one? Is there an agreed-upon set of rules for what it means to operate "within reason" or is it simply a matter of perspective?

Mathematical logic is the study of formal logical reasoning. Coincidentally, logic itself is one of the foundations of both mathematics and computer science. Recall that mathematical prose contains propositions that assert relationships between definitions. These propositions are stated in terms of mathematical logic and thus form one of the cornerstones of the discipline.

As computer scientists, we care about logic for similar reasons. We care about the properties of the algorithms we design and implement, in particular, their correctness and complexity. Logic gives us a way of stating and reasoning about these properties in a precise manner.

Propositional Logic

Let us begin to formalize our intuition about propositions. First, how can we classify propositions? We can classify them into two buckets:

• Atomic propositions that make elementary claims about the world. "It is beautiful today" and "it is rainy today" are both elementary claims about the weather.

• Compound propositions that are composed of smaller propositions "It is either rainy today or it is beautiful today" is a single compound proposition made of up two atomic propositions.

This is not unlike arithmetic expressions that contain atomic parts---integers---and compound parts---operators. As you learned about arithmetic throughout grade school, you learned about each operator and how they transformed their inputs in different ways. Likewise, we will learn about the different logical operators---traditionally called connectives in mathematical logic---and how they operate over propositions.

We can formally define the syntax of a proposition $p$ similarly to arithmetic using a grammar:

$$p::=A\mid \top \mid \perp \mid \neg p\mid p_1\wedge p_2\mid p_1\vee p_2\mid p_1\to p_2.$$

A grammar defines for a sort (the proposition $p$) its set of allowable syntactic forms, each written between the pipes ($\mid$). A proposition can take on one of the following forms:

• Atomic propositions, elementary claims about whatever domain we are considering. When we don't care about the particular domain (e.g., we want to hold the domain abstract), we'll use capital letters such as $A$ as meta-variables for atomic propositions.

• Top, $\top$ (LaTeX: \top), pronounced "top", the proposition which is always provable.

• Bot, $\perp$ (LaTeX: \bot), pronounced "bottom" or "bot", the proposition which is never provable.

• Logical negation, $\neg p$ (LaTeX: \neg), pronounced "not", which stands for proposition $p$, but negated. For example, the negation of $p$ = "It is beautiful today" is $\neg p$ = "It is not beautiful today".

• Logical conjunction, $p_1\wedge p_2$ (LaTeX: \wedge), pronounced "and", which stands for the proposition where both $p_1$ and $p_2$ are provable. For example, the conjunction of $p_1$ = "It is beautiful today" and $p_2$ = "The sun is out" claims that it is both beautiful and the sun is out.

• Logical disjunction, $p_1\vee p_2$ (LaTeX: \vee), pronounced "or", which stands for the proposition where at least one of $p_1$ or $p_2$ is provable. For example, the disjunction of $p_1$ = "It is beautiful today" and $p_2$ = "It is raining today" claims that it is either beautiful today or it is raining today (or both are true).

• Logical implication, $p_1\to p_2$ (LaTeX: \rightarrow), pronounced "implies", which stands for the proposition where $p_2$ is provable assuming $p_1$ is provable. For example, if $p_1$ = "It is cloudy" and $p_2$ = "It is raining", then $p_1\to p_2$ claims that it is raining, assuming that it is cloudy.

Notably, logical implication are the conditional propositions we have seen previously of the form "if … then … ." For example, if we had the following program correctness claim:

We might write it concisely using the formal notation above as:

This form of logic is called propositional logic because it focuses on propositions and basic logic connectives between them. There exist more exotic logics that build upon propositional logic with additional connectives that capture richer sorts of propositions we might consider.

Modeling with Propositions

Recall that mathematics is the study of modeling the world. In the case of mathematical logic, we would like to model real-world propositions using the language of mathematical propositions we have defined so far. This amounts to translating our informal natural language descriptions into formal mathematical descriptions.

To do this, keep in mind that mathematical propositions are formed from atomic and compound propositions. We then need to:

1. Identify the atomic propositions in the statement.

2. Determine how the atomic propositions are related through various compound propositions.

As an example, let's consider a proposition more complicated than the previous ones that we have encountered:

"If it is either the case that the grocer delivers our food on time, or I get out to the store this morning, then the party will start on time and people will be happy.

First, we identify the domain under which we are making this proposition: preparing for a party. Thus, the atomic propositions are the statements that directly talk about preparing for a party. These propositions are:

• $p_1$ = "The grocer delivers our food on time."
• $p_2$ = "I get out to the store this morning."
• $p_3$ = "The party will start on time."
• $p_4$ = "People will be happy."

Now, we re-analyze the statement to determine how the propositions are related, translating those relations into logical connectives. You may find it helpful to replace every occurrence of the atomic propositions with variables to make the connecting language pop out:

"If it is either the case that $p_1$ or $p_2$ then $p_3$ and $p_4$."

From this reformulation of the statement, we can see that:

• $p_1$ and $p_2$ are related by the word "or" which implies disjunction.
• $p_3$ and $p_4$ are related by the word "and" which implies conjunction.
• These previous two compound conjunctions are related by the words "if" and "then" which implies implication.

Thus we arrive at our full formalization of the statement:

$$p_1\vee p_2\to p_3\wedge p_4.$$

(Note that $(\to )$ has lower precedence than $(\vee )$ or $(\wedge )$ so the statement written as-is is not ambiguous.)

When translating statements in this manner, it is useful to keep in mind some key words that usually imply the given connective:

• $(\neg )$: "not"
• $(\wedge )$: "and"
• $(\vee )$: "or"
• $(\to )$: "implies", "if ...then"

Reasoning with Propositions

Recall that our goal is to formally model reasoning. While equivalences allow us to show that two propositions are equivalent, they do not tell us how to reason with propositions. That is, how do we prove propositions once they have been formally stated?

First, we must understand the reasoning process itself so that we can understand its parts. From there, we can state rules in terms of manipulating these parts. When we are trying to prove a proposition, whether it is in the context of a debate, an argument with a friend, or a mathematical proof, our proving process can be broken up into two parts:

• A set of assumptions, propositions that we are assuming are true.
• The proposition that we are currently trying to prove, our proof goal.

We call this pair of objects our proof state. Our ultimate goal when proving a proposition is to transform the proof goal into an "obviously" correct statement through valid applications of proof rules.

For example, if we are in the midst of a political debate, we might be tasked with proving the statement:

"80s-era Reaganomics is the solution to our current economic crisis."

Our proof goal is precisely this statement and our set of assumptions includes our knowledge of Reaganomics and the current economy. We might take a step of reasoning---unfolding the definition of Reaganomics, for example---to refine our goal:

"Economic policies associated with tax reduction and the promotion of the free-market are the solution to our current economic crisis."

We can then apply additional assumptions and logical rules to transform this statement further. Once our logical argument has transformed the statement into a self-evident form, for example:

"Everyone needs money to live."

Then, if everyone agrees this is a true statement, we're done! Because the current proof goal follows logically from assumptions and appropriate uses of logical rules, we know that if this proposition is true, then our original proposition is true. In a future reading, we will study these rules in detail in a system called natural deduction.

Propositional Logic Versus Boolean Algebra

Throughout this discussion, you might have noted similarities between propositions and a concept you have encountered previously in programming: booleans. Values of boolean type take on one of two forms, true and false, and there are various operators between booleans, && and ||,logical-AND and logical-OR, respectively. It seems like we can draw the following correspondence between propositions and booleans (using the boolean operators found in a C-like language):

• $\top$ is true.
• $\perp$ is false.
• $(\neg )$ is !.
• $(\wedge )$ is &&.
• $(\vee )$ is ||.

This correspondence is quite accurate! In particular, the equivalences we discussed in the previous section for propositions also work for boolean expressions. The only caveat is that there is no analog to implication for the usual boolean expressions, but the equivalence:

$$p_1\to p_2\equiv \neg p_1\vee p_2$$

Allows us to translate an implication into an appropriate boolean expression.

So why do we talk about propositions when booleans exist? It turns out they serve subtle, yet distinct purposes!

• A proposition is a statement that may be proven.
• A boolean expression is an expression that evaluates to true or false.

Note that a proposition does not say anything about whether the claim is true or false. It also doesn't say anything computational in nature, unlike a boolean expression which carries with it an evaluation semantics for how to evaluate it in the context of a larger computer program.

Furthermore, the scope of a boolean expression is narrow: we care about booleans values insofar as they assist in controlling the flow of a program, e.g., with conditionals and loops. We don't need to complicate booleans any further! In contrast, propositions concern arbitrary statements, and our language of propositions may need to be richer than the corresponding language of booleans to capture the statements we have in mind.

First-order Logic

Propositional logic gives us a formal language for expressing propositions about mathematical objects. However, is it sufficiently expressive? That is, can we write down any proposition we might have in mind using propositional logic?

On the surface, this seems to be the case because we can instantiate our atomic propositions to be whatever we would like. For example, consider the following proposition:

Every month has a day in which it rains.

We can certainly take this entire proposition to be an atomic proposition, i.e.,

$$P=\text{Every month has a day in which it rains}.$$

However, this is not an ideal encoding of the proposition in logic! Why is this the case? We can see that there is structure to the claim that is lost by taking the whole proposition to be atomic. In this case, the notion of "every" month is not distinguished from the rest of the proposition. This is a common idea in propositions, for example:

• For every natural number $n$, $n>0$.
• For any boolean expression $e$, $e{⟶}^{\ast }\mathsf{true}$.
• For any pair of people in the group, they are friends with each other.

We would like our formal language of logic to capture this idea of "every" as a distinguished form so that we can reason about it precisely. However, propositional logic has no such form!

To this end, we introduce a common extension to proposition logic, predicate logic (also known as first-order-logic), which introduces a notion of quantification to propositions. Quantification captures precisely this concept of "every" we have identified, and more!

Introducing Quantification

When we express the notion of "every month" or "any pair of people," we are really introducing unknown quantities, i.e., variables, into our propositions. For example, our sample proposition above introduces two such variables, months and days. At first glance, we might try expressing the proposition as an abstract proposition, i.e., a function that expects a month and day and produces a proposition:

$$P(x,y)=x\text{has}y\wedge \text{it rains during}y.$$

We call such functions that produce propositions predicates.

However, this encoding of our proposition is not quite accurate! If we think carefully about the situation, we will note that the interpretation of $x$ and $y$ are subtlety different! We can make this more clear by a slight rewriting of our original proposition:

For every month, there exists a day in which it rains.

Note how we are interested in "every month." However, we are not interested in "every day"; we only identify a single day in which the property holds. The property may hold for more than one day for any given month, but we only care that there is at least one such day.

Thus, we find ourselves needing to quantify our variables in two different ways:

• Any value (of a given type).
• At least one value (of a given type).

Observe that our predicate notation $P(x,y)$ does not tell us which quantification we are using!

First-order logic extends propositional logic with two additional connectives that make explicit this quantification:

$$p::=\dots \mid A(x)\mid \forall x.p\mid \exists x.p$$

• Universal quantification of a proposition, written $\forall x.p$ (pronounced "for all $x$, $p$", LaTeX: \forall) introduces a universally quantified variable $x$ that may be mentioned inside of $p$.
• Existential quantification of a proposition, written $\exists x.p$ (pronounced "there exists $x$, $p$", LaTeX: \exists) introduces an existentially quantified variable $x$ that may be mentioned inside of $p$.

These quantified variables may then appear inside of our atomic propositions. We write $A(x)$ to remind ourselves that our atomic propositions may be parameterized by these quantified variables.

With quantifiers, we can now fully specify our example in first-order logic:

$$P=\forall x.\exists y.x\text{has}y\wedge \text{it rains during}y.$$

The first quantifier $\forall x$ introduces a new variable $x$ that is interpreted universally. That is, the following proposition holds for every possible value of $x$. The second quantifier $\exists y$ introduces a new variable $y$ that is interpreted existentially. That is, the following proposition holds for at least one possible value of $y$. When taken together, our English pronunciation of this formal proposition now lines up with our intuition:

For all months $x$, there exists a day $y$ where $x$ has $y$ and it rains during $y$.

Variables and Scope in Mathematics

Like function headers in a programming language, quantifiers introduce variables into our propositions. For example, consider the following Python function definition:

def list_length(l):
    match l:
        case []:
            return 0
        case [_, *tail]:
            return 1 + list_length(tail)

Here, the function declaration introduces a new program variable l that may be used anywhere inside of the function list_length. However, l has no meaning outside of list_length. The location where a variable has meaning is called its scope:

In the case of functions, the scope of a parameter is the body of its enclosing function. So if we try to evaluate l outside of the definition of list_length, we receive an error:

>>> list_length([1, 2, 3])
3
>>> l
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
NameError: name 'l' is not defined

The same principles hold for logical variables. The quantifiers $\forall x.p$ and $\exists x.p$ introduce an appropriately quantified variable $c$ that has scope inside of $p$. $x$ does not have meaning outside of $p$. For example, the proposition:

$$P=x>5\wedge \forall x.x\ne 0.$$

Is malformed because the $x$ outside the quantifier is not well-scoped.

Implicit Types and Quantification

Variables are always quantified according to a particular set of values, its type. However, you may have noticed that we never mention the type of a variable in its quantification. How do we know what the type of $x$ is in $\forall x.p$? Traditionally, we infer the types of variables based on their usage.

For example, in the proposition:

$$\forall x.\exists y.x>y.$$

We can see that $x$ and $y$ are used in a numeric comparison $(>)$, so we assume that the quantified variables range over numbers. Could the variables be quantified more specifically? Certainly! $x$ and $y$ could certainly be real numbers, integers, or even the natural numbers (i.e., the positive integers or zero). We would need to look at more surrounding context, e.g., how this proposition is used in a larger mathematical text, to know whether the variables can be typed in more specific ways.

In addition to implicit types, sometimes quantification is also implicit. For example, the standard statement of the Pythagorean theorem is:

$$a^2+b^2=c^2$$

Where the quantification of $a$, $b$, and $c$ is implicit. What is the implied quantification of these variables? It turns out that when a quantifier is omitted, we frequently intend for the variables to be universally quantified, i.e., the Pythagorean theorem holds for any $a$, $b$, and $c$ of appropriate types.

When writing mathematics, you should always explicitly quantify your variables so your intent is clear. However, you should be aware that implicit typing and quantification is pervasive in mathematical texts, so you will need to use inference and your best judgment to make sense of a variable.

Lab: Modeling with Logic

Problem: Back and Forth

Translate each of the natural language propositions into formal logical propositions. Ensure in your answer that you (1) identify the atomic propositions and assign them to variables and (2) write your formal proposition in terms of these variables. Make sure you maximally translate the proposition using as many of the connectives introduced in the reading. In particular, make sure you use the negation logical operator when appropriate in your answers.

1. It rained this morning and it will be sunny this afternoon.
2. If I am forced to stay in-doors this week, I will play Genshin Impact, have fun, and become poor.
3. If I either eat Taco Bell or McDonalds, I will either become swoll, or I will not survive the night.
4. If Jan and Bob both work at the company, then Jan certainly works more than Bob.

Now, consider the following parameterized atomic propositions:

• $A(x)$ = "I love $x$."
• $B(x)$ = "$x$ barfs."
• $C(x)$ = "I own $x$."
• $D(x)$ = "I'm sending away $x$."

As well as their parameterized versions:

Translate each of the formal logical propositions to natural language propositions. Ensure that your natural language propositions clearly indicate the explicit grouping found in the formal logic propositions.

1. $A(\text{cats})\wedge B(\text{cats})$.
2. $A(\text{cats})\to \neg C(\text{dogs})$.
3. $A(\text{cats})\vee (B(\text{cat})\to C(\text{dog}))$.
4. $B(\text{my cat})\to D(\text{my cat})\wedge \neg A(\text{my cat})$.
5. $A(\text{dogs})\to C(\text{dogs})\wedge D(\text{cats})$.

Note that $(\wedge )$ and $(\vee )$ have higher precedence than $(\to )$. So, for example,

$$B(\text{my cat})\to D(\text{my cat})\wedge \neg A(\text{my cat})$$

is equivalent to

$$B(\text{my cat})\to (D(\text{my cat})\wedge \neg A(\text{my cat})).$$

Problem: Warm-up

In our examples from the reading relied heavily on non-mathematical, intuitive propositions to convey the meaning of quantified propositions. Now we'll consider translating propositions of a more mathematical nature between formal, symbolic statements and English.

First, translate each of the following formal statements regarding integers into English and for each, explain in a sentence or two why they are true.

• $\exists x.\exists y.x-y=0$.
• $\forall x.\exists y.y>x$.
• $\forall x.\forall y.x\ge y\wedge y\ge x\to x=y$.

Now, consider the following theorems taken from Fortnow's paper on his Favorite Ten Complexity Theorems of the Past Decade. Computational complexity theory is a branch of computer science concerning the resource usage (both time and space) of algorithms. While we do not have the background to fully understand what each of Fortnow's theorems (i.e., main propositions) says, we can certainly translate their logical intent. For each of these theorems, identify relevant atomic propositions and predicates and give a formal statement of the theorem maximizing your use of our logical connectives.

• Theorem 1: For any one-way function, there exists a pseudorandom generator constructed from that one-way function.
• Theorem 2: There are no sparse sets hard for $\text{NP}$ via polynominal-time bounded truth-table queries unless $\text{P}=\text{NP}$. (Hint: to deal with "unless," think about what it means and try to rewrite the theorem in terms of a "if...then" rather than "unless.")

Problem: Quantification and Negation

The negation of propositions can be tricky to reason about. De Morgan's laws:

• $\neg (p_1\wedge p_2)\equiv \neg p_1\vee \neg p_2$
• $\neg (p_1\vee p_2)\equiv \neg p_1\wedge \neg p_2$

Remind us that negation doesn't simply "distribute into" connectives like conjunction and disjunction. Instead, De Morgan's laws say we "distribute/factor the negations and flip the signs." Are there similar equivalences for quantifiers? We'll answer this question by using real-world examples and our intuition to gain understanding.

Consider the following variants of propositions involving universal and existential quantification and negation both inside and outside of the quantifier.

• $P_1=\forall x.A(x)$.
• $P_2=\exists x.A(x)$.
• $P_3=\neg \forall x.A(x)$.
• $P_4=\neg \exists x.A(x)$.
• $P_5=\forall x.\neg A(x)$.
• $P_6=\exists x.\neg A(x)$.

1. Come up with a concrete example predicate $A(x)$ to use for this exploration. For each of these propositions above, translate the proposition into English. Try to choose a predicate that is both memorable and simple to reason about.
2. Using your English translations as a guide, decide which pairs of propositions are equivalent.
3. For each pair of propositions you believe are equivalent, write a sentence or two justifying the equivalence, using your concrete example to explain why it holds.

Problem: Thinking About Proof

Thinking ahead, we've used first-order logic to explore the extends of what we can express as far as propositions go. However, we are studying logic in this course to derive a set of rules for proving a proposition. Because our propositions are defined inductively, i.e., as a finite set of cases, our rules for proving a proposition also follow by case analysis on the different cases.

For each possible form of a proposition given in the reading, describe at a high-level how you would go about proving that proposition in a few sentences per form. Use a concrete example of a proposition in English for each case to describe your process. For example, for conjunction $p_1\wedge p_2$, I would instantiate $p_1$ and $p_2$ to concrete propositions, e.g.,

• $p_1$ = "The sky is rainy."
• $p_2$ = "It is dark outside."

And then explain how I would prove $p_1\wedge p_2$. Use your example and your intuition about what each logical connective means to arrive at your process. In tomorrow's reading and lab, we'll firm up your intuition with concrete rules and then look at how we express these rules precisely using mathematical notation.

Natural Deduction

So far we have discussed the objects of study of logic, the proposition, defined recursively as:

$$p::=A(x)\mid \top \mid \perp \mid \neg p\mid p_1\wedge p_2\mid p_1\vee p_2\mid p_1\to p_2\mid \forall x.p\mid \exists x.p$$

However, recall that our purpose for studying propositional logic was to develop rules for developing logically sound arguments. Equivalences, while convenient to use in certain situations, e.g., rewriting complex boolean equations, do not translate into what we would consider to be "natural" deductive reasoning.

Now, we present a system for performing deductive reasoning within propositional logic. This system closely mirrors our intuition about how we would prove propositions, thus giving it the name natural deduction. As we explore how we formally define deductive reasoning in this chapter, keep in mind your intuition about how these connectives ought to work to help you navigate the symbols that we use to represent this process.

The Components of a Proof

To understand what are the components proof that we capture in natural deduction, let us scrutinize a basic proof involving the even numbers. First we remind ourselves what it means for a number to be even.

In other words, an even number is a multiple of two. This intuition informs how we prove the following fact:

From the above proof, we can see that there is an overall proposition that we must prove, called the goal proposition:

For any natural number $n$, if $n$ is even then $4n$ is also even.

As the proof evolves, our goal proposition changes over time according to the steps of reasoning that we take. For example, implicit in the equational reasoning we do in the proof:

$$4n=4(2k)$$

Is a transformation of our goal proposition, "$4n$ is even," to another proposition "$4(2k)$ is even." Ultimately, our steps of reasoning transform our goal repeatedly until the goal proposition is "obviously" provable. In the proof above, we transform our goal from "$4n$ is even" to "$2(4k)$ is even" by the rules of arithmetic. At this point, we can apply the definition of evenness directly which says that a number is even if it can be expressed as a multiple of two.

However, in addition to the goal proposition, there are also assumptions that we acquire and use in the proof. For example, the proposition "$n$ is even" becomes an assumption of our proof after we process the initial goal proposition which is stated in the form of an implication, $P\to Q$, where:

• $P=$ "$n$ is even"
• $Q=$ "$4n$ is even"

We then utilize this assumption in our steps of reasoning. In particular, it is the assumption that $n$ is even coupled with the definition of evenness that allows us to conclude that $n=2k$ for some natural number $k$. There exists other assumptions in our proof as well, e.g., $n$ and $k$ are natural numbers, that we use implicitly in our reasoning.

Proof States and Proofs

We can crystallize these observations into the following definition of "proof."

In our above example, we initially started with a proof state consisting of:

• No assumptions.
• The initial claim as our goal proposition: "For any natural number $n$, if $n$ is even then $4n$ is also even."

After some steps of reasoning that breaks apart this initial goal, we arrived at the following proof state:

• Assumptions: "$n$ is a natural number," "$n$ is even"
• Goal: "$4n$ is even."

At the end of the proof, we rewrote the goal in terms of a new variable $m$ and performed some factoring, leading to the final proof state:

• Assumptions: "$n$ and $m$ are natural numbers," "$n$ is even," "$m=4k$"
• Goal: "$2m$ is even"

This final goal is provable directly from the definition of evenness since the quantity $2m$ is precisely two times a natural number.

Rules of Natural Deduction

Our proof rules manipulate proof states, ultimately driving them towards goal propositions that are directly provable through our assumptions. Because of the syntax of our propositions breaks up propositions into a finite set of cases, our rules operate by case analysis on the syntax or shape of the propositions contained in the proof state. Specifically, these propositions can either appear as assumptions or in the goal proposition. Therefore, for each kind of proposition, we give one or more rules describing how we "process" that proposition depending on where it appears in the proof goal.

• Rules that operate on propositions in the goal proposition are called introduction rules. This is because we typically first introduce various propositions when they initially appear in our goal.
• Rules that operate on propositions in assumptions are called elimination rules. These rules use or "consume" assumptions, resulting in more assumptions and/or an updated set of goals.

A Note on the Presentation of Proof Rules

When we talk about rules of proof we really mean the set of "allowable actions" that we can take on the current proof state. We describe these rules in the following form:

To prove a proof state of the form … we can prove proof state(s) of the form …

One of our proof rules applies when it has the form specified by the rule, e.g., the goal proposition is a conjunction or there is an implication in the assumption list. The result of the proof rule is one or more new proof states that we must now prove instead of the current state. In effect, the proof rule updates the current state to be a new state (or set of states) that becomes the new proof state under consideration.

In terms of notation, we will use $p$ and $q$ to denote arbitrary propositions. Similarly, for assumptions, we will use the traditional metavariable $\Gamma$ (i.e., Greek uppercase Gamma, $\text{LATEX}$: \Gamma) to represent an arbitrary set of assumptions. When writing down our proof rules, it is very onerous to describe the components of proof states in prose:

If our proof state contains assumptions $\Gamma$ and goal proposition $p$ … .

Instead, we will write down a proof state as a pair of a set of assumptions and a proof state. Traditionally, we write pairs using parentheses, separating the components of the pair with commas, e.g., a coordinate pair $(x,y)$. However, in logic, we traditionally write this pair as a stylized pair called a sequent:

$$\Gamma ⊢p.$$

The turnstile symbol ($\text{LATEX}$, \vdash) acts like the comma in the coordinate pair; it merely creates visual separation between the assumptions $\Gamma$ and the goal proposition $p$.

Conjunction and Assumptions

A conjunction, $p_1\wedge p_2$, is a proposition that asserts that both propositions $p_1$ and $p_2$ are provable. For example, the proposition "I'm running out of cheeseburgers and the sky is falling" is a conjunction of two propositions: "I'm running out of cheeseburgers" and "the sky is falling." We call each of the sub-propositions of a conjunction a conjunct.

First, let's consider how we prove a proposition that is a conjunction. If we have to prove the example proposition above, our intuition tells that we must prove both "sides" of the conjunction. That is, to show that the proposition "I'm running out of cheeseburgers and they sky is falling", we must show that both

• "I'm running out of cheeseburgers" and
• "the sky is falling"

Are true independently of each other. In particular, we don't get to rely on fact being true when going to prove the other fact.

We can codify this intuition into the following proof rule describing how we can process a conjunction when it appears as our proof goal:

Recall that $\Gamma ⊢p_1\wedge p_2$ represents the following proof state:

• We assume that the assumptions in set $\Gamma$ are provable.
• Our goal proposition we must prove is $p_1\wedge p_2$.

Our proof rule says that whenever we have a proof state of this form, we can prove it by proving $\Gamma ⊢p_1$ and $\Gamma ⊢p_2$ as two separate cases. More generally, our introduction rules describe, for each kind of proposition, how to prove that proposition when it appears as a goal.

Note that this proof rule applies only when the overall goal proposition is of the form of a conjunction. For example:

• If our goal is $A\wedge B$, then the intro-∧ rule applies with $p_1=A$ and $p_2=B$.
• If our goal is $(A\to B)\wedge (C\wedge D)$, then the intro-∧ rule applies with $p_1=A\to B$ and $p_2=C\wedge D)$.

This rule cannot be applied if only a sub-component of the goal proposition is a conjunction. For example, if our goal is $A\to (B\wedge C)$, the rule does not apply even though $B\wedge C$ is part of the goal.

Now, what happens if the conjunction appears to the left of the turnstile, i.e., as an assumption? From our intro-∧ rule, we know that if the conjunction is provable, then both conjuncts are provable individually. So if we know that "I'm running out of cheeseburgers and the sky is falling" is provable, then we know that both conjuncts are true, i.e., "I'm running out of chesseburgers" and "the sky is falling." The following pair of rules captures this idea:

If we are trying to prove some proposition $p$ and we assume that a conjunction $p_1\wedge p_2$ is true, then the two rules say we can continue trying to prove $p$, but with an additional assumption gained from the conjunction. In terms of the new notation in these rules:

• To state that $p_1\wedge p_2$ is contained in $\Gamma$, we write $p_1\wedge p_2\in Gamma$ where the $(\in )$ symbol ($\text{LATEX}$, \in) is pronounced "in."
• To add a new assumption to the set of assumptions $\Gamma$, we "cons" on the new assumption, e.g., $p_1$ in the elim-∧-left rule, by adding it to the front of $\Gamma$ with a comma, i.e., $p_1,\Gamma$.

The elim-∧-left rule allows us to add the left conjunct to our assumptions, and the elim-∧-right rule allows us to add the right conjunct. In effect, these elimination rules allow us to decompose or extract information from assumptions. However, how do we use these assumptions to prove a goal? The assumption rule allows us to prove a goal proposition directly if it is one of our assumptions.

Proofs in Natural Deduction

First-order logic and natural deduction give us all the definitions necessary for rigorously defining every step of reasoning in a proof. Let's see this in action with a simple claim within formal propositional logic.

Claim: $A,B⊢A\wedge B$.

First, let's make sure we understand what the claim says. To the left of the turnstile are our set of assumptions. Here we assume that propositions $A$ and $B$ are provable. To the right of the turnstile is our goal. We are trying to prove that $A\wedge B$ is provable.

Next, let's develop a high-level proof strategy. Because we are working at such a low-level of proof, it is important to ask ourselves:

• Is the proof state as I understand it provable?
• How do the different parts of the proof state relate to each other?

In our example claim, we see that the proposition consists of atomic propositions $A$ and $B$ joined by conjunction and those same propositions appear as assumptions in the initial sequent. Thus, our overall strategy in our proof will be to decompose the proof goal into cases where we need to prove these individual cases directly via our hypotheses.

With this in mind, let's see what the formal proof looks like:

Because each proof rule creates zero or more additional proof states that we must prove or discharge, our proofs take on a tree-like shape. In a diagram, our reasoning would look as follows:

      A, B |- A ∧ B
        /        \
  [intro-∧ (1)]   [intro-∧ (2)]
      /            \
 A, B |- A     A, B |- B
    /                \
[assumption: A]  [assumption: B]

Because the intro-∧ rule creates two sub-goals we must prove, we have two branches of reasoning emanating from our initial proof state, one for each goal (labeled (1) and (2), respectively). We then prove each branch immediately by invoking the appropriate assumption. Every proof, not just in formal logic but in any context, has a hierarchical structure like this.

We can write this hierarchical structure in linear prose with a bulleted list where indentation levels correspond to branching. Whenever we perform case analysis, we should be clear when we are entering different cases, usually through some kind of sub-heading or bullet-like structure.

Finally, note that we cite every step of our proof. This "luxury" is afforded to us because our proof rules are now explicit and precise---we can justify every step of reasoning as an invocation of one of our proof rules!

Implication

Next, let's look at implication. An implication, $p_1\to p_2$, is a proposition that asserts that whenever $p_1$ is provable, then $p_2$ is provable as well. For example, the proposition "If I'm running out of cheeseburgers then the sky is falling" is an implication where "I'm running out of cheeseburgers" is the premise of the implication and "the sky is falling" is the conclusion.

Implication is closely related to the preconditions and postconditions we analyzed in our study of program correctness. Pre- and postconditions form an implication where the preconditions are premises and the postcondition is a conclusion. When we went to prove a claim that involved pre- and postconditions, we assumed that preconditions held and went on to prove the postcondition. Likewise here, to prove an implication, we assume the premises and then go on to prove the conclusion.

What do we do if the implication appears as a hypothesis, i.e., to the left of the turnstile, rather than the right? We saw this process, too, in our discussion of program correctness. If we had an auxiliary claim that we proven that was the form of a conditional, or if our induction hypothesis was a conditional, we needed to first prove the preconditions and then we could assume that the conclusion held. Thus, to use an assumed implication, we must first prove its premise and then we can assume the conclusion as a new hypothesis:

After using elim-→, we must prove two proof goals:

1. The first requires us to prove that the premise of the assumed implication is provable.
2. The second requires us to prove our original goal, but with the additional information of the conclusion of implication.

If you are familiar with logic already, e.g., from a symbolic logic class, you should recognize elim-→ as the modus ponens rule that says:

If $p$ implies $q$ and $p$ is true, then $q$ is true as well.

Here is a pair of simple example proofs that illustrate the basic usage of these rules:

Compare the flow of these proofs with the rules presented in this section to make sure you understand how the rules translate into actual proof steps.

Disjunction

Now, let's look at disjunction. A disjunction, $p_1\vee p_2$, is a proposition that asserts that one or both of $p_1$ and $p_2$ are provable as well. For example, the proposition "I'm running out of cheeseburgers or the sky is falling" is a disjunction where at least one of "I'm running out of cheeseburgers" and "the sky is falling" must be provable.

Again, using our intuition, we can see that if we have to prove a disjunction, our job is easier than with a conjunction. With a conjunction we must prove both conjuncts; with disjunction, we may prove only one of the disjuncts.

The intro-∨-left and intro-∨-right rules allow us to explicit choose the left- and right-hand sides of the disjunction to prove, respectively.

We have flexibility in proving a disjunction. However, that flexibility results in complications when we reasoning about what we know if a disjunction is assumed to be true. As an example, suppose that our example disjunction from above is assumed to be true. What do we know as a result of this fact? Well, we know that at least one of "I'm running out of cheeseburgers" and "the sky is falling" is true. The problem is that we don't know which one is true!

We seem to be stuck! It doesn't seem like we can extract any interesting information from a disjunction. Indeed, a disjunction doesn't give us the same direct access to new information like a conjunction. However, disjunctions can be used in an indirect manner to prove a claim!

Suppose that we are trying to prove the claim that "the apocalypse is now" and we know our disjunction is true. We know that at least of the disjuncts is true, so if we can do the following:

• Assume that "I'm running out of cheeseburgers" and then prove "the apocalypse is now."
• Assume that "the sky is falling" and then prove "the apocalypse is now."

It must be the case that apocalypse is happening because both disjuncts imply the apocalypse and we know at least one of the disjuncts is true!

This logic gives rise to the following left-rule for disjunction:

In effect, a disjunction gives us additional assumptions when proving a claim, but we must consider all possible cases when doing so. This reasoning should sound familiar: this is precisely the kind of reasoning we invoke when analyzing the guard of a conditional in a computer program: "either the guard evaluates to true or false." This reasoning is possible because we know that the guard of a conditional produces a boolean value and booleans can only take on two values.

Top, Bottom, and Negation

Finally, we arrive at our two "trivial" propositions. Recall that $\top$ ("top") is the proposition that is always provable and $\perp$ ("bottom") is the proposition that is never provable.

First let's consider $\top$. Since $\top$ is always provable, its introduction is straightforward to write down:

But what if we know $\top$ holds as an assumption? Well that doesn't mean much because intro-⊤ tells us that we can always prove $\top$! Indeed, there is no left-rule for $\top$ because knowing $\top$ holds does not tell us anything new.

Similarly, because $\perp$ is never provable, there is no introduction rule for $\perp$ because we should never be able to prove it! But what does it means if $\perp$ somehow becomes an assumption in our proof state? Think about what this implies:

• $\perp$ is defined to never be provable.
• We assume that $\perp$ is provable as a hypothesis.

This is a logical contradiction: we are assuming something we know is not true! We are now in an inconsistent state of reasoning where, it turns out, anything is provable. This gives rise to the following elimination rule for $\perp$:

Finally, how do we handle negation? It turns out rather than giving proof rules for negation, we'll employ an equivalence, relating negation to implication:

$p\to \perp$ means that whenever we can prove $p$ we can "prove" a contradiction. Since contradictions cannot arise, it must be the case that $\neg p$ must be true instead.

Reasoning About Quantifiers

We have given rules for all of the connectives in propositional logic. But what about the additional constructs from first-order logic: universal and existential quantification? Let's study each of these constructs in turn.

Universal Quantification

A universally quantified proposition, for example, $\forall x.x\ge 5$ holds for all possible values of its quantified variable. Here, $x\ge 5$ means that every possible value of $x$ is greater than five.

Because the proposition must hold for all possible values, when we go to prove a universally quantified proposition, we must consider the value as arbitrary. In other words, we don't get to assume anything about the universally quantified variable. As we discussed during the program correctness section of the course, this amounts to substituting an unknown, yet constant value for that variable when we go to reason about the proposition. In practice, we think of the variable as the unknown, yet constant value, but it is important to remember that we need to remove the variable, either implicitly or explicitly, from the proposition before we can continue processing it.

In contrast, when we have a universally quantified proposition as an assumption, we can take advantage of the fact that the proposition holds for all values. We do so by choosing a particular value for the proposition's quantified variable, a process called instantiation. We can choose whatever value we want, or even instantiate the proposition multiple times to many variables, depending on the situation at hand.

We can summarize this behavior as introduction and elimination rules in our natural deduction system: