Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in: ~eker/public_html/Maude/Alpha86c/ or downloaded from: http://www.csl.sri.com/~eker/Maude/Alpha86c/ Alpha release site authentication: User Name: maudeabuser Password: bughunter This version is a Maude 2.2 release candidate and reports itself as such. So far I have only made binaries for Linux on i86 and Darwin. What other (unix) platforms do Maude Abusers want to see supported in this release? I would like to drop less popular platforms to ease the maintenance burden; also is there any interest in Linus on AMD64? Bug fixes ========== (1) A bug in the recovery from surface level syntax errors in renamings that led to internal errors; for example: fmod SYNTAX-BUG is pr INT * (op _*_ to) . op a : -> Int . endfm (2) A bug where an attempt to rename a polymorphic operator from a parameter theory is ignored without generating an advisory; for example: fth POLY is sort Elt . op f : Universal -> Elt [poly (1)] . endfth fmod P{X :: POLY} is op a : -> X$Elt . endfm fmod TEST{X :: POLY} is inc (P * (op f to g)){X} . endfm show all . (3) A bug where the backquoted form of structured sort names is used in op renamings within created module names; for example: fmod FOO{X :: TRIV, Y :: TRIV} is sort Foo{X,Y} . op f : Foo{X,Y} -> Foo{X,Y} . endfm fmod BAR{Z :: TRIV} is inc FOO{Nat, Nat} * (op f : Foo{Nat,Nat} -> Foo{Nat,Nat} to g) . endfm show modules . (4) The sorts in op head : NeList{X} -> X$Elt . op last : NeList{X} -> X$Elt . op occurs : X$Elt List{X} -> Bool . from fmod LIST* are incorrect. The declarations for these operators are now fixed, however since they are defined symbols and rewriting is allowed at the kind level, the effect of the bug is invisible for normal rewriting. (5) A bug where mapping an AC(U) symbol to a term in a view could cause an internal error during instantiation; exposed by: fth T is sort Elt . op f : Elt Elt -> Elt [assoc comm] . endfth fmod M{X :: T} is op g : X$Elt X$Elt -> X$Elt . vars A B : X$Elt . eq g(A, B) = f(A, B, A, B) . endfm show all . view V from T to NAT is sort Elt to Nat . op f(X:Elt, Y:Elt) to term X:Nat + Y:Nat . endv fmod TEST is inc M{V} . endfm show all . Other Changes ============== (1) There is now some recovery from surface level syntax errors in views at the statement level, by ignoring stuff up to the next period followed a by a suitable keyword. view String2 from TRIV to STRING is meaningless junk . sort Elt to String . endv (2) There is more overparsing, and a full recovery can made in the following situations: (a) missing "is" keyword (modules, theories and views). (b) missing period after an importation (modules and theories). (c) missing period after an operator declaration (modules and theories). (d) missing period after a variable alias declaration (modules, theories and views). (e) missing period after a sort mapping (views). Note that the line number reported for missing tokens is the one at a token other than the one expected was seen; and this is typically one or more lines later than the user would have typed the token; for example: fmod FOO is sort Foo . ops a b : -> Foo eq a = b . endfm Maude indicates that a period is missing on the 5th line, whereas, while the missing period could legally appear at the beginning of this line, most users would type it at the end of the 3rd line. (3) Duplicate/conflicting attributes at object level now generate appropriate warnings: fmod FOO is sort Foo . ops a b c d e : -> Foo . op f : Foo Foo -> Foo [left id: a right id: b] . op g : Foo Foo -> Foo [assoc assoc] . op _+_ : Foo Foo -> Foo [prec 4 prec 5] . endfm (4) Renaming of modules with bound parameters is now supported. This turns out to be necessary if we allow renaming of modules with free parameters because of cases such as: fth T is endfth view Bool from T to BOOL is endv fmod FOO{X :: T} is sort Foo{X} . endfm fmod BAR{Y :: T} is inc FOO{Y} . endfm fmod BAZ is inc (BAR * (sort Foo{Y} to Bar{Y})){Bool} . endfm show all . Here BAR has only a free parameter and so it can be renamed; however it's renaming imports the renaming of FOO{[Y]} which has a bound parameter. Allowing renaming of modules with bound parameters requires that renamings be capable of instantiation; that is parameterized sort names inside a renaming have their parameters instantiated, with an extra {} pair being added in the case of instantiation by theory-views. Currently this is done in a somewhat naive manner and it is possible to trick the implementation by using structured sort names that contain things other than parameters. When, due to instantiation by a theory-view, a bound parameter in a renamed module escapes and needs to be rebound by an extra instantiation, the extra instantiation is inserted _before_ rather than after the renaming. For example: fmod FOO{X :: TRIV} is sort Foo{X} . op f : Foo{X} -> Foo{X} . endfm fmod BAR{X :: TRIV} is inc FOO{X} . sort Bar{X} . op g : Bar{X} -> Foo{X} . endfm fmod BAZ is inc (BAR * (sort Foo{X} to Foo'{X}, sort Bar{X} to Bar'{X}, op f : Foo{X} -> Foo{X} to f', op g : Bar{X} -> Foo{X} to g') ){TAO-SET}{Nat<} . endfm show modules . It seems that recapturing the parameter after the renaming would also work but it is done before the renaming for consistancy with Full Maude. (5) Passing parameters from an enclosing module (PEMs) in nonfinal instantiations is now prohibited. This restriction also appears in Full Maude and avoids many subtle issues, some of which don't seem to have a consistent resolution now that renaming of modules with bound parameters is supported. Thus: fmod TEST{X :: TRIV, Y :: TAO-SET} is inc MAP{X, TAO-SET}{Y} . endfm is now illegal because X occurs in nonfinal instantiation MAP{X, TAO-SET}. This example must now be rewritten as view TRIV from TRIV to TRIV is endv fmod TEST{X :: TRIV, Y :: TAO-SET} is inc MAP{TRIV, TAO-SET}{X, Y} . endfm Note that view TRIV is now defined in the prelude. Another way of viewing the restriction is that parameters from an enclosing module and theory views may not occur in the same instantiation. Note that theory-views may never occur in a final instantiation (otherwise there would be free parameters in an import) and must occur in any nonfinal instantiation (otherwise there would be no free parameters for the next instantiation). One nice feature of this restriction is that it is now impossible to have a module with both free and bound parameters and in particular it is not possible to have a module with free and bound parameters having the same name. Thus the automatic renaming of a free parameter from say X to $X to avoid a name clash no longer happens. (6) Code now compiles under gcc 4.0.1; Doug Lea's malloc.c upgraded to version 2.7.3; test suite expanded. New features ============= (1) There is a new command line option, -no-wrap, to disable the automatic line wrapping of output. (2) There is a new parameterized fmod, LIST-AND-SET{X :: TRIV} in the prelude. This includes LIST{X} and SET{X} and provides 4 ops: op makeSet : List{X} -> Set{X} . computes a set of the elements occuring in an n size list in O(n log n) time. op makeList : Set{X} -> List{X} . computes a list (system defined order) of the elements occuring in an n size set in O(n log n) time. op filter : List{X} Set{X} -> List{X} . filters an n size list by discarding those elements that do not occur in an m size list in O(n log m) time. op filterOut : List{X} Set{X} -> List{X} . filters an n size list by discarding those elements that do occur in an m size list in O(n log m) time. This feature was requested by Carolyn. (3) The is a new fth, DEFAULT which is like TRIV but require that there be a distiguished "default" element: op 0 : -> Elt . There are views Nat0, Int0, Rat0, Float0, String0, Qid0, that map from DEFAULT to the various builtin data type modules in the obvious way. The point of DEFAULT is so that the new parameterized fmod ARRAY can be defined. This works like MAP except that mappings to 0 are never inserted and an attempt to look up an unmapped value always returns 0; i.e. sparse array semantics. Note that mappings to 0 that are created by constructors rather than the insert operator are not removed as doing this check each time a new Array is formed would be very costly. (4) There is now a builtin linear Diophantine equation solver. The interface to the solver is defined in the file linear.maude which contains the fmod DIOPHANTINE. The current solver finds non-negative solutions a system S of n simultaneous equations in m variables having the form: M v = c where M is an n * m integer coefficient matrix, v is a column vector of m variables and c is a column vector of n integer constants. Both matrices and vectors are represented as sparse arrays with their dimensions implicit and their indices starting from 0. For example the matrices 1 2 0 -1 1 2 0 0 -1 0 0 0 0 are both described by the following syntax (0,0) |-> 1 ; (1,1) |-> 2 ; (1,1) |-> -1 No distinction is made between row and column vectors so both (-2 0 0 3) and (-2 0 0 3)^T are described by the following syntax: 0 |-> -2 ; 3 |-> 3 The special constants zeroMatrix and zeroVector denote the all zero matrix and vector respectively. The solver is invoked with the builtin operator: natSystemSolve : IntMatrix IntVector String -> IntVectorSetPair [special (...)] . which takes the coefficient matrix, constant vector and a string naming the algorithm to be used, and returns the complete set of solutions encoded a pair of sets of vectors [A | B]. The non-negative solutions of the linear Diophantine system correspond exactly to those vectors that can be formed as the sum of a vector from A and a non-negative linear combination of vectors from B. In particular, if the the system S is homogeneous (c == zeroVector) then A contains just the zeroVector and B is the Diophantive basis of S (which will be empty if S only admits the trivial solution). A homogeneous system either has just the trivial solution or infinitely many solutions. If S is inhomegeneous (c =/= zeroVector) then if S has no solution, both A and B will be empty. Otherwise B will consists of the Diophantine basis of S', the system formed by setting c == zeroVector, while A contains all solutions of S that are not strictly larger than any element of B. An inhomegeneous system may have no solution (A and B both empty), a finite number of solutions (A nonempty, B empty) or infinitly many solutions (A and B both nonempty). In either case, the solution encoding [A | B] is unique. Deciding whether a linear Diophantine system admits a non-negative, nontrivial solution is NP-complete (stated as known in [1]). Furthermore the size of the Diophantive basis of a homogeneous system can be very large. For example the equation: x + y - k z = 0 for constant k > 0, has a Diophantive basis (i.e. set of minimal, nontrivial solutions) of size k + 1. The are currently two algorithms implemented. "cd" specifies a version of the classical Contejean-Devie algorithm[2] with various improvements. The algorithm is based on incrementing a vector of counters, one for each variable, and so it can only solve systems where the answers involve fairly small numbers. It is fairly insensitive to the number of degrees of freedom in the problem. The improvements in this implementation kick in when an equation has zero or one unfrozen variables with nonzero coefficients and result in either forced assignments or early pruning of a branch of the search. It performs well on this 13 minimal solution homogeneous system from [4]: red natSystemSolve( (0,0) |-> 1 ; (0,1) |-> 2 ; (0,2) |-> -1 ; (0,3) |-> 0 ; (0,4) |-> -2 ; (0,5) |-> -1 ; (1,0) |-> 0 ; (1,1) |-> -1 ; (1,2) |-> -2 ; (1,3) |-> 2 ; (1,4) |-> 0 ; (1,5) |-> 1 ; (2,0) |-> 2 ; (2,1) |-> 0 ; (2,2) |-> 1 ; (2,3) |-> -1 ; (2,4) |-> -2 ; (2,5) |-> 0, zeroVector, "cd") . "gcd" specifies an original algorithm based on integer Gaussian elimination following by a sequence of extended gcd computations. It can "home in" quickly on solutions involving large numbers but it is very sensitive to the number of degrees of freedom and can easily degenerate into a brute force search. Furthermore, termination depends on the bound on the sum of minimal solution established in [3] which can cause an huge amount of fruitless search after the last minimal solution has been found. It performs well on the "sailors and monkey" problem from [2]: red natSystemSolve( (0,0) |-> 1 ; (0,1) |-> -5 ; (1,1) |-> 4 ; (1,2) |-> -5 ; (2,2) |-> 4 ; (2,3) |-> -5 ; (3,3) |-> 4 ; (3,4) |-> -5 ; (4,4) |-> 4 ; (4,5) |-> -5 ; (5,5) |-> 4 ; (5,6) |-> -5, 0 |-> 1 ; 1 |-> 1 ; 2 |-> 1 ; 3 |-> 1 ; 4 |-> 1 ; 5 |-> 1, "gcd") . Finally "" can be passed which allows the system to choose which algorithm to use. For convenience, the operator op natSystemSolve : IntMatrix IntVector -> IntVectorSetPair . is equationally defined to invoke the builtin operator with "" References =========== [1] Ana Paula Tomas. On solving linear diophantine constraints. PhD thesis, Universidade do Porto, 1997. [2] Evelyn Contejean and Herve Devie. An efficient incremental algorithm for solving systems of linear diophantine equations. Information and Computation 113, pages 143-172, 1994. [3] L. Pottier. Minimal solutions of linear diophantine systems: bound and algorithms. Proceedings of RTA '91, LNCS 488, pages 162-173. [4] E. Domenjoud. Solving systems of linear diophantine equations: an algebraic approach. In Proceedings of MFCS'91, LNCS 520, pages 141-150. Steven