—GR
753 On a theorem by Lambek and Moser
Nuenen, 9 October 1980. 3 pages.
States a theorem of Leo Moser and Joachim Lambek (1954), about mapping an increasing sequence of integers to its functional "inverse", and a resulting partition of integers into two sets. A proof of the theorem by a picture, from a book of R. Honsberger, is given.
The subject is taken up in EWD758 "An intriguing example", EWD759 "A somewhat open letter to D.A. Turner", and EWD770 "D.A. Turner's reply", about a program for the function inversion task in the functional (or "applicative"= programming language SASL, and in EWD776 "Lambek and Moser revisited", with a different proof by Dijkstra, by transforming an imperative ("iterative") program.
—GR
776 Lambek and Moser revisited
Nuenen, 8 February 1981. 7 pages. transcription
Proves a theorem of Leo Moser and Joachim Lambek (1954) about mapping an increasing sequence of integers to its functional "inverse", and a resulting partition of integers into two sets. The theorem is proved by deriving a program for the computation of one sequence from the other, and then transforming the program.
This is related to EWD753, where the theorem has been stated, and a different proof has been reported.
The subject has also appeared in EWD758 "An intriguing example", EWD759 "A somewhat open letter to D.A. Turner", and EWD770 "D. A. Turner's reply", about a version of the program in SASL (a "functional" or "applicative" programming language).
—GR