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