Dear Maude Abusers, A new alpha release can be accessed at SRI-CSL in ~eker/public_html/Maude/Alpha73/ or downloaded from http://www.csl.sri.com/~eker/Maude/Alpha73/ Running this new version is complicated by the fact it uses dynamic libraries, (gmp 4.1 and its C++ bindings) that will not be installed on most machines. Thus you may need to install them by one of these methods: (1) Obtain the source code from http://www.swox.com/gmp/ Configure with --enable-cxx for C++ support. Compile it with g++ 2.95.3 (because the C++ ABI changes with every compiler release you need the same g++ as I used to compile Maude). Install the two shared objects produced some place where your dynamic linker can find them. If you cannot write to system library directories and your sysadmins won't install them for you, you can always place them in ~/lib and point the LD_LIBRARY_PATH environment variable at this directory. (2) If this fails, you can get the shared objects I use from http://www.csl.sri.com/~eker/Maude/Lib/Linux/ or http://www.csl.sri.com/~eker/Maude/Lib/Solaris/ as appropriate and put them in ~/lib Then make the symbolic links and set LD_LIBRARY_PATH ln -s ~/lib/libgmp.so.3.3.0 ~/lib/libgmp.so.3 ln -s ~/lib/libgmpxx.so.3.0.2 ~/lib/libgmpxx.so.3 setenv LD_LIBRARY_PATH ~/lib Note also the the linux version is now dynamically linked whereas previous versions were statically linked and in particular you will need the libstdc++.so.3 that comes with g++ 2.95.3. If you run into linking problems you can use the ldd command to see what shared objects are needed. BTW I will be offline from Sat June 22 thru Sun July 7 so if you are going to try this new version I suggest install it before noon PST friday in case you need email support. Bug fixes: 1 A bug in sortLeq which caused unpredictable behavior when the two sorts were in different kinds - reported by Carolyn. 2 A bug which caused a incomplete module terminated by ctrl-D to not be discarded, causing unpredictable behavior - reported by Carolyn. 3 A bug where memoized rewrites were not counted - reported by Carolyn. Minor changes: 1 show all . and show ops . now display format attributes; further more generated gather info is only displayed if the op has arguments. 2 show all . now puts multiple subsorts in a single subsort declaration where possible. There are a number of major changes in this version, the last two of which will break most existing Maude code, however the existing model-checker.maude can be used unmodified. The iter theory =============== Unary operators may be declared to belong to the iter (short for iterated function symbol) theory. op f : Foo -> Foo [iter] . The sole purpose of this theory is to permit the efficient i/o and manipulation of very large stacks of functions symbols. The term f(f(f(X:Foo))) can be input as f^3(X:Foo) and will be output in that form. A term such as f^1234567890123456789(X:Foo) is too large to be input, output or manipulated is regular notation but can be input and output in this compact notation and certain (built in) manipulations may be efficient. The precise form the of compact iter theory notation is the prefix name of the operator followed by: ^[1-9][0-9]* (in lex regular expression notation) without no intervening white space. Note that f^0123(X:Foo) is not acceptable. Of course regular notation (and mixfix notation if appropriate) can still be used. Sort computations using subsort polymorphism are efficient: subsorts Odd Even < Foo . op f : Odd -> Even [ditto] . op f : Even -> Odd [ditto] . red f^1234567890123456789(X:Odd) . Membership axioms headed by iter operators are neither efficient nor correct (the same is true of assoc operators since we started allowing declarations at the kind level). Correctness may eventually be fixable, efficiency will not be. The situation with matching and rewriting is analogeous to the assoc theory - proper subterms of s^3(X:Foo), such as s^2(X:Foo) and s(X:Foo) can be matched and rewritten by means of extension. However for the pupose of calculating term depth, if the top level is 0, X:Foo is at level 1, not level 3. Fair rewriting treats a whole stack of iter operartors as a single position for the purposes of position fairness (again this is analogeous to the assoc case). The iter attribute is reflected by op iter : -> Attr [ctor] . A term such as f^1234567890123456789(X:Odd) is metarepresented as 'f^1234567890123456789['X:odd] metaParse() understands the compact iter theory notation and metaPrettyPrint() uses it. A version of the notation is also supported by the -xml-log command line flag, using the number attribute: The built in NATs ================= This is the primary application of the iter theory - an algebraic specification of the natural numbers that supports efficient builtin representation and operations. The natural numbers are constructed as follows: sorts Zero NzNat Nat . subsort Zero NzNat < Nat . op 0 : -> Zero [ctor] . op s_ : Nat -> NzNat [ctor iter special (...)] . Natural numbers can be input, and by default will be output in normal decimal notation; however 42 is just an alternative concrete syntax for s_^42(0). The command set print number on/off . controls whether decimal notation is used by the pretty printer. Note that redundant notation such as 00042 is not acceptable. metaParse() and metaPrettyPrint() support decimal notation however there is no other reflection of it - the metarepresentation of 42 is 's_^42['0.Zero] not '42.NzNat Nor is there XML support for it. Most of the usual arithmetic and bitwise operators are provided. They are not defined algebraically but could be given an algebraic definition by the user if desired. The operation semantics for most of the builtin operators is that you only get builtin behaviour when all the arguments are actually natural numbers. The exception is AC builtin operators which will compute as much as possible on natural number arguments and leave other arguments unchanged; so for example: red in NAT : gcd(gcd(12, X:Nat), 15) . results in: result Nat: gcd(X:Nat, 3) If the builtin operator does not disappear due to builtin semantics then user equations are tried. You can define functions on the Nats by matching into the sucessor notation; for example: fmod FACT is inc NAT . op _! : Nat -> NzNat . var N : Nat . eq 0 ! = 1 . eq (s N) ! = (s N) * N ! . endfm red 100 ! . red 1000 ! . It is even possible to get a specification of Z_{3} by fmod MOD3 is inc NAT . eq 3 = 0 . endfm However. apart from it's poor efficiency, this "writes up" from NzNat to Nat. Note that to avoid producing negative numbers, negation, subtraction and bitwise not are not provided. There is however symmetric difference: op sd : Nat Nat -> Nat [comm special (...)] . There is a limit on exponentiation in that builtin behavior will not occur if the first agumnent is > 1 and the second argument is too large. Similarly left shift does not work if the first argument is >= 1 and the second argument is too large. Currently "too large" means greater than 1000000 but this may change. Warning: it is easy to fill your machine's memory by generating huge natural numbers. Modular exponentiation op modExp : Nat Nat NzNat ~> Nat [special (...)] . has no such limits and may be useful for cryptographic algorithms. The built in INTs ================= The integers are constructed on top of the natural numbers as follows: sorts NzInt Int . subsort NzNat < NzInt Nat < Int . op -_ : NzNat -> NzInt [ctor special (...)] . Integers can be input, and by default are output in normal decimal notation; however -42 is just an alternative concrete syntax for - 42 which itself is just an alternative concrete syntax for - s_^42(0). As with NATs this notation is supported by metaParse() and metaPrettyPrint() but not by the metaterm representation or XML. Many of the operations in NAT extend to the integers, and a few new ones are provided. Bitwise operations on negative integers use the 2's complement representation. The built in RATs ================= The rationals are constructed on top of the integers and natural numbers as follows: sorts NzRat Rat . subsorts NzInt < NzRat Int < Rat . op _/_ : NzInt NzNat -> NzRat [ctor prec 31 gather (E e) special (...)] . Rationals can be input, and by default are output in normal decimal notation; however -5/42 is equivalent to -5 / 42 which is equivalent to - 5 / 42 which really denotes - s_^5(0) / s_^42(0). As with NATs and INTs this notation is supported by metaParse() and metaPrettyPrint() but not by the metaterm representation or XML. The numerator and denominator of a rational may contain common factors but these are removed by a single builtin rewrite whenever the rational is reduced (_/_ is not a free constructor). Some of the operations in INT are extended to rationals and a few new ones are provided. However unlike operations on the NATs and INTs these are defined in Maude by equations and may do some rewriting even when their arguments are not properly constructed rationals. Note that the choice of equations for defining operations on the rationals is motivated by performance - simpler equations are possible in many cases but they turn out to have a big performance penalty. op trunc : Rat -> Int . rounds its argument towards 0. op frac : Rat -> Rat . gives the fraction part of its argument and this always has the same sign as its argument. MachineInts replaced by number hierarchy ======================================== This is the most far reaching change since most of the builtin operations (except the model checker and sat solver) are affected to some extent and have their semantics subtly or not so subtly altered. fmod FLOAT is unaffected except some special hooks are renamed for consistancy. fmod STRING now protects NAT rather than MACHINE-INT. Nats are used in place of MachineInts which means that operations can no longer take nehative arguments. The String <-> MachineInt conversion functions are deleted. fmod FLOAT-CONVERSION is deleted. fmod NUMBER-CONVERSION is added to consolidate all the conversion functions between the 3 major builtin data types (Nats/Ints/Rats, Floats and Strings). op float : Rat -> Float . Computes the nearest Float to a given Rat. If the absolute value of the Rat falls outside the range representable by IEEE-754 double precision finite floating point numbers, Infinity or -Infinity is returned as appropriate. This seems consistant since Infinity & -Infinity are used to handle out-of-range situations in the Float world. op rat : FiniteFloat -> Rat . Converts finite Floats to Rats exactly (since every IEEE-754 finite floating point number is a rational number). Of course if the result happens to be a Nat or an Int that is what you get. rat(Infinity) and rat(-Infinity) do not reduce since they have no reasonable representation in the Rat would. It is intended that float(rat(F:FiniteFloat)) = F:FiniteFloat though I am relying on a 3rd party library (GNU gmp) for the yucky bit twiddling and I have not checked it's correctness. Also note that counterintuitive results are possible when converting from the approximate world of Floats to the exact world of Rats: red rat(1.1) . gives result NzRat: 2476979795053773/2251799813685248 This is because 1.1 cannot be represented exactly as a Float and the nearest Float is 1.100000000000000088817841970012523233890533447265625 which is the above rational. op string : Rat NzNat ~> String Converts a Rat to a String using a given base which must lie in the range 2,...,36. Of course Rats that are really Nats or Ints are converted to string representations of Nats or Ints so red string(-1, 10) . gives result String: "-1" op rat : String NzNat ~> Rat Converts a String to a Rat using a given base which must lie in the range 2,...,36. Of course if the result happens to be a Nat or an Int that is what you get. Currently the function is very strict about what strings are converted: the string must be something that the Maude parse would recognize as a Nat, Int or Rat. This could be changed to a more generous interpretation in the future. op string : Float -> String . op float : String ~> Float . These work as they did in FLOAT-CONVERSION. In particular float(string(F:Float)) == F:Float . op <_,_,_> : Int String Int -> DecFloat [ctor] . op decFloat : Float Nat -> DecFloat . DecFloats provide the means for arbirary formating of Floats as they did in FLOAT-CONVERSION. A DecFloat consists of a sign (1, 0 or -1), a String of digits and a decimal point position (0 is just in front of first digit, -ve is to the left, +ve is to the right). Thus < -1, "123", 11 > represents -1.23e10 . decFloat(F, N) converts F to a decFloat, rounding to N significant digits using the IEEE-754 "round to nearest" rule with trailing zeros if need. If N is 0, an _exact_ DecFloat representation of F is produced - this may require hundreds of digits. For any well formed Nat N: decFloat(Infinity, N) = < 1,"Infinity",0 > and decFloat(-Infinity, N) = < -1,"Infinity",0 > In fmod QID, the only operations that depended on MACHINE-INT were the deprecated backward compatibility operations so these are deleted. In fmod META-TERM some function definitions are rewritten to avoid the need for maxMachineInt. In fmod META-MODULE, Nats replace MachineInts and NatLists replace MachineIntLists: sort NatList . subsort Nat < NatList . op __ : NatList NatList -> NatList [ctor assoc] . op strat : NatList -> Attr [ctor] . op prec : Nat -> Attr [ctor] . In fmod META-LEVEL we need a notion of unbounded that was previously supplied by maxMachineInt. We use: sort Bound . subsort Nat < Bound . op unbounded : -> Bound . Also Nat replaces MachineInt in: op noParse : Nat -> ResultPair? [ctor] . The descent functions with modified semantics are: op metaRewrite : Module Term Bound ~> ResultPair . op metaFrewrite : Module Term Bound Nat ~> ResultPair . Rewrite limit is a Bound; it must be >= 1 and may be unbounded. Gas is now a Nat and must be >= 1. op metaApply : Module Term Qid Substitution Nat ~> ResultTriple? . op metaXapply : Module Term Qid Substitution Nat Bound Nat ~> Result4Tuple? . op metaMatch : Module Term Term Condition Nat ~> Substitution? . op metaXmatch : Module Term Term Condition Nat Bound Nat ~> MatchPair? . op metaSearch : Module Term Term Condition Qid Bound Nat ~> ResultTriple? . Last argument is always the solution number which is now a Nat. For metaXapply() and metaXmatch() the minimum depth is now a Nat. For metaXapply(), metaXmatch() and metaSearch() the maximum depth is now a Bound and can take the value unbounded. Statement Attributes ==================== Statements can now take attributes; currently only two statement attributes are available - more are planned. They are label, which is followed by an identifier and metadata which is followed by string. For example: eq foo = bar [label e1 metadata "lemma 1"] . cmb a : b if c [label m1] . rl quux => baz [metadata "\cite{Bloggs:2001}"] . Note that membership axioms and equations can now take labels rather than just rules. One use for such labels is in conjunction with the tracer/debugger. For example set trace on . set trace select on . trace select e1 . would cause selective tracing of rewrites that have e1 as top symbol _or_ involve a statement labeled e1 such as the equation above. In a similar vein it is possible to break into the debugger when a given labeled statement is about to execute: set break on . break select e1 . There will be other applications for labeled equations in the future. The old style rule labels are now supported as syntactic sugar, even for membership axioms and equations: eq [e1]: foo = bar [metadata "lemma 1"] . cmb [m1]: a : b if c . The metadata attribute is intended to hold data about the statement in whatever syntax the user cares to create/parse. It is like a comment that is carried around with the statement. Usual string escape conventions apply. Statement attributes and the new syntax for labels is reflected by the following changes to the metasignature: op label : Qid -> Attr [ctor] . op metadata : String -> Attr [ctor] . op mb_:_[_]. : Term Sort AttrSet -> MembAx [ctor] . op cmb_:_if_[_]. : Term Sort EqCondition AttrSet -> MembAx [ctor] . op eq_=_[_]. : Term Term AttrSet -> Equation [ctor] . op ceq_=_if_[_]. : Term Term EqCondition AttrSet -> Equation [ctor] . op rl_=>_[_]. : Term Term AttrSet -> Rule [ctor] . op crl_=>_if_[_]. : Term Term Condition AttrSet -> Rule [ctor] . There is no distinction at the sort level between statement and operator attributes but of course you should only pass operator attributes to operators and statement attributes to statements. Steven