177 lines
7.0 KiB
Plaintext
177 lines
7.0 KiB
Plaintext
// First, let's give some type-variables some values:
|
|
Nationality = Englishman | Swede | Dane | Norwegian | German
|
|
Colour = Red | Green | Yellow | Blue | White
|
|
Cigarette = PallMall | Dunhill | BlueMaster | Blend | Prince
|
|
Domestic = Dog | Bird | Cat | Zebra | Horse
|
|
Beverage = Tea | Coffee | Milk | Beer | Water
|
|
HouseRow = First | Second | Third | Fourth | Fifth
|
|
|
|
{
|
|
We use injections to make the array-elements unique.
|
|
Example: 'Pet' is an array of unique elements of type 'Domestic', indexed by 'Nationality'.
|
|
In the predicate 'Zebra', we use this injection 'Pet' to define the array-variable 'pet'
|
|
as a parameter of the 'Zebra'-predicate.
|
|
The symbol used is the '->>'. 'Nationality->>Domestic' can be read as 'Domestic(Nationality)'
|
|
in "plain array-speak";
|
|
the difference being that the elements are by definition unique (cf. 'injective function').
|
|
|
|
So, in FormulaOne we use a formula like: 'pet(Swede) = Dog', which simply means that the 'Swede'
|
|
(type 'Nationality') has a 'pet' (type 'Pet', of type 'Domestic', indexed by 'Nationality'),
|
|
which appears to be a 'Dog' (type 'Domestic').
|
|
Or, one could say that the 'Swede' has been mapped to the 'Dog' (Oh, well...).
|
|
}
|
|
|
|
Pet = Nationality->>Domestic
|
|
Drink = Nationality->>Beverage
|
|
HouseColour = Nationality->>Colour
|
|
Smoke = Nationality->>Cigarette
|
|
HouseOrder = HouseRow->>Nationality
|
|
|
|
pred Zebra(house_olour::HouseColour, pet::Pet, smoke::Smoke, drink::Drink, house_order::HouseOrder) iff
|
|
|
|
// For convenience sake, some temporary place_holder variables are used.
|
|
// An underscore distinguishes them:
|
|
|
|
house_colour(green_house) = Green &
|
|
house_colour(white_house) = White &
|
|
house_colour(yellow_house) = Yellow &
|
|
smoke(pallmall_smoker) = PallMall &
|
|
smoke(blend_smoker) = Blend &
|
|
smoke(dunhill_smoker) = Dunhill &
|
|
smoke(bluemaster_smoker) = BlueMaster &
|
|
pet(cat_keeper) = Cat &
|
|
pet(neighbour_dunhill_smoker) = Horse &
|
|
|
|
{ 2. The English man lives in the red house: }
|
|
house_colour(Englishman) = Red &
|
|
|
|
{ 3. The Swede has a dog: }
|
|
pet(Swede) = Dog &
|
|
|
|
{ 4. The Dane drinks tea: }
|
|
drink(Dane) = Tea &
|
|
|
|
{ 'smoke' and 'drink' are both nouns, like the other variables.
|
|
One could read the formulas like: 'the colour of the Englishman's house is Red' ->
|
|
'the Swede's pet is a dog' -> 'the Dane's drink is tea'.
|
|
}
|
|
|
|
{ 5. The green house is immediately to the left of the white house.
|
|
The local predicate 'LeftOf' (see below) determines the house order: }
|
|
LeftOf(green_house, white_house, house_order) &
|
|
|
|
{ 6. They drink coffee in the green house: }
|
|
drink(green_house) = Coffee &
|
|
|
|
{ 7. The man who smokes Pall Mall has birds: }
|
|
pet(pallmall_smoker) = Bird &
|
|
|
|
{ 8. In the yellow house they smoke Dunhill: }
|
|
smoke(yellow_house) = Dunhill &
|
|
|
|
{ 9. In the middle house (third in the row) they drink milk: }
|
|
drink(house_order(Third)) = Milk &
|
|
|
|
{10. The Norwegian lives in the first house: }
|
|
house_order(First) = Norwegian &
|
|
|
|
{11. The man who smokes Blend lives in the house next to the house with cats.
|
|
Another local predicate 'Neighbour' makes them neighbours: }
|
|
Neighbour(blend_smoker, cat_keeper, house_order) &
|
|
|
|
{12. In a house next to the house where they have a horse, they smoke Dunhill: }
|
|
Neighbour(dunhill_smoker, neighbour_dunhill_smoker, house_order) &
|
|
|
|
{13. The man who smokes Blue Master drinks beer: }
|
|
drink(bluemaster_smoker) = Beer &
|
|
|
|
{14. The German smokes Prince: }
|
|
smoke(German) = Prince &
|
|
|
|
{15. The Norwegian lives next to the blue house
|
|
Cf. 10. "The Norwegian lives in the first house", so the blue house is the second house: }
|
|
house_colour(house_order(Second)) = Blue &
|
|
|
|
{16. They drink water in a house next to the house where they smoke Blend: }
|
|
drink(neighbour_blend_smoker) = Water &
|
|
Neighbour(blend_smoker, neighbour_blend_smoker, house_order)
|
|
|
|
{ A simplified solution would number the houses 1, 2, 3, 4, 5
|
|
which makes it easier to order the houses.
|
|
'right in the center' would become 3; 'in the first house', 1
|
|
But we stick to the original puzzle and use some local predicates.
|
|
}
|
|
|
|
local pred Neighbour(neighbour1::Nationality, neighbour2::Nationality, house_order::HouseOrder)iff
|
|
neighbour1 <> neighbour2 &
|
|
house_order(house1) = neighbour1 &
|
|
house_order(house2) = neighbour2 &
|
|
( house1 = house2 + 1 |
|
|
house1 = house2 - 1 )
|
|
|
|
local pred LeftOf(neighbour1::Nationality, neighbour2::Nationality, house_order::HouseOrder) iff
|
|
neighbour1 <> neighbour2 &
|
|
house_order(house1) = neighbour1 &
|
|
house_order(house2) = neighbour2 &
|
|
house1 = house2 - 1
|
|
|
|
{
|
|
The 'all'-query in FormulaOne:
|
|
all Zebra(house_colour, pet, smokes, drinks, house_order)
|
|
gives, of course, only one solution, so it can be replaced by:
|
|
one Zebra(house_colour, pet, smokes, drinks, house_order)
|
|
}
|
|
|
|
// The compacted version:
|
|
|
|
Nationality = Englishman | Swede | Dane | Norwegian | German
|
|
Colour = Red | Green | Yellow | Blue | White
|
|
Cigarette = PallMall | Dunhill | BlueMaster | Blend | Prince
|
|
Domestic = Dog | Bird | Cat | Zebra | Horse
|
|
Beverage = Tea | Coffee | Milk | Beer | Water
|
|
HouseRow = First | Second | Third | Fourth | Fifth
|
|
|
|
Pet = Nationality->>Domestic
|
|
Drink = Nationality->>Beverage
|
|
HouseColour = Nationality->>Colour
|
|
Smoke = Nationality->>Cigarette
|
|
HouseOrder = HouseRow->>Nationality
|
|
|
|
pred Zebra(house_colour::HouseColour, pet::Pet, smoke::Smoke, drink::Drink, house_order::HouseOrder) iff
|
|
|
|
house-colour(green_house) = Green &
|
|
house-colour(white_house) = White &
|
|
house-colour(yellow_house) = Yellow &
|
|
smoke(pallmall_smoker) = PallMall &
|
|
smoke(blend_smoker) = Blend &
|
|
smoke(dunhill_smoker) = Dunhill &
|
|
smoke(bluemaster_smoker) = BlueMaster &
|
|
pet(cat_keeper) = Cat &
|
|
pet(neighbour_dunhill_smoker) = Horse &
|
|
house_colour(Englishman) = Red &
|
|
pet(Swede) = Dog &
|
|
drink(Dane) = Tea &
|
|
LeftOf(green_house, white_house, house_order) &
|
|
drink(green_house) = Coffee &
|
|
pet(pallmall_smoker) = Bird &
|
|
smoke(yellow_house) = Dunhill &
|
|
drink(house_order(Third)) = Milk &
|
|
house_order(First) = Norwegian &
|
|
Neighbour(blend_smoker, cat_keeper, house_order) &
|
|
Neighbour(dunhill_smoker, neighbour_dunhill_smoker, house_order) &
|
|
drink(bluemaster_smoker) = Beer &
|
|
smoke(German) = Prince &
|
|
house_colour(house_order(Second)) = Blue &
|
|
drink(neighbour_blend_smoker) = Water &
|
|
Neighbour(blend_smoker, neighbour_blend_smoker, house_order)
|
|
|
|
local pred Neighbour(neighbour1::Nationality, neighbour2::Nationality, house_order::HouseOrder)iff
|
|
neighbour1 <> neighbour2 &
|
|
house_order(house1) = neighbour1 & house_order(house2) = neighbour2 &
|
|
( house1 = house2 + 1 | house1 = house2 - 1 )
|
|
|
|
local pred LeftOf(neighbour1::Nationality, neighbour2::Nationality, house_::HouseOrder) iff
|
|
neighbour1 <> neighbour2 &
|
|
house_order(house1) = neighbour1 & house_order(house2) = neighbour2 &
|
|
house1 = house2 - 1
|