Incremental development is fun. I've just added support for branching as required to implement the disjunction and implication rules of my propositional calculus and it's been quite interesting to see just how easy a functional programming language makes with sort of exploratory approach to design and development.
Once I've got this up and running (all I need to do is add a check for contradiction), I'll refactor it to be a little neater, write a parser and generator that supports all of the features and get an initial, pre-alpha, demonstration version posted.
Hopefully that'll be in the next two or three days.
Monday, June 27, 2005
Friday, June 24, 2005
Another Night's Worth of Code
I've just finished the first major part of my first step along the road to [real] implementation: I now have a working type for propositional calculus, a simple representation of a tableau branch, can saturate said branch (modulo the rules which branch) and generate a model (which is simply a list of literals at this point).
Next, I need to extend this tableau implementation to support branching and then complete the logic with correct rules for branching connectives (disjunction and implication). Once that is done, I'll rewrite my language parser and code generator so that I can actually generate this implementation of the propositional calculus from the definition.
Once that is done, I'll move on to the basic propositional modal logic: K. Getting K to work will require that I implement labels, relations and extend my language so that it can import and extend existing logics. Once that is done, I'll move onto a more complex modal logic (perhaps S4) before tackling intuitionistic logic (which uses two-part labels).
Next, I need to extend this tableau implementation to support branching and then complete the logic with correct rules for branching connectives (disjunction and implication). Once that is done, I'll rewrite my language parser and code generator so that I can actually generate this implementation of the propositional calculus from the definition.
Once that is done, I'll move on to the basic propositional modal logic: K. Getting K to work will require that I implement labels, relations and extend my language so that it can import and extend existing logics. Once that is done, I'll move onto a more complex modal logic (perhaps S4) before tackling intuitionistic logic (which uses two-part labels).
Reusing Throwaway Code
I've just had my first go at writing a monad, and it's harder than it would seem. As a result of my moderately dismal failure, I've decided to go back and actually read the monads sections of the various Haskell tutorials (the Gentle Introduction, Yet Another Haskell Tutorial, and anything else I find laying around on my hard disc). I've just been looking at Yet Another Haskell Tutorial and the section on computations (Section 8.4.2 in the PDF) defines a small graph library which might be a useful starting point when I need to start dealing with transitive, Euclidean and even more bizarre frames and rules with conditions on them.
In one section, I get some [hopefully] usable code, and a better understanding of monads.
In one section, I get some [hopefully] usable code, and a better understanding of monads.
Thursday, June 23, 2005
[Haskell-cafe] Re: Using type classes for polymorphism of data constructors
[Haskell-cafe] Re: Using type classes for polymorphism of data constructors
A message on the Haskell-cafe mailing list gives an alternative (better, even) approach to the polymorphism of formulæ using differential types. It works just as well as my solution, and results in much more complex (and therefore complete) types:
I'll probably wind up using a version based on Ralf's example, unless I run into problems.
A message on the Haskell-cafe mailing list gives an alternative (better, even) approach to the polymorphism of formulæ using differential types. It works just as well as my solution, and results in much more complex (and therefore complete) types:
Main> :t (Impl (Prop "p") (Poss (Prop "p")))
Impl (Prop "p") (Poss (Prop "p")) :: PC2 PC0 (Modal1 PC0)I'm not yet sure which route I'll take. My approach results in a single data type (PC, Modal, etc) for each language, which is good, but the types don't mean much and it isn't Haskell-98 (or, at least, Hugs won't load it as such). Ralf's approach also works, the types is assigns formulæ contain more information and it is Haskell-98.I'll probably wind up using a version based on Ralf's example, unless I run into problems.
Goals: the Motivation of Procrastination
So far, I have:
- written a parser for my logic definition language;
- solved the problem I was having with polymorphism;
- designed, in the large, my data structures; and
- thought about name for the project.
- define a state monad (to model the saturation of a branch);
- define a backtracking monad (to model the branching of non-deterministic choices);
- find a way to compose them (perhaps by deriving a monad transformer);
- finalise the structure of the logic modules;
- write a realistic (perhaps even production) parser and code generator for the logics;
- learn to use hs-plugins to write dynamically loadable modules (and find a way to make logic modules dynamically loadable); and
- implement some representative test logics (propositional calculus, K, intuitionistic logic, something with transitive frames, etc).
Wednesday, June 22, 2005
Polymorphism and Generality Redux; or The Beneficial Side Effects of Reading
I've started looking at how to code my backtracking monad (the framework that will provide the branching, failure, etc within which the tableau method for each logic will be implemented). To try to get a handle on the subject, I've started looking at Deriving Backtracking Monad Transformers by Ralf Hinze.
Section 3 of the paper defines an abnormal termination (i.e. exceptions) monad and 3.1 begins to define a transformer to extend an arbitrary monad with exceptions. As part of this, it uses an existentially quantified type variable in the definition of a type constructor (for :>>=). Needless to say, the similarity to my previous attempts to make polymorphic formulae was obvious.
Although I'm still, by any meaningful standard, a Haskell novice and haven't looked at this extension before, I've managed to extend that example (by restricting the type variable to members of my Formula type class) and Hey, Presto! I can now create polymorphic types representing my inter-mixable logical languages.
As an example, I've got a type PC for the propositional calculus, and a type < span style="font-family: monospace;" >Modal for alethic modal logic. The connectives of each language can take formulae of either type (or both) as parameters, and everything Just WorksTM.
Polymorphism, they way it was intended.
Section 3 of the paper defines an abnormal termination (i.e. exceptions) monad and 3.1 begins to define a transformer to extend an arbitrary monad with exceptions. As part of this, it uses an existentially quantified type variable in the definition of a type constructor (for :>>=). Needless to say, the similarity to my previous attempts to make polymorphic formulae was obvious.
Although I'm still, by any meaningful standard, a Haskell novice and haven't looked at this extension before, I've managed to extend that example (by restricting the type variable to members of my Formula type class) and Hey, Presto! I can now create polymorphic types representing my inter-mixable logical languages.
As an example, I've got a type PC for the propositional calculus, and a type < span style="font-family: monospace;" >Modal for alethic modal logic. The connectives of each language can take formulae of either type (or both) as parameters, and everything Just WorksTM.
Polymorphism, they way it was intended.
Thursday, June 16, 2005
Meta-post: Inward Links.
Wow, this blog has been mentioned in both Consequently (Greg Restall's blog) and That Logic Blog (Jon Cohen's blog).
Now I'll just have to get some meaningful posts up.
Now I'll just have to get some meaningful posts up.
Saturday, June 11, 2005
Hello, I'll be your host tonight as we play...
Name that Project...
My project is in need of a name. Rather than give it an acronym, I've been trying to think of a name at least somewhat relevant to the topic at hand and my approach. I'm currently thinking about "Vindaloo" with the rather tenuous link being Haskell Curry and that the project will, I hope, be pretty hot (for some definition). "Vindaloo," though, doesn't have all that much to do with modal logic.
Names have never been a strong point of mine (I still don't know the names of many of the people I've seen and talked to every day this year), so I'll take this opportunity to solicit suggestions: If you can think of a name for a labelled tableaux theorem prover written in the Haskell programming language please leave your suggestions in a comment, or email them to me at: thsutton at gmail dot com.
My project is in need of a name. Rather than give it an acronym, I've been trying to think of a name at least somewhat relevant to the topic at hand and my approach. I'm currently thinking about "Vindaloo" with the rather tenuous link being Haskell Curry and that the project will, I hope, be pretty hot (for some definition). "Vindaloo," though, doesn't have all that much to do with modal logic.
Names have never been a strong point of mine (I still don't know the names of many of the people I've seen and talked to every day this year), so I'll take this opportunity to solicit suggestions: If you can think of a name for a labelled tableaux theorem prover written in the Haskell programming language please leave your suggestions in a comment, or email them to me at: thsutton at gmail dot com.
Polymorphism and Generality
One of the main goals of this project, to my mind at least, is generality. The prover must be easily extendable with support for a wide range (ideally, the entire range) of labelled tableaux calculi. Furthermore, it ought to be possible to define new logics as extensions to existing logics: propositional modal logic, for example, is an extension of the propositional calculus to support two new operators: ◇ and □.
Unfortunately, I've not been able to get determine just how to get this level of flexibility to work under Haskell's type system. I've asked the Haskell-cafe mailing list for pointers and, in the mean time, have moved on to doing this composition in the compiler for my mini-language rather than in the generated Haskell code.
Hopefully, I'll get this to work as it will be quite useful and, unless I'm mistaken, interesting.
Unfortunately, I've not been able to get determine just how to get this level of flexibility to work under Haskell's type system. I've asked the Haskell-cafe mailing list for pointers and, in the mean time, have moved on to doing this composition in the compiler for my mini-language rather than in the generated Haskell code.
Hopefully, I'll get this to work as it will be quite useful and, unless I'm mistaken, interesting.
Friday, June 10, 2005
Data Structures
I'm getting to the point where I'll have to start thinking about the data structures used to implement my tableaux. They need to be as small as possible and allow fast membership testing and updating. As my current goal is to accept a formula to prove and produce either a counter-model or a "yes" as output. As such, I will only ever need access to those parts of the tree on the path from the current node, to the root. The tree is, essentially, the progress of the computation backtracking over time.
As such, I'm looking forward to trying to write the run-time (once I've finished figuring out how the logic-specific code the DSL will be transformed into will work). It will require a bit of input handling (in the IO monad), parsing (in the Parser monad) and backtracking (in some backtracking monad) along with some state (perhaps a State monad, perhaps built into the backtracking monad) and a whole bunch of lazy computation (the actual tableau rules).
Unless I am overlooking something (I'm sure I am and I imagine that Raj and Pietro agree), my main data structure will be...
a list. The main rationale behind this decision (rather than trying to build some sort of tree structure, or some bizarre nested set-like structure) is that, as I'm merely trying to build a model, the tree itself is expressed in the computation (or, rather, its backtracking). Furthermore, as I'm working with labelled tableaux (with an explicit modal relation), all I need to construct a model once I've found an open branch is the list of formulæ (and relations) from the end of that branch, to the root of the tree.
In Haskell, lists act like (and probably are) singly linked lists of cons cells with a pointer to the item, and one to the rest of the list. This means that you can add stuff to the front of a list without modifying the original list. This is rather helpful as it means that we can add junk onto one end of a list, which is what we'll be doing with tableaux (adding things to the end of the branch), and you can have multiple lists sharing the same tail (to give an right-way-up tree structure, like an upside-down tableau or a sequent proof). As we're going to be doing backtracking (because we can through away everything we don't need to write a model), and we've got a ready-made tree structure that can be extended at the leaves, there is a very simple way to code it all up: as a monad (for the backtracking) over the list pointers.
Using a monad (probably a MonadPlus) to implement backtracking will allow us to express branching naturally (using mzero "fail" on branch closure and mplus to do the "branching" evaluation) and if we add in a little state to each branch (a pointer to the current head of the list, for instance) we have a backtracking model search procedure. All that remains is to implement it (no doubt discovering that my understanding of monads is completely wrong) and find out which mountains I need to move to get this approach to work for the non-simple case...
As such, I'm looking forward to trying to write the run-time (once I've finished figuring out how the logic-specific code the DSL will be transformed into will work). It will require a bit of input handling (in the IO monad), parsing (in the Parser monad) and backtracking (in some backtracking monad) along with some state (perhaps a State monad, perhaps built into the backtracking monad) and a whole bunch of lazy computation (the actual tableau rules).
Unless I am overlooking something (I'm sure I am and I imagine that Raj and Pietro agree), my main data structure will be...
a list. The main rationale behind this decision (rather than trying to build some sort of tree structure, or some bizarre nested set-like structure) is that, as I'm merely trying to build a model, the tree itself is expressed in the computation (or, rather, its backtracking). Furthermore, as I'm working with labelled tableaux (with an explicit modal relation), all I need to construct a model once I've found an open branch is the list of formulæ (and relations) from the end of that branch, to the root of the tree.
In Haskell, lists act like (and probably are) singly linked lists of cons cells with a pointer to the item, and one to the rest of the list. This means that you can add stuff to the front of a list without modifying the original list. This is rather helpful as it means that we can add junk onto one end of a list, which is what we'll be doing with tableaux (adding things to the end of the branch), and you can have multiple lists sharing the same tail (to give an right-way-up tree structure, like an upside-down tableau or a sequent proof). As we're going to be doing backtracking (because we can through away everything we don't need to write a model), and we've got a ready-made tree structure that can be extended at the leaves, there is a very simple way to code it all up: as a monad (for the backtracking) over the list pointers.
Using a monad (probably a MonadPlus) to implement backtracking will allow us to express branching naturally (using mzero "fail" on branch closure and mplus to do the "branching" evaluation) and if we add in a little state to each branch (a pointer to the current head of the list, for instance) we have a backtracking model search procedure. All that remains is to implement it (no doubt discovering that my understanding of monads is completely wrong) and find out which mountains I need to move to get this approach to work for the non-simple case...
Advice, Suggestions and Supervision
I've just had a talk with Pietro about my project and directions in which I might move it. Pietro's PhD project (the Tableaux Work Bench) is written in OCaml (an eager functional programming language) and works with implicit tableaux. My Honours project (which needs a name, suggestions are welcome) is written in Haskell (a lazy, pure functional language) and works with labelled tableaux.
In spite of these differences, the projects are quite similar and Pietro's advice and suggestions are going to be invaluable. In our meeting, we discussed the data structures I am planning on using which has helped solidify my thoughts, which I shall write up and post this evening.
In spite of these differences, the projects are quite similar and Pietro's advice and suggestions are going to be invaluable. In our meeting, we discussed the data structures I am planning on using which has helped solidify my thoughts, which I shall write up and post this evening.
Parsing stuff in Haskell
I've just started looking parsing in Haskell with Parsec. After a few hours of reading the documentation (PDF, 424K)and poking at the examples, I've managed to hack together a parser for my little language.
Only a few hours after I started looking at Parsec, I've got a prototype which generates code in an abstract syntax suitable for passing to a semantics checker and code generator (the system will generate Haskell from specs written in my DSL, which is then linked against some infrastructure). Very cool. Haskell is great for my productivity.
Only a few hours after I started looking at Parsec, I've got a prototype which generates code in an abstract syntax suitable for passing to a semantics checker and code generator (the system will generate Haskell from specs written in my DSL, which is then linked against some infrastructure). Very cool. Haskell is great for my productivity.
Monday, June 06, 2005
About Labelled Tableaux
On this blog I will chronicle the work on my Honours project in computer science: developing a system to construct counter-models for non-theorems of modal logics. This system will be a small theorem prover based on tableaux, written in Haskell.
I will link to relevant papers and technical reports, technical details which I encounter whilst coding, material that I make available to download, and anything else in the slightest bit relevant to the topic at hand.
I will link to relevant papers and technical reports, technical details which I encounter whilst coding, material that I make available to download, and anything else in the slightest bit relevant to the topic at hand.
Subscribe to:
Posts (Atom)