# Quiz (Week 1)

## Table of Contents

## 1 Computability

#### 1.0.1 Question 1

Which of the following is *not* equivalent according to the Church-Turing
thesis?

- ✗Turing Machines
- ✗Recursive Functions
- ✔Propositional Logic
- ✗Lambda Calculus

Propositional logic is not powerful enough to be Turing-complete. This has its advantages: because it's not equivalent to a turing machine, we can solve the Entscheidungsproblem for propositional logic. That is, given a propositional logic formula, we can write a program to determine if that formula is true or not. For any more sophisticated logic, such as first order logic or higher order logic (which is directly built on the lambda calculus), this becomes impossible.

#### 1.0.2 Question 2

Which one of the following problems is computable, that is, can be decided by a computer program?

- ✗Determining if a program will divide by zero
- ✗Determining if a program exhibits undefined behaviour
- ✗Determining if a program has any index-out-of-bound bugs
- ✔Determining if a program has a type error

Note: For these answers, a "program" refers to a program in a Turing-complete language with a type system, such as C, Java or Haskell.

A type error is detected by the compiler following *syntactic* rules.
All the other answers would require a solution to the halting problem, which
is undecidable.

## 2 Logic

#### 2.0.1 Question 3

For which values of \(A\) and \(B\) (listed below, choose one or more) does the boolean expression \(\neg (A \Rightarrow B) \lor \neg B\) evaluate to \(\mathit{True}\)?

- ✔\(A\) false, \(B\) false.
- ✔\(A\) true, \(B\) false.
- ✗\(A\) false, \(B\) true.
- ✗\(A\) true, \(B\) true.

The \(\neg B\) disjunct makes answers 1 and 2 instantly correct. The first disjunct, \(\neg (A \Rightarrow B)\), is by logic, equivalent to \(\neg (\neg A \lor B)\). Following de Morgan's law, we get \(\neg \neg A \land \neg B\), which by Double Negation Elimination is the same as \(A \land \neg B\), which is already covered by case 2.

Later on in the course we will look at logics that are *constructive*.
In these logics, principles such as double negation elimination don't hold.

#### 2.0.2 Question 4

Check all of the following expressions that are equivalent to the expression \((A \Rightarrow B) \lor (B \Rightarrow A)\).

- ✔\(\mathit{True}\)
- ✗\(\mathit{False}\)
- ✗\(A \land B\)
- ✗\(A \lor B\)
- ✗\(A \Leftrightarrow B\)

By logic we can translate the implications to disjunctions, giving us: \((\neg A \lor B) \lor (\neg B \lor A)\). Shuffling the terms around we get \((\neg A \lor A) \lor (\neg B \lor B)\), which by the law of the excluded middle is just \(\mathit{True} \lor \mathit{True}\), thus \(\mathit{True}\) by absorption.

It cannot be equivalent to \(\mathit{False}\) as we can make it true by making
\(A\) and \(B\) true. Nor is it equivalent to \(A \land B\), as in the case where \(A\) is
true but \(B\) is false, for example. Nor is it equivalent to \(A \lor B\), with
the case where both \(A\) and \(B\) are false. It also isn't equivalent to
\(A \Leftrightarrow B\), as that is equivalent to the *conjunction* of the
two implications, not the *disjunction*.

## 3 Lambda Calculus

#### 3.0.1 Question 5

Select all expressions that are α-equivalent to \((\lambda x. x\ y)\):

- ✔\((\lambda x. x\ y)\)
- ✗\((\lambda y. y\ y)\)
- ✔\((\lambda z. z\ y)\)
- ✗\((\lambda x. x\ z)\)
- ✗\((\lambda y. y\ x)\)
- ✗\((\lambda x. (\lambda z. z)\ x\ y)\)

The rules for α-conversion states that we can only rename *bound*
variables, not *free* ones. This means that we can only rename \(x\), not \(y\).
This instantly rules out 4 and 5. Furthermore, 6 is ruled out easily as we
can see that β-reduction is required, and the question only calls for
α-conversion. Option 2 can be ruled out because by renaming \(x\) to \(y\)
we cause the originally free variable \(y\) to refer instead to the bound
variable formerly known as \(x\), resulting in a semantically different
expression. This leaves options 1 and 3. Option 1 is α-equivalent
as it is identical. Option 3 is α-equivalent as the only change
is the renaming of the bound variable \(x\) to \(z\).

#### 3.0.2 Question 6

If I apply β-reduction as much as possible to the following expression, which expression do I get as a result?

\begin{equation*} (\lambda x. \lambda y. x\ y\ x)\ (\lambda a. \lambda b. a)\ (\lambda m. \lambda n. n) \end{equation*}- ✗\((\lambda a. \lambda b. a)\)
- ✔\((\lambda m. \lambda n. n)\)
- ✗\((\lambda b. \lambda n. n)\)
- ✗\((\lambda x. \lambda y. x\ y\ x)\ (\lambda a. \lambda b. a)\ (\lambda m. \lambda n. n)\)

If you answered option 3, it's likely that you are reading function application as being right-associative. It is in fact left-associative, that is \(a\ b\ c\) is the same as \((a\ b)\ c\).

#### 3.0.3 Question 7

Through the use of *church encodings*, we can define booleans in lambda calculus as
follows:

With this definition, the \(\mathbf{T}\) function will always return its first argument, and
the \(\mathbf{F}\) function will always return its second argument. Thus, a traditional
`if`

expression \(\mathsf{if}\ p\ \mathsf{then}\ x\ \mathsf{else}\ y\) can be written
as just \(p\ x\ y\).

We can define a boolean \(\mathbf{AND}\) operator (written `&&`

in C) for logical
conjunction as follows:

What would be a suitable definition for \(\mathbf{OR}\)?

- ✗\((\lambda p. \lambda q. q\ p\ q)\)
- ✗\((\lambda p. \lambda q. q\ p\ p)\)
- ✗\((\lambda p. \lambda q. p\ q\ q)\)
- ✔\((\lambda p. \lambda q. p\ p\ q)\)

Option 1 is just a symmetric version of \(\mathbf{AND}\). Options 2 and 3 both just always return \(p\) or \(q\) respectively.

Option 4 can be read as \((\lambda p. \lambda q. \mathsf{if}\ p\ \mathsf{then}\ p\ \mathsf{else}\ q)\) which is a satisfactory definition for \(\mathbf{OR}\).

#### 3.0.4 Haskell Setup

For the purposes of statistics gathering, please select the toolchain that you have successfully
configured and tested on your *usual working environment*
(be it your own laptop, desktop or on CSE machines/servers). For more information, please
see the Haskell Setup instructions.

- ✔GHC w/ Cabal on CSE machines using 3141 account binaries.
- ✔Haskell for Mac.
- ✔A
`stack`

based setup on my own computer. - ✔Some other, not recommended setup.

If you selected option 4, we will provide no support and you must accept full responsibility for maintaining your toolchain. You have been warned.