Steven Pemberton
In [1], several methods are propounded for the hard problem of catching a lion in the Sahara Desert.
However, due to an unfortunate case of bad timing, several important methods were overlooked. We include here, for historical completeness, one of them.
The way the problem reached me was: catch a wild lion in the Sahara Desert. Another way of stating the problem is:
Axiom 0: Sahara ∈ deserts
Axiom 1: Lion ∈ Sahara
Axiom 2: ¬(Lion ∈ cage)
We observe the following invariant:
P1: C(L) ∨ ¬(C(L))
where C(L) means: the value of "L" is in the cage.
Establishing C initially is trivially accomplished with the statement
;cage := {}
Note 0.
This is easily implemented by opening the door to the cage and
shaking out any lions that happen to be there initially.
(End of note 0.)
The obvious program structure is then:
;cage:={} ;do NOT (C(L)) -> ;"approach lion under invariance of P1" ;if P(L) -> ;"insert lion in cage" [] not P(L) -> ;skip ;fi ;od
where P(L) means: the value of L is within arm's reach.
Note 1.
Axiom 1 ensures that the loop terminates.
(End of note 1.)
Exercise 0.
Refine the step "Approach lion under invariance of P1".
(End of exercise 0.)
Note 2.
The program is robust in the sense that it will lead to abortion if
the value of L is "tiger".
Remark 0.
This may be a new sense of the word "robust" for you.
(End of remark 0.)
(End of note 2.)
Note 3.
From observation we can see that the above program leads to the
desired goal. It goes without saying that we therefore do not have to
run it.
(End of note 3.)
References.
(End of references.)
(End of Method.)
[1] H. Petard, A Contribution to the Mathematical Theory of Big Game Hunting, Princeton, N. J., in American Mathematical Monthly, August, 1938