Code Katas
Small programming exercises can sharpen the definitions in this module. Use any language you are comfortable with. The goal is not production code. The goal is to make formal ideas operational.
Kata 1: Truth-Table Generator
Time limit: 20 minutes
Goal: Encode propositional formulas and generate all truth assignments for two or three variables.
Setup: Accept a small hard-coded formula such as (P -> Q) <-> (not Q -> not P).
Implement a script that prints the full table and tells you whether the formula is a tautology.
Repeat until: You can generate a table without confusing implication with conjunction.
Kata 2: Relation Classifier on a Finite Set
Time limit: 20 minutes
Goal: Test reflexive, symmetric, antisymmetric, and transitive properties algorithmically.
Setup: Represent a relation as a set of ordered pairs over a finite set.
Write a classifier that reports which properties hold and prints one violating witness when a property fails.
Repeat until: You can explain the output using the formal definitions, not only the code behavior.
Kata 3: Function Image and Preimage Checker
Time limit: 20 minutes
Goal: Compute images and preimages for functions on finite domains.
Setup: Represent a function by a dictionary or table from a finite domain to a codomain.
Given a subset of the domain, compute its image. Given a subset of the codomain, compute its preimage.
Repeat until: You never mix up the direction of image and preimage.
Kata 4: Recursive Size Function
Time limit: 20 minutes
Goal: Implement a recursive size or depth function on a recursively defined object such as a list, binary tree, or expression tree.
Setup: Use a tiny custom data type or nested list structure.
After implementing the function, write a short note explaining what the corresponding structural-induction proof would need to show.
Repeat until: You can connect the recursive cases in code to the constructor cases in the proof.
Completion Standard
- Completed all four katas at least once
- Explained the mathematical definition each kata operationalizes
- Produced at least one bug or edge case that corrected your understanding