Haskell Road ILLC Project, June 2012
General Information about the Project
This project is a lightning course in programming in the
functional programming language Haskell. We will use The Haskell Road
to Logic, Maths and Programming [1] (see
here).
Copies of The Haskell Road will be made available to you at the
first project meeting, at the discounted price of 15 euros. You
will get your copy of the book in exchange for exact payment in
cash on the spot.
The first two weeks you will develop basic programming skills by going
through a substantial number of the programming exercises in the first
five chapters of [1]. In the third week you will develop your own
tableau-style theorem prover for first-order logic. In the fourth week
you will get a choice menu of tasks, or you can work on an
implementation task related to your own interest. The deliverable for
this final week is a documented Haskell program written in literate
style.
The overall aim of the project is to get you so familiar with Haskell
that you can use it in the future as a modelling tool for your own
logic research. It will change your life.
Prerequisites
This project is intended for students who are not yet
familiar with functional programming. Programming experience in other
languages is irrelevant (it can even harm your progress in this
project).
Reference
K. Doets and J. van Eijck. The Haskell Road to Logic, Maths and
Programming. Texts in Computing. College Publications, London, 2004.
Course Goals:
- Learn the basics of programming in Haskell.
- Learn how to write literate programs.
- Learn how to use Haskell for implementing algorithms
that arise in the context of logic.
- Learn how to use Haskell in implementation projects that
are connected with your own field of study.
Participants
Current list:
Maja Jaakson,
Riccardo Pinosio,
Alexander Block,
Jiahong Guo,
Tanmay Inamdar,
Sanne Brinkhorst,
Georgios Sarailidis,
Hans Bugge Grathwohl,
Justin Kruger,
Eric Flaten,
Nal Kalchbrenner,
Holger Brunn,
Cecilia Hernandez,
Julia Ilin.
Project Meetings Here is a provisional schedule.
All meetings will take place at CWI. You will have to ask for
access at the CWI reception desk. Rooms will be announced
here, as soon as the information becomes available.
- Tuesday June 5th, 10 am: Startup Meeting. Room L016.
Please bring 15 euros in cash to pay for your copy of The Haskell Road.
- Wednesday June 6th, 10 am. Room L016.
- Thursday June 7th, 10 am. Room L016.
- Friday June 8th: No meeting!
- Monday June 11th, 10 am. Room L016.
- Wednesday June 13th, 10 am. Room L016.
- Friday June 15th, 10 am. Room L120.
- Wednesday June 20th, 10 am. Room L016.
- Friday June 22nd, 10 am. Room L016.
Schedule for further meetings still to be determined.
Project Overview
We will treat the following,
roughly in this order:
- Getting started with functional programming
- Literate programming
- Using Haskell to do maths
- Using Haskell to do logic
- Implementing parsers for formal languages
- Implementing tableau-style theorem proving for FOL
- Implementing for your own projects
Grading
You will be graded on the basis of your deliverable for the final week.
Lecture slides, assignments, programs
Week 1
- Please bring your laptop, with
the Haskell platform installed on it. See
platform.
- You can find chapters 1 and 2 of The Haskell Road
here.
- Please read Chapters 1 and 2 of "The Haskell Road", and make notes of
everything that you do not understand.
- Instead of the Hugs interpreter
mentioned in the book, we will use the GHC interpreter, ghci.
This interpreter comes with the Haskell platform.
- Homework: Carry out all implementation exercises in
chapters 1 and 2 of the book. (Or see how far you get.) You will
need the code for the chapters, which you can find
here.
- Note: pattern matching on the pattern (x+1) is no longer
allowed in the new Haskell standard. Therefore, you will get error
messages when you want to read in the code for the first Haskell
Road chapter in ghci. This can be remedied by changing
(x+1) in the head of a definition clause into x,
and x in the body of that clause into (x-1).
- Slides of the first meeting:
Getting Started.
- Code in de slides of the first meeting:
GettingStarted.hs.
- Literate programming document:
LP.pdf, and its source:
LP.tex.
- Here is a bash (linux) script for converting from tex to
lhs. Save the following lines in a file called
lhs and make the file executable.
# produce literate haskell code from latex source code
#
cat < $1'.tex' | sed -f /ufs/jve/bin/lhsfilter.sed > $1'.lhs'
echo "Literate Haskell code written to file $1.lhs"
The part /ufs/jve/bin/lhsfilter.sed
still
has to be modified.
The script calls an auxiliary file
that contains the following lines:
s/\%\#/\#/
s/\\bc\\begin[{]verbatim[}]/\\begin\{code\}/g
s/\\end[{]verbatim[}]\\ec/\\end\{code\}/g
Save these lines in a file called lhsfilter.sed
and let the path in lhs point to it.
- Slides of the second meeting:
PropLogic.
- Code in de slides of the second meeting:
PropLogic.hs.
- During the third meeting, we discussed a function for converting formulas
of propositional logic from arrow free form into negation normal form.
A formula in negation normal form only has negation signs in front
of proposition letters. Here is the code for that:
-- precondition: input is arrowfree
nnf :: Form -> Form
nnf (Prop x) = Prop x
nnf (Neg (Prop x)) = Neg (Prop x)
nnf (Neg (Neg f)) = nnf f
nnf (Cnj fs) = Cnj (map nnf fs)
nnf (Dsj fs) = Dsj (map nnf fs)
nnf (Neg (Cnj fs)) = Dsj (map (nnf.Neg) fs)
nnf (Neg (Dsj fs)) = Cnj (map (nnf.Neg) fs)
- Extra homework: Write a function for converting formulas of
propositional logic into conjunctive normal form.
- Slides of the third meeting:
Propositional Reasoning and Proof Construction
and
Sets, Types and Lists.
- Use the tutorials at http://www.haskell.org/haskellwiki/Tutorials
to help you get started with Haskell.
- If you want to hone your skills in Haskell problem solving, have
a go at Ninety-nine
Haskell problems. Recommended!
- Challenge: ``We still lack Haskell solutions to problems
80,82,83,85,86 and 94.''
Week 2
- We will illustrate specification based testing of Haskell
programs by testing some of your CNF submissions.
- A useful piece of code for testing properties of formulas is
a random formula generator. Here is one:
RandomForms.hs. You can play with this
by adjusting the parameters. Constructing useful random datatype
generators is more art than science.
- Here is an example test file that uses this:
Test.hs. This assumes that propositional
logic code is in a file called PropLogic.hs or PropLogic.lhs,
and your CNF conversion code in a file called CNF.hs or CNF.lhs.
- My own version of the CNF converter is in
CNF.hs. So you can use this together with
PropLogic.hs to run the tests.
- The random formula generator uses the Haskell IO Monad.
See this tutorial
for an introduction. Another useful resource is
IO inside.
- A famous tool that uses random generation of test cases for property
based testing is QuickCheck. This tool is documented
here.
It is has been the inspiration for a number of similar tools for other
programming languages.
- The conversion skills for propositional logic that you are
developing will be useful for implementing theorem provers
for propositional logic and for predicate logic. We will start by
looking at resolution style and tableau style theorem proving for
propositional logic.
- Also, we have studied the concept of abstract data types, using the
implementation of sets from Chapter 4 of the Haskell Road book as
an illustration.
- Slides with an implementation of a Set datatype
in Haskell (discussed in the Monday 11 June meeting):
Ordered Pairs, Products, Sets ....
The code for SetEq.hs and Hierarchy.hs can be found on the
Haskell Road book page.
- Theorem proving exercise 1: as a preparation for resolution
style theorem proving, write a conversion tool for converting from
CNF to clause form. Here are the appropriate datatypes:
type Clause = [Int]
type Clauses = [Clause]
A precondition for correct conversion is that the indices of basic
propositions are positive integers, so that negation of
formulas in NNF can be implemented as integer negation.
- Theorem proving exercise 2: as a preparation for
tableay style theorem proving, write a conversion function for
converting propositional logic formulas from NNF to disjunctive
normal form (DNF). Only slight modifications of the CNF converter
should be necessary. Test your implementation using randomly generated
formulas.
- Theorem proving exercise 3: write a conversion tool for
converting from DNF to tableau form. Here are the appropriate
datatypes:
type Branch = [Int]
type Tableau = [Branch]
- Binary relations can be implemented in several ways. We
will look at some of them, and we will study the implementation of
important operations on relations, using material from Chapter 5 of
the Haskell Road book. Slides we discussed in class are
in Relations.
- We discussed the syntax of first order logic. Slides are in
First Order Logic. The code is in
FOL.hs.
- Theorem proving exercise 4: Implement a resolution theorem
prover for clause lists. The type of the key function is:
resolve :: [Int] -> [Clause] -> [Clause]
The first argument of resolve gives the list of indices of all
literals that occur. The output of the function is an equivalent
fully resolved clause set.
Resolution theorem proving works by applying the
resolution rule for each literal that occurs in the clause set. Once
you have resolve you can implement the rest of the prover as
follows:
lits :: Clauses -> [Int]
lits = sort . nub . concat . map (map abs)
resol :: Clauses -> Clauses
resol cls = resolve (lits cls) cls
simplify :: Form -> Clauses
simplify f = resol (cls (Neg f))
thm :: Form -> Bool
thm f = simplify f == [[]]
- FOL exercise 1: Implement a function that collects the variables
that have free occurrences in a given formula.
The type declaration for your function is:
freeVarsInForm :: Form -> [Id]
- FOL exercise 2: Extend the definition of applying a substitution
to formulas. The type declaration for your function is:
appF :: Subst -> Form -> Form
Week 3
- The tutorial on theorem proving is in
TOTP.pdf. The code of the tutorial is
in TOTP.hs.
- Your task for this week is to solve as many of the implementation
exercises in this paper as you can.
- Friday June 22nd: Parsing.
Deadlines
- Homework for the first week: the implementation exercises from
the two first chapters of The Haskell Road, plus the CNF conversion
exercise for propositional formulas (see above). Deadline for this
has passed.
- Deadline for the three theorem proving exercises for the second week:
has passed.
- Deadline for the fourth theorem proving exercise and the two FOL
exercises: Friday June 15th, before the beginning of the meeting.
- Homework for the second week: exercises 4.44, 4.47, 4.48, 4.49,
4.50, 4.54, 4.55, 5.54, 5.55, 5.56 from the Haskell Road book.
Deadline for this: Wednesday June 20th, before the beginning of the meeting.
- Homework for third week: theorem proving exercises from the Tutorial
on Theorem Proving. Deadline: Monday June 25, 10 am.
- Homework exercises have to be mailed to
Jan van Eijck.
There are no further constraints on the format of your submission,
as long as it is comprehensible (for me).
Week 4: special topics.