Lecture - Functional Programming, MT22, VII

Created: November 08, 2022

Flashcards

What is the “take lemma” about $\text{xs}$ and $\text{ys}$?
\[\forall n \in \mathbb{N} \text{ (take n xs} = \text{take n ys)} \implies \text{xs} = \text{ys}\]

Why is the take lemma useful?

Because it lets you prove stuff about functions that return lists using induction on the natural numbers.

What is a partial list?

A list with a tail that is either $\bot$ or a smaller partial list.

What’s the induction scheme for proving a property $P(\text{xs})$ is true for all finite lists?
  • Prove $P([])$
  • Prove $P(\text{xs}) \implies P(\text{x}:\text{xs})$

What’s the induction scheme for proving a property $P(\text{xs})$ is true for all partial lists?
  • Prove $P(\bot)$
  • Prove $P([])$
  • Prove $P(\text{xs}) \implies P(\text{x}:\text{xs})$

Given that $P$ is chain-complete (i.e. because it’s an equation between haskell expressions) then what is the induction scheme for proving a property $P(\text{xs})$ about all infinite lists?
  • Prove $P(\bot)$
  • Prove $P([])$
  • Prove $P(\text{xs}) \implies P(\text{x}:\text{xs})$

What’s a good heuristic for deciding what variable to induct on when proving something about a program?

Look at what the definition recurses on.



Related posts