Previous Contents Next

She Turned me into a Newt!

Chapter 14: She Turned me into a Newt!

After the difficult and heavy-going chapters about Gordon's Computer, it is time for Something Completely Different (as they used to say). This is essentially an excuse for some light relief - though there is one serious point at the end.

14.1. Background: Monty Python and the Holy Grail

Since many of you are not from the UK, and most of the rest of you may be too young to have seen this film, a bit of background is called for. Monty Python and the Holy Grail was a film in which King Arthur and assorted Knights of the Round Table search for the Holy Grail (a mythical Christian relic - a Grail is a cup). This is based on the Arthurian Legend, which forms part of the History of the Kings of England, written by Geoffrey of Monmouth in 1136. Geoffrey was of Welsh, or Welsh/Breton descent - not an exceptional combination since the native language of Brittany is very closely related to Welsh (it is one of the P-Celtic languages along with Welsh and Cornish). Geoffrey's 'History' purports to tell the history of British kings from 1100 BC to 689 AD. It is more or less all made up - for example, it starts with the arrival of Aeneas in Britain, who founds a dynasty of kings which supposedly leads to a civilisation of equal standing to Greece and Rome. (Aeneas is a figure from Homer's Iliad, about the seige of Troy, who was popular in classical literature - for example, Virgil's Aeneid.) Despite being basically fiction, Geoffrey's History was taken as true for about 600 years - and was massively popular in Britain and Continental Europe - before being seriously questioned by the academic world (though there are earlier figures who clearly did not believe it - for example, Gerald of Wales). The Arthurian Legend - including the Holy Grail - forms a very substantial part of the History. Determining what, if any, of it is based in fact is still a semi-serious topic of research.

There have been many retellings of the story since it was written. As you might expect, the Python version does not stick all that closely to the text... It is a bizarre journey through an absurd medieval world in which Arthur and the Knights blunder about - some of them coming to a sticky end en route - before the survivors are finally arrested. In one scene, some villagers want to burn a 'witch'.

14.1.1. The Witch Scene

A group of village idiot types are attempting burn a woman that they claim to be witch. Sir Bedevere arrives on the scene, and asks them why. They first claim that she looks like a witch - and she points out that they dressed her up. The grudgingly admit this, and then make some more outrageous claims (one says that she turned him into a newt - though he later 'got better'). Sir Bedevere then talks them through the 'logic' for checking that she is a witch - and after some false turns and lots of dim stares, they come to the following basic conclusions.

  1. Witches Burn. This one is fair enough - though the villagers suggest trying to actually burn her as way of testing this.
  2. Wood Burns. Hence witches are made of wood. How do you check that she is made of wood? Try building a bridge out of her, one suggests - but Bedevere points out that you can also make bridges from stone.
  3. Wood Floats. Bedevere gently leads them to this point, and asks them if they know anything else that floats.
  4. Ducks Float. They actually have a lot of trouble thinking of something else that floats - and it is Arthur, who has just arrived on the scene, who says: 'A Duck!' (stunned amazement and dramatic music.)
  5. Therefore... The logic goes: that if she weighs the same as a duck, she's a witch and they can burn her. So they put her on a set of scales with a duck, and of course she does weigh the same ('it's a fair cop').

How does the logic here work out? We can model it in Maude. Note that I cannot claim to have thought of using this example, though I did independently reconstruct it in Maude (I lost the original version years ago). It was originally proposed as a more interesting example of computer-based logic checking than the 'usual' ones.

14.2. The Maude Version

This is a somewhat different application of Maude than previous ones - we have so far just been interested in modelling systems. Now, we are going to do some logic (as a exercise, if you have lots of time on your hands, you might want to try this in Prolog).

Here is the Maude code


