Zebra puzzle: Difference between revisions

Line 2,598:

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 if the 'Zebra'-predicate.~~

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 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')~~

So, in FormulaOne we use a formula like: 'pet(Swede) = Dog', which simply means that the 'Swede'

has a 'pet' (type 'Pet', of type 'Domestic', indexed by 'Nationality'), ~~which appears to be a 'Dog' (type 'Domestic').~~

(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...).

}

Line 2,613:

Line 2,616:

HouseOrder = HouseRow->>Nationality

pred Zebra(~~houseColour~~::HouseColour, pet::Pet, smoke::Smoke, drink::Drink, house_order::HouseOrder) iff

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:

~~houseColour~~(green_house) = Green &

house_colour(green_house) = Green &

~~houseColour~~(white_house) = White &

house_colour(white_house) = White &

~~houseColour~~(yellow_house) = Yellow &

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: }

~~houseColour~~(Englishman) = Red &

house_colour(Englishman) = Red &

{ 3. The Swede has a dog: }

Line 2,642:

Line 2,645:

}

{ 5. The green house is immediately to the left of the white house~~: }~~

{ 5. The green house is immediately to the left of the white house.

{ The local predicate 'LeftOf' (see below) determines the house order: }

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: }

Line 2,661:

Line 2,664:

house_order(First) = Norwegian &

{11. The man who smokes Blend lives in the house next to the house with cats~~: }~~

{11. The man who smokes Blend lives in the house next to the house with cats.

{ Another local predicate 'Neighbour' makes them neighbours:}

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: }

Line 2,676:

Line 2,679:

{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: }

~~houseColour~~(house_order(Second)) = Blue &

house_colour(house_order(Second)) = Blue &

{16. They drink water in a house next to the house where they smoke Blend: }

Line 2,703:

Line 2,706:

{

The 'all'-query in FormulaOne:

all Zebra(~~houseColour~~, pet, smokes, drinks, house_order)

all Zebra(house_colour, pet, smokes, drinks, house_order)

gives, of course, only one solution, so it can be replaced by:

one Zebra(~~houseColour~~, pet, smokes, drinks, house_order)

one Zebra(house_colour, pet, smokes, drinks, house_order)

}

Line 2,723:

Line 2,726:

HouseOrder = HouseRow->>Nationality

pred Zebra(~~houseColour~~::HouseColour, pet::Pet, smoke::Smoke, drink::Drink, house_order::HouseOrder) iff

pred Zebra(house_colour::HouseColour, pet::Pet, smoke::Smoke, drink::Drink, house_order::HouseOrder) iff

~~houseColour~~(green_house) = Green &

house-colour(green_house) = Green &

~~houseColour~~(white_house) = White &

house-colour(white_house) = White &

~~houseColour~~(yellow_house) = Yellow &

house-colour(yellow_house) = Yellow &

smoke(pallmall_smoker) = PallMall &

smoke(blend_smoker) = Blend &

Line 2,734:

Line 2,737:

pet(cat_keeper) = Cat &

pet(neighbour_dunhill_smoker) = Horse &

~~houseColour~~(Englishman) = Red &

house_colour(Englishman) = Red &

pet(Swede) = Dog &

drink(Dane) = Tea &

Line 2,747:

Line 2,750:

drink(bluemaster_smoker) = Beer &

smoke(German) = Prince &

~~houseColour~~(house_order(Second)) = Blue &

house_colour(house_order(Second)) = Blue &

drink(neighbour_blend_smoker) = Water &

Neighbour(blend_smoker, neighbour_blend_smoker, house_order)

Line 2,763:

Line 2,766:

<pre>

~~houseColour~~=[ {Englishman} Red, {Swede} White, {Dane} Blue, {Norwegian} Yellow, {German} Green ]

house_colour = [ {Englishman} Red, {Swede} White, {Dane} Blue, {Norwegian} Yellow, {German} Green ]

pet =[ {Englishman} Birds, {Swede} Dog, {Dane} Horse, {Norwegian} Cats, {German} Zebra ]

pet = [ {Englishman} Birds, {Swede} Dog, {Dane} Horse, {Norwegian} Cats, {German} Zebra ]

smokes =[ {Englishman} PallMall, {Swede} BlueMaster, {Dane} Blend, {Norwegian} Dunhill, {German} Prince ]

smokes = [ {Englishman} PallMall, {Swede} BlueMaster, {Dane} Blend, {Norwegian} Dunhill, {German} Prince ]

drinks =[ {Englishman} Milk, {Swede} Beer, {Dane} Tea, {Norwegian} Water, {German} Coffee ]

drinks = [ {Englishman} Milk, {Swede} Beer, {Dane} Tea, {Norwegian} Water, {German} Coffee ]

house_order=[ {First} Norwegian, {Second} Dane, {Third} Englishman, {Fourth} German, {Fifth}, Swede ]

house_order = [ {First} Norwegian, {Second} Dane, {Third} Englishman, {Fourth} German, {Fifth}, Swede ]

</pre>