equational versions of fixed-point induction

To: types@theory.lcs.mit.edu
Subject: equational versions of fixed-point induction
From: John C. Mitchell <jcm@cs.stanford.edu>
Date: Thu, 14 Feb 91 08:53:41 EST
Sender: meyer@theory.lcs.mit.edu

Date: Wed, 13 Feb 91 16:04:08 -0800

This is a question that came up in the context of a class I am teaching.
I wanted to find a simple, equational version of induction that
would let me prove some nontrivial equations between typed lambda 
expressions involving a fixed-point operator FIX. The best I can
think of at the moment is the following rule, which relies on
reduction instead of an equational hypothesis.

          F  -->>  M F
       ------------------
          F  =   FIX M

This seems sound in any model equating terms with identical Bohm trees.
It becomes unsound if the hypothesis of the rule is replaced by the 
equation F = M F. A conterexample is just to take M to be the identity.
Otherwise, the rule is similar to McCarthy's recursion induction rule. 

My question is whether anyone else has something similar but better.

As an example of the kind of proof you can do with this, here is
a proof that the term G ::=  (FIX \f.\g. g(fg)) is equal to FIX.
Let F be the term Gx. Then we have F ->> x(Gx). So by the above rule,
F = FIX x. Hence \x.Gx = \x.FIX x, which gives the desired conclusion
by eta-equivalence. I assume that other reasonable proofs can be carried 
out using this rule. If not, I would be interested in counterexamples.

John Mitchell