fmod WITCH is

    *** Anything can be a thing - duck, witch etc.
    sort Thing .
    
    *** Represents the weight of an object
    sort Weight .
  
    *** true if a thing floats
    op floats : Thing -> Bool .
    
    *** true if a thing is made of wood
    op isWood : Thing -> Bool .
    
    *** true is Thing burns
    op burns : Thing -> Bool .
    
    *** true if a Thing is a witch
    op isWitch : Thing -> Bool .

    *** Returns the weight of a Thing
    op weight : Thing -> Weight .
    
    *** Equality operator for Things
    op _===_ : Weight Weight -> Bool .
    
    *** Constant representing the possible witch
    op witch? : -> Thing .

    *** Constant for the duck
    op duck : -> Thing .
    
    vars x y : Thing .

    *** The assumptions
    eq floats(duck) = true .
    eq weight(witch?) === weight(duck) = true .

    *** The rules
    ceq isWood(x) = true if floats(x) == true .
    ceq burns(x) = true if isWood(x) == true .
    ceq isWitch(x) = true if burns(x) == true .
    ceq floats(x) = true if floats(duck) and
                        (weight(x) === weight(duck)) .
endfm

So is she a witch? Here is the important reduction.


Maude> red isWitch(witch?) .
reduce in WITCH : isWitch(witch?) .
rewrites: 10 in -10ms cpu (0ms real) (~ rewrites/second)
result Bool: true

Yes, she is - which might be a bit surprising. There is nothing wrong with the logic - it is some of the assumptions that are nonsense.

(Incidentally, if you try reducing isWitch(duck), you will find that ducks are witches too.)

The serious point that comes out of this is: you cannot expect tools like mathematical logic (or software based on it) to give sensible results without sensible initial assumptions This is a restatement of the old Computer Science saying: 'Garbage In, Garbage Out', or GIGO.

14.2.1. Small Confession

For completeness, I should own up to cheating slightly in the example above. The problem is the line


    ceq floats(x) = true if floats(duck) and
                        (weight(x) === weight(duck)) .

Although this is true, I have effectively manually made one computation step which in an ideal world the system would accomplish itself. It would have been better to be able to write something like


    ceq floats(x) = true if there exists a y such that
                        floats(y) and
                        (weight(x) === weight(y)) .

That is, let the system work out that there is something that is known to float (i.e a duck). You can express such things in Maude, but it requires meta-level code and is beyond this module.

14.3. Another Version: Membership Axioms

It is also possible to encode most of the 'logic' in the witch example using membership axioms. In fact, the resulting code (here) requires less rewrites - though the total work is similar because of the need to check the membership axioms. Here is the code.


fmod WITCH is

    *** Anything can be a thing - duck, witch etc.
    sort Thing .
    
    *** Sorts for *particular* things
    sorts Witch Burns Wood Floats .

    *** Represents the weight of an object
    sort Weight .

    *** The subsort relationships
    subsort Witch < Burns < Wood < Floats < Thing .

    op weight : Thing -> Weight .

    *** Equality operator for Things
    op _===_ : Weight Weight -> Bool .

    *** Constant for the duck
    op duck : -> Floats .

    *** Constant for the possible witch
    op witch? : -> Thing .

    var wood : Wood .
    var burn : Burns .
    var witch : Witch .
    var floats : Floats .
    var x : Thing .
  
    *** The membership axioms now capture most of the
    *** 'logic'
    mb wood : Burns .
    mb floats : Wood .
    mb burn : Witch .
    cmb x : Floats if (weight(x) === weight(duck)) .

    eq weight(witch?) === weight(duck) = true .

endfm

The faulty logic might be clearer here. The subsort relationships say that:

These are all fine - but then some of the membership axioms are false.

Here is what happens when we type the reduction.


Maude> red witch? .
reduce in WITCH : witch? .
rewrites: 3 in -10ms cpu (0ms real) (~ rewrites/second)
result Witch: witch?

We have just asked Maude to reduce the constant witch? - and it has worked out that it is actually of sort Witch. (Incidentally, ducks are still witches in this version.)

Previous Contents Next