COMP3161/9164 Concepts of Programming Languages
Term 3, 2024

Tute - Completed (Week 1)

Table of Contents

1. Predicate Logic

1.1. Question 1

For which values of \(A\) and \(B\) does the boolean expression \(\varphi = \neg (A \Rightarrow B) \lor \neg B\) hold?

Using a truth table:

\(A\) \(B\) \(A \Rightarrow B\) \(\neg B\) \(\varphi\)
\(\bot\) \(\bot\) \(\top\) \(\top\) \(\top\)
\(\bot\) \(\top\) \(\top\) \(\bot\) \(\bot\)
\(\top\) \(\bot\) \(\bot\) \(\top\) \(\top\)
\(\top\) \(\top\) \(\top\) \(\bot\) \(\bot\)

This is an answer but it is not so informative. Using boolean algebra manipulation instead:

\begin{array}{lcl} \neg (A \Rightarrow B) \lor \neg B & = & \neg (\neg A \lor B) \lor \neg B \\ & = & (A \land \neg B) \lor \neg B \\ & = & (A \lor \neg B) \land (\neg B \lor \neg B) \\ & = & (A \lor \neg B) \land \neg B \\ & = & \neg B \\ \end{array}

Here we can see clearly that \(\varphi\) holds only when \(B\) is false, and the value of \(A\) does not matter.

1.2. Question 2

Simplify the boolean expression \((A \Rightarrow B) \lor (B \Rightarrow A)\)

\begin{array}{lcl} (A \Rightarrow B) \lor (B \Rightarrow A) & = & (\neg A \lor B) \lor (\neg B \lor A) \\ & = & (\neg A \lor A) \lor (\neg B \lor B) \\ & = & \top \lor \top\\ & = & \top \\ \end{array}

This proof is not constructive. Discuss what it means for a proof to be constructive.

1.3. Question 3

A binary connective \(\bullet\) is defined as follows:

\(A\) \(B\) \(A\ \bullet\ B\)
\(\bot\) \(\bot\) \(\top\)
\(\bot\) \(\top\) \(\bot\)
\(\top\) \(\bot\) \(\top\)
\(\top\) \(\top\) \(\top\)

Restate the formula \(A \lor B\) in terms of \(\bullet\). What is the \(\bullet\) connective?

\(A \bullet \neg B\), \(\bullet\) is a flipped implication operator. The ex falso quodlibet principle is relevant here: from false, you can prove anything.

1.4. Question 4

Assuming that \(F(x)\) states that the person \(x\) is my friend and that \(P(x)\) states that the person \(x\) is perfect, what is a logical translation of the phrase "None of my friends are perfect"?

One option is \(\lnot \exists x. \; F(x) \land P(x)\), which can be read literally as saying "there does not exist a person \(x\) such that they are both my friend and perfect" in plain English. There are a number of other equally-valid translations too:

  • \(\forall x. \; F(x) \Rightarrow \lnot P(x)\), which can be read as saying "if a person is my friend, then they aren't perfect".
  • \(\forall x. \; P(x) \Rightarrow \lnot F(x)\), which can be read as saying "if a person is perfect, then they aren't my friend".

The logical formulae for all 3 are equivalent. As an exercise, prove this!

1.5. Question 5

Given the following function

\[ f (n) = \begin{cases} 0 & \text{if}\ n = 0 \\ 2n - 1 + f(n-1) & \text{if}\ n > 0 \end{cases} \]

Prove that \(\forall n \in \mathbb{N}.\ f(n) = n^2\).

Proof by mathematical induction on the natural number \(n\).

Base Case: \(n = 0\)

\begin{array}{lcl} f(0) & = & 0 \\ & = & 0^2 \\ & & \blacksquare \end{array}

Inductive Case: \(n = k + 1\), for arbitrary \(k \in \mathbb{N}\). Assume the inductive hypothesis that \(f(k) = k^2\).

\begin{array}{lcl} f(k+1) & = & 2(k+1) - 1 + f(k) \\ & = & 2k + 2 - 1 + f(k) \\ & = & 2k + 1 + f(k) \\ & = & 2k + 1 + k^2 \quad \text{(I.H)}\\ & = & k^2+k+k+1 \\ & = & k(k+1)+(k+1) \\ & = & (k+1)(k+1) \\ & = & (k+1)^2 \\ & & \blacksquare \end{array}

Thus \(f(n) = n^2\) for all \(n \in \mathbb{N}\).

2. Haskell

Consider the Haskell code written in the lecture.

2.1. Haskell lexical structure

  1. What is the difference between a data and a type declaration?
  2. What is the difference between a type and a data constructor? List the identifiers in the code which represent type names, and those which represent data constructor names.
  3. Which phase of the compiler would be responsible for distinguishing type and data constructors?

1: A data declaration introduces a new type, for example the Tree type below. type keyword just introduces a new name for an existing type, like typedef in C. For example, the String type in the standard library is defined merely to be [Char] using a type declaration.

2: A data constructor describes a way to create a value of a certain type. For example, the data constructors in the below Tree type are Leaf and Branch:

data Tree a = Branch a (Tree a) (Tree a) | Leaf

3: The parser is responsible, as it requires information from the grammar of the language to determine if, for example, Tree is a data constructor or a type name, as it is lexically indistinguishable.

2.2. Haskell programming

  1. Write a Haskell function mySum that sums all elements in a list of numbers. Feel free to use the following template:

    mySum :: [Int] -> Int
    mySum []     = ???
    mySum (n:ns) = ???
    
  2. Write a Haskell function myProduct that multiplies all elements in a list of numbers.
  3. You probably used copypaste to solve the previous question, didn't you? No reason to be ashamed, we've all done it! But let's try not to.

    Find a generalisation myBinop that applies a given binary operator f with unit element z to a list of numbers. We will then be able to define myProduct and mySum using myBinop.

    myBinop :: (Int -> Int -> Int) -> Int -> ([Int] -> Int)
    myBinop f z [] = ???
    myBinop f z (n:ns) = ???
    
    mySum :: [Int] -> Int
    mySum ns = myBinop (+) 0 ns
    
    myProduct :: [Int] -> Int
    myProduct ns = myBinop (*) 1 ns
    
  4. We just reinvented a wheel. The fold functions are general-purpose library functions that completely subsume myBinop. Try to implement mySum and myProduct using foldr instead of myBinop.

    The linked library documentation references a lot of concepts that we don't assume familiarity with, so don't worry if you don't fully understand it. Perhaps start by looking at the examples.

mySum :: [Int] -> Int
mySum [] = 0
mySum (n:ns) = n + mySum ns

myProduct :: [Int] -> Int
myProduct [] = 1
myProduct (n:ns) = n*myProduct ns

myBinop :: (Int -> Int -> Int) -> Int -> ([Int] -> Int)
myBinop f z [] = z
myBinop f z (n:ns) = n `f` myBinop f z ns

mySum2 :: [Int] -> Int
mySum2 = myBinop (+) 0

myProduct2 :: [Int] -> Int
myProduct2 = myBinop (*) 1

mySum3 :: [Int] -> Int
mySum3 = foldr (+) 0

myProduct3 :: [Int] -> Int
myProduct3 = foldr (*) 1

3. Subtyping Sins

The Monday lecture demonstrated a flaw in Java's static type system. It's been there for decades and it's well-known, including by the Java developers. Yet they've chosen not to fix it. Why do you think that is?

There's no right or wrong answer to this question (unless your name is James Gosling).

2024-11-28 Thu 20:06

Announcements RSS