This homework covers material from Lecture 1: The Study of Programming Languages and Lecture 2: Classical Logic and Proofs. You will demonstrate comprehension of programming language foundations, formal reasoning, and logical systems.
All questions require written responses. Show your work where applicable, and provide clear justifications for your answers. Partial credit will be awarded based on the quality of your reasoning.
In your own words, define programming language and computation. Your definitions should capture the essential characteristics discussed in lecture.
The lecture introduced four major programming paradigms: imperative, functional, object-oriented, and logic.
Choose two paradigms and for each:
The lecture showed the "sum of even squares" problem implemented in many languages across different decades. Consider this Haskell implementation:
sumOfEvenSquares :: [Int] -> Int
sumOfEvenSquares = sum . map (^ 2) . filter even
Compare this to an imperative approach (like C or Fortran with explicit loops). Identify:
Explain what it means for a language to be:
Give one practical consequence that arises from each category.
Rust's ownership and borrowing system is formalized in its type system to prevent data races at compile time.
Explain:
Compare a language with formal foundations from birth (choose one: ML, Haskell, or Rust) to one formalized after the fact (choose one: JavaScript or C).
For each language, describe one practical consequence (positive or negative) that arose from its approach to formalization, with a specific example.
Python is described as "still being formalized" through its gradual typing system.
Explain:
Classify each of the following as a term, predicate, or formula:
Using the predicates provided below, translate each English sentence into first-order logic:
Available predicates:
Translate:
The description operator
Explain:
Construct a complete truth table for the following compound formula:
Based on your truth table, what can you conclude about the relationship between implication and disjunction?
Many students find it counterintuitive that
Explain:
Consider the following formulas. For each, determine whether it is valid (tautology), satisfiable (but not valid), or unsatisfiable (contradiction). Justify each answer.
De Morgan's Laws state:
Demonstrate the first law using a truth table. Show all columns for
The order of quantifiers matters. Explain the difference in meaning between:
Give a scenario where statement 1 is true but statement 2 is false.
Intuitionistic logic rejects the law of excluded middle (
Explain:
Translate each of the following natural language statements into formal logic using the appropriate modal operators. Identify which modal logic (alethic, deontic, epistemic, doxastic, or temporal) you are using.
In fuzzy logic, the statement "Bob is tall" might have a truth value of 0.7 (Bob is 70% tall).
Given:
Calculate the fuzzy truth values for:
Show your work using the standard fuzzy operators.
The lecture mentioned that predicate logic can sometimes express ideas similar to modal operators. For example:
Explain why this equivalence works. What does "possible worlds" semantics mean in this context?
Natural deduction proofs use introduction and elimination rules to derive conclusions from premises. This question tests your ability to read and understand proofs.
Consider the following natural deduction proof:
1. P ∧ Q (premise)
2. P (∧E₁ from 1)
3. Q (∧E₂ from 1)
4. Q ∧ P (∧I from 3, 2)
Answer the following:
Consider this proof of implication transitivity:
1. [P ⊃ Q] (assumption)
2. [Q ⊃ R] (assumption)
3. [P] (assumption)
4. Q (⊃E from 1, 3)
5. R (⊃E from 2, 4)
6. P ⊃ R (⊃I from 3-5)
7. (Q ⊃ R) ⊃ (P ⊃ R) (⊃I from 2-6)
8. (P ⊃ Q) ⊃ ((Q ⊃ R) ⊃ (P ⊃ R)) (⊃I from 1-7)
Answer the following:
For each of the following logical fallacies, explain what inference rule it superficially resembles and why the fallacy is invalid:
Affirming the Consequent: "If it rains, the ground is wet. The ground is wet. Therefore, it rained."
Denying the Antecedent: "If you study, you'll pass. You didn't study. Therefore, you won't pass."
Appeal to Ignorance: "No one has proven that aliens don't exist, so they must exist."
Define soundness and completeness for a logical system.
For each property:
Godel's Incompleteness Theorems revealed fundamental limits of formal systems.
The Curry-Howard Correspondence reveals that proofs are programs and propositions are types.
| Logic | Programming |
|---|---|
| Proposition | Type |
| Proof | Program |
| Implication | Function type |
| Conjunction | Product type |
Choose one of these correspondences and explain it in detail:
| Section | Question | Points |
|---|---|---|
| Part 1 | Q1: Languages, Paradigms, and History | 15 |
| Q2: Formal Foundations in Practice | 10 | |
| Part 2 | Q3: Building Blocks of Logic | 15 |
| Q4: Logical Operators and Semantics | 15 | |
| Q5: Alternative Logics | 15 | |
| Q6: Reading Natural Deduction Proofs | 15 | |
| Q7: Metalogic and Curry-Howard | 15 | |
| Total | 100 |
This optional assignment is Stage 1 of a semester-long project: building pieces of a real WebAssembly (Wasm) implementation. WebAssembly is a formally specified, industry-standard compilation target that runs in every major browser and an increasing number of server-side environments. Its specification is written using the exact formalisms you are studying in this course — and you are going to read it.
In HW1, you read and reasoned about inference rules and natural deduction proofs on paper. In this optional, you will translate those same structures into code — for a real industrial specification.
All stages of this project work on a restricted subset of WebAssembly, keeping the scope manageable while remaining Turing-complete:
i32 onlyi32.const, i32.add, i32.sub, i32.mul, i32.div_s, i32.eq, i32.lt_s, i32.gt_s, i32.eqzlocal.get, local.setblock, loop, if/else/end, br, br_if, return, nopcalldropThis subset supports factorial, fibonacci, and simple loops — everything you need to see the full formal pipeline at work.
Before you begin coding, read the following sections of the WebAssembly Core Specification:
Introduction → Overview — Read the "Semantic Phases" section. Note that Wasm's pipeline is: Decoding → Validation → Execution. This stage implements Validation.
Structure → Types — Focus on numtype (specifically i32), valtype, and functype. These are the types your checker will work with.
Validation → Instructions — This is the core reading. Each instruction has a typing rule written as an inference rule. Start with the simple ones:
nop — an axiom with no premisesdrop — consumes one value of any typelocal.get — reads from the contexti32.add — consumes two i32 values, produces one (identical in structure to a BinaryOp rule)Validation → Conventions — Understand the typing context types, funcs, locals, labels, and return. This is the analog of the environments you will study later in the course.
Implement a function typecheck(instruction, context) that takes an instruction AST node and a typing context, and returns the instruction's type signature (input types → output types) or raises a type error.
Your type checker should handle all instructions in the target subset above. For each instruction, your code should correspond directly to one inference rule from the spec. Add a comment above each case citing the spec rule you are implementing (e.g., "See spec: valid/instructions.html § i32.add").
You may use any programming language.
Below is a reference data model you can use or adapt. You do not need to follow this structure exactly — it is here to get you started.
AST types — representing the instructions in the target subset:
Instruction =
| I32Const(value: int)
| I32Add | I32Sub | I32Mul | I32DivS
| I32Eq | I32LtS | I32GtS | I32Eqz
| LocalGet(index: int)
| LocalSet(index: int)
| Block(resultType: valtype?, body: Instruction[])
| Loop(resultType: valtype?, body: Instruction[])
| If(resultType: valtype?, thenBody: Instruction[], elseBody: Instruction[])
| Br(labelIndex: int)
| BrIf(labelIndex: int)
| Return
| Nop
| Drop
| Call(funcIndex: int)
Typing context — the information available during validation:
Context = {
locals: valtype[] -- types of local variables
labels: resulttype[] -- stack of label types (for br/br_if targets)
return: resulttype? -- return type of the enclosing function
funcs: functype[] -- signatures of all functions in the module
}
valtype = "i32"
functype = { params: valtype[], results: valtype[] }
resulttype = valtype[]
Type signature — what your function returns for each instruction:
instrtype = { inputs: valtype[], outputs: valtype[] }
For example, i32.add has the signature { inputs: ["i32", "i32"], outputs: ["i32"] }.
Use these to verify your implementation. Each is a sequence of instructions with a declared context.
Test 1 — Simple arithmetic: Context: locals = ["i32", "i32"]. Instructions: [local.get 0, local.get 1, i32.add]. Expected signature: [] → ["i32"].
Test 2 — Type error: Context: locals = []. Instructions: [local.get 0]. Expected: type error (index out of bounds).
Test 3 — Conditional: Context: locals = ["i32"], labels = []. Instructions: [local.get 0, if (result i32) [i32.const 1] else [i32.const 0] end]. Expected signature: [] → ["i32"].
Test 4 — Function call: Context: locals = ["i32"], funcs = [{ params: ["i32"], results: ["i32"] }]. Instructions: [local.get 0, call 0]. Expected signature: [] → ["i32"].
Test 5 — Drop and nop: Context: locals = ["i32"]. Instructions: [local.get 0, drop, nop]. Expected signature: [] → [].
Submit your type checker source code and verify it passes all 5 tests. Additionally, write a short reflection (1 paragraph): compare the structure of one Wasm typing rule from the spec to one natural deduction rule from HW1 Q6. What is structurally the same? What differs?