[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Bogus << TCC




I have a datatype for simple expressions, and need to define recursive
functions on the expressions.  But when I use << for the measure, I get
the following TCC:


fv_TCC1: OBLIGATION
      well_founded?(LAMBDA (x: exp_adt[identifier, nat].exp,
                            y: exp_adt[identifier, nat].exp):
                      x << y);

The prover can't finish the proof of the TCC, and neither can I.  What
am I doing wrong?

Here is my datatype and the theory that uses it:

exp [ id, num: TYPE ]: DATATYPE

  BEGIN

   num_exp(n: num): num?
   id_exp(name: id): id?
   add_exp(e1, e2: exp): add_exp?
   let_exp(name: id, e1, e2: exp): let_exp?

  END exp


freevars: THEORY
 BEGIN
  
  IMPORTING exp
  
  identifier: TYPE
  
  e: VAR exp[identifier, nat]
  
  i: VAR identifier

  fv(e):
      RECURSIVE SETOF[identifier] = CASES e OF
          num_exp(n): emptyset,
          id_exp(id): singleton(id),
          add_exp(e1, e2):
              union(fv(e1), fv(e2)),
          let_exp(id, e1, e2):
              union(fv(e1),
                    difference(fv(e2),
                               singleton(id)))
          ENDCASES
       MEASURE e BY <<

  END freevars

---------------------------
Galen Williamson
Semantics Group
College of Computer Science
Northeastern University
gwilliam@ccs.neu.edu