Previous Contents Next
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.
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'.
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.
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.
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.
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.
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