An unusual application of program-proving
Mitchell Wand · 1973
An inductive proof in mathematics may often be expressed as an algorithm and a proof that the algorithm is correct. Especially when the proof proceeds by cases, a recursive pattern-matching language, such as Hewitt's MATCHLESS, is a felicitous language for writing the algorithm. We use this idea to prove a new mathematical result, which itself is of interest in computer science. We define objects called k-models. Our main theorem is a necessary and sufficient condition for a k-model to be the restriction of a k+1-model.