Lab Lunch: 15 January 2019 - Mike Fourman

Title: Computation & Logic: How should we introduce our undergraduates to the foundations of informatics?

Abstract:

I have taught the first-year computation and logic course for the past five years. This year for the first time it was formally merged with the Haskell course, which has always been taught independently, but in parallel.

The core content of the CL course consists of Propositional Calculus (notation, algebra, semantics, satisfiability, DPLL) and Finite State Machines (DFA, NFA, subset construction, regex). However, I think its primary contribution is at a meta-level: to introduce students to formalisation.

In this talk I will report on this year’s experience — I tried to strengthen the connection with Haskell by implementing representations and algorithms wherever I could. In some ways this worked but, as I will describe, in others it failed.

I have started to think of changes for next year, and will present some ideas, hoping for constructive criticisms and comments. 

Two particular issues are:

  1. The traditional presentation of CL has been based on naive set theory. I am minded to  introduce a naive simple type theory instead.

  2. In their informal reasoning, students are often confused by quantification and this confusion shows in their (lack of) understanding of the propositional  semantics  (the semantics of clausal forms). I am minded to introduce explicitly the syntax and quantification over finite domains.  I hope to stimulate a productive discussion.