175 lines
6.7 KiB
Text
175 lines
6.7 KiB
Text
// First, let's give some 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
|
|
HouseOrder = 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'.
|
|
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.
|
|
|
|
So, in FormulaOne we use a formula like: 'pet(Swede) = Dog', which simply means that the 'Swede' (type 'Nationality')
|
|
has a 'pet' (type 'Pet', which is 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
|
|
Order = HouseOrder->>Nationality
|
|
|
|
pred Zebra(houseColour::HouseColour, pet::Pet, smoke::Smoke, drink::Drink, order::Order) iff
|
|
|
|
// For convenience sake, some temporary place_holder variables are used.
|
|
// An underscore distinguishes them:
|
|
|
|
houseColour(green_house) = Green &
|
|
houseColour(white_house) = White &
|
|
houseColour(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: }
|
|
houseColour(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' determines the order: }
|
|
LeftOf(green_house, white_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 they drink milk: }
|
|
drink(order(Third)) = Milk &
|
|
|
|
{10. The Norwegian lives in the first 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, order) &
|
|
|
|
{12. In a house next to the house where they have a horse, they smoke Dunhill: }
|
|
Neighbour(dunhill_smoker, neighbour_dunhill_smoker, 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: }
|
|
{10. The Norwegian lives in the first house,
|
|
so the blue house is the second house }
|
|
houseColour(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, 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, order::Order)iff
|
|
neighbour1 <> neighbour2 &
|
|
order(house1) = neighbour1 &
|
|
order(house2) = neighbour2 &
|
|
( house1 = house2 + 1 |
|
|
house1 = house2 - 1 )
|
|
|
|
local pred LeftOf(neighbour1::Nationality, neighbour2::Nationality, order::Order) iff
|
|
neighbour1 <> neighbour2 &
|
|
order(house1) = neighbour1 &
|
|
order(house2) = neighbour2 &
|
|
house1 = house2 - 1
|
|
|
|
{
|
|
The 'all'-query in FormulaOne:
|
|
all Zebra(houseColour, pet, smokes, drinks, order)
|
|
gives, of course, only one solution, so it can be replaced by:
|
|
one Zebra(houseColour, pet, smokes, drinks, 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
|
|
HouseOrder = First | Second | Third | Fourth | Fifth
|
|
|
|
Pet = Nationality->>Domestic
|
|
Drink = Nationality->>Beverage
|
|
HouseColour = Nationality->>Colour
|
|
Smoke = Nationality->>Cigarette
|
|
Order = HouseOrder->>Nationality
|
|
|
|
pred Zebra(houseColour::HouseColour, pet::Pet, smoke::Smoke, drink::Drink, order::Order) iff
|
|
|
|
houseColour(green_house) = Green &
|
|
houseColour(white_house) = White &
|
|
houseColour(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 &
|
|
|
|
houseColour(Englishman) = Red &
|
|
pet(Swede) = Dog &
|
|
drink(Dane) = Tea &
|
|
LeftOf(green_house, white_house, order) &
|
|
drink(green_house) = Coffee &
|
|
pet(pallmall_smoker) = Bird &
|
|
smoke(yellow_house) = Dunhill &
|
|
drink(order(Third)) = Milk &
|
|
order(First) = Norwegian &
|
|
Neighbour(blend_smoker, cat_keeper, order) &
|
|
Neighbour(dunhill_smoker, neighbour_dunhill_smoker, order) &
|
|
drink(bluemaster_smoker) = Beer &
|
|
smoke(German) = Prince &
|
|
houseColour(order(Second)) = Blue &
|
|
drink(neighbour_blend_smoker) = Water &
|
|
Neighbour(blend_smoker, neighbour_blend_smoker, order)
|
|
|
|
local pred Neighbour(neighbour1::Nationality, neighbour2::Nationality, order::Order)iff
|
|
neighbour1 <> neighbour2 &
|
|
order(house1) = neighbour1 & order(house2) = neighbour2 &
|
|
( house1 = house2 + 1 | house1 = house2 - 1 )
|
|
|
|
local pred LeftOf(neighbour1::Nationality, neighbour2::Nationality, order::Order) iff
|
|
neighbour1 <> neighbour2 &
|
|
order(house1) = neighbour1 & order(house2) = neighbour2 &
|
|
house1 = house2 - 1
|