CS 486 Applied Logic Assignment #12
Spring 1997 Exercise-not to be turned in

Define a complete binary tree over inductively as
Tree = (Tree Tree).
Describe this as a fixed point over sets.

Using recursion on complete binary trees define a function summing all the numbers in the tree.

In Caldwell's library for the propositional calculus there is a definition of formula rank. Explain it in Smullyan's terms.

An iteration is defined by

Give reduction rules for computing this function and carry them out for a simple example.
Explain why a while loop, is like an iteration.

Give the meaning of a while loop by reduction rules.

Define as a type by specifying the canonical values and primitive recursion on lists.

• About this document ...