OBJ3 Bug List

This document includes a summary of all known bug-list in this version of OBJ3. To report a new bug, please send an email to kiniry@acm.org

OBJ3 2.10 [Fedora Core 3/x86 and Mac OS X 10.3.6 on PPC] (GCL+CMU+SBCL+CLISP)

No known bugs.

OBJ3 2.09 [RedHat 8/glibc-2.3.2-4.80.6] (GCL+CMU)

No known bugs.

OBJ3 2.08 (TRIM)

While not a bug per se, it is important to note that the TRIM compiler has several limitations. In general, it cannot be used on arbitrary OBJ3 code because it does not support the following OBJ3 features: built-ins, A/C rewriting, evaluation strategies, and non-left-linear equations. Even so, the speed increase afforded by TRIM is quite welcome for evaluations of high computational complexity. See the TRIM paper included with the distribution for more information.

OBJ3 2.04

in(put) cannot accept filenames with a '_' in them.
noted: ?, fixed: 1993-04-07 by A. Stevens

No details available.

Module processing crash.
noted: 20/4/93, fixed: ?

Description: If an attempt is made to instantiate a parameterized module with complete garbage, especially if insufficient parameters are given, the system drops out with a LISP exception. Missing error check someplace?

No fix currently available.

Parser Limitations not commented on.
noted: 1993-04-20, fixed: ?

The parser is unable to handle operator syntax involving brackets. For example,

      op (.All _ ) _ : ...
      

However, operator declarations of this form are silently accepted.

No fix currently available.

Problems with comm assoc matcher.
noted: 1993/03/18, fixed: ?

Summary. For example,

      obj MATCH is
      sorts S1 S2 .
      subsort S2 < s1 .
      op _+_ : S1 S1 -> S1 [assoc] .
      op _+_ : S2 S2 -> S2 [assoc comm] .
      op a   : -> S2 .
      op b   : -> S2 .
      op c   : -> S1 .
      op _*_ : S1 S1 -> S1 .

      var x : S1 .
      eq x * x = x .
      endo

      red (a + b)*(b + a).  ***> should be: a + b

      red ((a + b) + c)*((b + a)+ c).  ***> should be: a + b + c
      
Problem with comm assoc id matcher.
noted: 1993/04/28, fixed: ?

If you open . a module instantiated with a module introducing an operator needing matching acz matching, attempting to use the operator causes a segmentation fault. Running within the interpreter gives a more informative response.

From original obj3/lisp/basic/counter.txt (unconfirmed claim):
      Joseph,

      I think I may have found a bit of a bug in the current
      lecture notes.  In section 5.5 you claim that if a Sigma
      term-rewriting system A with no void sorts is confluent
      then so is A with fresh constant (i.e. A treated as a
      Sigma U X term-rewriting system).

      Here's what seems to be a counter-example to this claim.
      Consider

      obj A is
      sort Nat .
      vars X Y Z : Nat .

      op 0 : -> Nat
      op s : Nat -> Nat .
      op _+_ : Nat Nat -> Nat .
      op t : Nat Nat Nat -> Nat .

      eq 0 + X = X .
      eq s(X) + Y = s(X + Y) .
      eq X+(Y+Z) = t(X,Y,Z) .
      eq t(s(X),Y,Z) = s(X + (Y+Z)) .
      eq t(0,Y,Z) = Y + Z .
      endo

      Termination is pretty trivial: e.g.

      p(0) = 2
      p(s(a)) = 1 + p(a)
      p(a+b) = 4 + p(a)p(b)
      p(t(a,b,c)) = 2 + p(a)(4 + p(b)p(c))

      We now prove A is confluent.  Let a,b,c,d,e etc denote
      A-terms

      There are two critical pairs:

      a + (b + (c + d)) 1=> a + t(b,c,d)	(i)
      1=> t(a,b, c + d)

      and
      a + (s(b) + c)   1=> t(a,s(b),c)       (ii)
      1=> a+s(b+c) 		   

      Now, it is easy to see that for any term t we either have

      t *=> s(t') or  a *=> 0

      (Simply rewrite using an most-nested-first ``layered''
      rewriting strategy.  I.e. alternately rewrite most-nested
      +'s, then most-nested t's)
      

      Thus we can easiy show that a + t(b,c,d) and t(a,b, c +
      d) are both rewriteable to one of

      s(a' + s(b' + (c + d))) or s(b' + (c + d)) or s(a' + (c +
      d)) or (c + d)

      depending on which of the two cases above hold for a and b .

      Similarly, we can easily show t(a,s(b),c) and 1=>
      a+s(b+c) are both rewriteable to one of

      s(a',s(b+c)) or s(b + c) 
      
      depending on which of the two cases above holds for a.
      Hence A is locally confluent and hence confluent.


      Now let X = { a,b,c,d } and consider A as a Sigma^{A} U X
      term-rewriting system.


Adding a,b,c,d as fresh constants we obtain

a + (b + (c + d))) 1=> t(a,b, c + d)
1=> a + t(b,c,d)

with both alternate rewritings normal forms. Hence A
treated as Sigma^{A} U X term-rewriting system is NOT
confluent.

Andrew