Home

CafeOBJ User`s Manual — ver.1.4.8 (Draft) —

Contents

1. 4 2 3 Behavioural Equation Declaration 4 3 Transition Declaration on isa e ao eee ee eS 44 Internalising AXIOMS 222522200 a 4 4 1 Equality Predicate gt o o a os ea 26 46444 aa re do 4 4 2 Transition Predicate ooo A ee w 4 4 3 Behavioural Equivalence Predicate 4 4 4 Sort Predicate o o e a ke e he RR a pea e os 5 Inspecting Modules 5 1 Using Inspection CommandsS e 5 1 1 Printing Whole Modules e o coc caes u ooe a a 5 1 2 Print Park or Modules vo ea ok dp ee ee ie a a Bula Deep Inspection i oa 6 aie Ge e a ea a ee eS 5 1 4 Inspecting Records gt i oa pee eaa a a ee es 5 2 come Typical Modules o pa we ee eee ak eh ee ao Tal Unique Models o cea aco orani a a a ee e es Maa Inspecting Transition Axioms o aaa 5 2 3 Non isomorphic Models aaa 5 2 4 Inspecting Hidden Sorts gt o s ec ca aeea 4 24 6 Evaluating Terms 61 Term Rewriting System ca cec 24 6 fee a E Gdl Wet deo TRI 2 5 4 ood 3 ee ee ee a a E ee e 6 1 2 How a Module Defines a TRS 6 2 Do the Eyasluation oo eors pa EE MAREE PERERA EO 0 21 Evaluation Commands sa e cc s e es 6 2 2 Replacing Equals by Equals o s aoeeoe amwa na p ea ai 6 23 Equations and Transitions gt e ccoo e ce eac 6 2 4 Using Behavioural Equations iii 23 24 26 26 27 27 29 32 33 34 35 37 37 39 39 41 41 42 43 43 44 46 47
2. L eq empty 0 8 3 4 Parameters with Parameters There are also cases when parameter modules themselves are parameterised Consider the following example module ONE Elt gt module STACK X ONE 4 Stack op push Elt Stack gt Stack module TRAY Y STACK Tray op tray Stack Stack gt Tray ops in tray out tray Tray gt Stack op in Elt Tray gt Tray var E Elt vars S S Stack eq in E tray S S tray push E S S trans tray push E S S gt tray S push E S eq in tray tray S S S eq out tray tray S S 9 The module TRAY is intended to describe the desk of an important executive The parameter STACK of this module itself has a parameter ONE the same as the one in Section 8 2 1 There are two ways to instantiate TRAY a Instantiate Y or b Instantiate X of Y 135 8 MODULE STRUCTURE In case of a Y should be bound by a module which has the same module ONE as parameter For example if you have defined module LIST X ONE 4 NeList lt List op nil gt List op __ Elt List gt NeList op __ Elt NeList gt NeList op head_ NeList gt Elt op tail_ NeList gt List var E Elt var L List eq head E L eq tail E L mou Pw you may bound LIST to the parameter Y as view LIST AS STACK from STACK to LIST 4 sort Stack gt NeList op push gt module LIST TRAY protecting TRAY
3. Recall that when we gave a view for MONOID Section 8 2 4 the associativity axiom remained to be proven This obligation was discharged just now Similarly commutativity is proven by proving commutativity of _ open SIMPLE NAT ops ab gt Nat reduce 0 0 0 0 eqb 0 0 b inner hypothesis reduce s b 0 0 s b eq a X Nat X a outer hypothesis reduce 0 s a s a 0 eq b s a s a b inner hypothesis reduce s b s a s a s b close The proof relies on double induction And in this proof the direction of equations is crucial in giving the equation marked if you exchanged the sides the subsequent evaluations would produce false To get true you need reverse applications by using apply 10 2 2 Nondeterministic Transitions Since the current implementation of evaluation mechanism is deterministic it is impossible to prove transition relations by execute command alone In such a case the transition predicate _ gt _ is often useful As explained in Section 4 4 2 _ gt _ is supported by _ gt _ which systematically checks transitions step by step Recall CHOICE NAT Section 5 2 1 and let us prove a simple fact that If t transits to u t also transits to u for any t Cafe0BJ gt open CHOICE NAT opening module CHOICE NAT done CHOICE NAT gt ops abc gt Nat CHOICE NAT gt trans a gt c CHO
4. s s s 0 reduce in MULT s s 0 s s s 0 gt gt stepper term s s 0 s s s 0 STEP 1 p stop pattern 0 N Nat STEP 1 c gt gt subterm 0 s s s 0 of term s s s s s s 0 0 s s s 0 matches to stop pattern 0 N lt lt will stop rewriting gt gt stop because matches stop pattern gt gt stepper term s s s 0 0 s s s 0 STEP 7 set stop pattern STEP 7 c s s s s s s 0 NzNat 0 010 sec for parse 11 rewrites 0 030 sec 19 matches MULT gt p prints the term given by set command and c resumes reduction The system stopped when a matching term appeared as requested After the restriction was lifted the reduction continued uninterrupted You may print the current pattern as STEP 1 show stop stop pattern 0 N Nat STEP 1 instead of p This command can be invoked without entering the stepper In fact pattern restrictions may be used outside the stepper For example 81 6 EVALUATING TERMS MULT gt set step off MULT gt set stop pattern O N Nat MULT gt show stop stop pattern 0 N Nat MULT gt reduce s s 0 s s s 0 reduce in MULT s s 0 s s s 0 gt gt subterm 0 s s s 0 of term s s s s s s 0 0 s s s 0 matches to stop pattern 0 N lt lt will stop rewriting s s s s s s 0 0 s s s 0 NzNat 0 000 sec for parse 6 rewrites
5. show let selection pending context modules views time limit stop features memo show all rule rule_specification switches switch_name 11 1 DIALOGUE WITH THE SYSTEM Again do not bother now Most of these arguments are unrelated and we explain the system s response separately for each of them in relevant chapters There is a command that enables you to look deeper into module definitions Syntax 16 describe command describe module_ezpression describe all sorts ops sign axioms module_expression describe vars params subs module_expression describe sort sort_name op operator_name module_ezpression In using the system you may notice that it treats show and describe in com bination In fact Cafe0BJ gt show lets you know the syntax of describe as well as show Try also CafeOBJ gt describe 12 Module Declaration The basic building blocks of CafeOBJ are modules This chapter explains the outermost structure of a module 2 1 Overall Structure A module without parameters has the following syntax Syntaz 17 module without parameters module module_name module_element my A module name is an arbitrary character string A module element is either 1 import declaration 2 sort declaration with ordering 3 operator declaration 4 record decla ration 5 variable declaration 6
6. SIMPLE NAT gt select CHOICE NAT CHOICE NAT gt set stats on CHOICE NAT gt reduce s 0 s s 0 s s s 0 reduce in CHOICE NAT s 0 s s 0 s s s 0 s 0 s s s s s 0 Nat 0 010 sec for parse 3 rewrites 0 000 sec 5 matches CHOICE NAT gt execute s 0 s s 0 s s s 0 execute in CHOICE NAT s 0 s s 0 s s s 0 s 0 NzNat 0 000 sec for parse 1 rewrites 0 000 sec 1 matches CHOICE NAT gt show all rules rewrite rules in module CHOICE NAT 1 ceq cvi Nat cv2 Nat gt cv3 Nat cv4 Nat true if cv1 Nat gt cv3 Nat and cv2 Nat gt cv4 Nat 2 ceq s cvi Nat gt s cv2 Nat true if cvi Nat gt cv2 Nat 3 ceq cvi Nat cv2 Nat gt cv3 Nat cv4 Nat true if cv1 Nat gt cv3 Nat and cv2 Nat gt cv4 Nat 4 eq N N gt N true 5 eq N N gt N true 6 trans N N gt N 7 trans N N gt N 8 eq0 N NMN 9 eq s N N s N N 10 We omitted the rest of the listing which contains axioms in BOOL reduce command ignores transition declarations 6 and 7 so the reduction stopped after rewriting the second argument of _ _ execute applied the rule 6 immediately and just one rewrite see the statistics led to the result Technically the TRS faithful to the underlying model should be a TRS de rived entirely from transitions over equivalence classes of terms determined by equations The current system does not disti
7. STEP 3 n 3 s s s 0 s 0 s s s 0 gt s s s 0 s 0 s s s 0 gt gt stepper term s 0 s 0 s s s 0 STEP 4 which shows the stepper is focusing more and more inside To skip several steps use g 78 6 3 Stepper STEP 4 set trace whole off STEP 4 g 5 gt gt stepper term s 0 0 s s s 0 STEP 9 g 5 s s s s s s 0 NzNat 0 010 sec for parse 11 rewrites 0 040 sec 19 matches MULT gt show command may take arguments term and tree Then a tree form of the term is printed See Section 9 2 3 for an example The rest of the commands act as follows MULT gt reduce s s 0 s s s 0 reduce in MULT s s 0 s s s 0 gt gt stepper term s s 0 s s s 0 STEP 1 a s s 0 s s s 0 Nat 0 000 sec for parse 1 rewrites 0 000 sec 2 matches MULT gt a stops the evaluation immediately MULT gt reduce s s 0 s s s 0 reduce in MULT s s 0 s s s 0 gt gt stepper term s s 0 s s s 0 STEP 1 n gt gt stepper term s s s 0 s 0 s s s 0 STEP 2 r s N Nat N Nat s N Nat N Nat STEP 2 s N Nat gt s 0 s s s 0 N l gt s s 0 STEP 2 c s s s s s s 0 NzNat 0 000 sec for parse 11 rewrites 0 010 sec 19 matches MULT gt r and s show the rule and the substitution to be used in the next step study the
8. sort Bar gt Foo is equivalent to module FOO protecting BAR sort Bar gt Foo Principal Sort principal sort can be abbriviated to psort Import Mode For import modes the following abbriviations can be used Keyword Abbriviation protecting pr extending ex including inc using us Simultaneous Operator Declaration Several operators with the same arity coarity and operator attributes can be declared at once by ops The form ops operator_symbol operator_symboln arity gt coarity op_attrs is just equivalent to the following multiple operator declarations op operator_symbol arity gt coarity op_attrs op operator_symboln anit gt coarity op attrs bops is the counterpart of ops for behavioural operators 182 A 2 CafeOBJ Syntax bops operator_symbol arity gt coarity op_attrs and the effect is the same as many operators as there are operator_symbolss In simultaneous declarations parentheses are sometimes necessary to separate operator symbols This is always required if an operator symbol contains dots blank characters or underscores Predicate A predicate is a syntactic sugar for operator declarations with arity Bool and is defined as predicate pred operator_symbol arity op_attrs The form pred operator_symbol arity op_attrs is equivalent to op operator_symbol arity gt Bool op_attrs Operator Attributes The following abbriviations
9. term all rules rules rules term apply action substitution range selection n regularize module_name 10 11 12 13 Bibliography Dershowitz N and Jouannaud J P Rewrite Systems Handbook of Theoretical Computer Science Vol B Formal Models and Semantics The MIT Press Elsevier Sci ence Publishers 1990 pp 245 320 Diaconescu R and Futatsugi K Logical Semantics of CafeOBJ Technical Report IS RR 96 00245 Japan Advanced Institute for Science and Teleology 1996 Diaconescu R and Futatsugi K CafeOBJ Report World Scientific 1998 Ehrig H and Mahr B Fundamentals of Algebraic Specifications 1 Equations and Initial Semantics Springer Verlag 1985 Goguen J and Burstall R Institutions Abstract Model Theory for Specification and Programming Journal of the Association for Computing Machinery Vol 39 1992 pp 95 146 Goguen J and Diaconescu R An Oxford Survey of Order Sorted Algebra Mathe matical Structures in Computer Science Vol 4 1994 pp 363 392 Goguen J and Malcom G A Hidden Agenda technical report UCSD 1998 Goguen J A and Meseguer J Order Sorted Algebra 1 Equational Deduction for Multiple Inheritance Polymorphism Overloading and Partial Operations Technical Report SRI CSL 89 10 SRI International 1989 Goguen J Winkler T Meseguer J Futatsugi K and Jouannaud J P Introducing OBJ Technicha
10. At last the condition was satisfied and the system rewrote the original term You may continue this time applying the rule 3 GCD gt apply 3 at term shifting focus to condition condition 1 not s 0 lt O Bool Y GCD gt But reduction of _ lt _ is obvious so you apply reduce at once GCD gt apply reduce at term condition 1 true Bool condition is satisfied applying rule shifiting focus back to previous context result gcd s s 0 s 0 s 0 Nat 7 GCD gt The original term was further rewritten and you can continue as before As shown by this frustrating example what apply basically offers is a painful step by step reasoing There are ways to skip certain parts at one go One way is to invoke the action reduce as above In the case of conditional rewrite rules there is another systematic way to do it Let us redo the above session using this mechanism 155 9 THEOREM PROVING TOOLS GCD gt start gcd s 0 s s 0 7 GCD gt set reduce conditions on GCD gt apply 1 at term result gcd s s 0 s 0 Nat GCD gt apply 3 at term result gcd s s 0 s 0 s 0 Nat GCD gt apply 1 at term Warning rule not applied result gcd s s 0 s 0 s 0 Nat GCD gt The switch reduce conditions when on makes the system to evaluate conditions au tomatically 9 3 Matching Terms Matching is a basic procedure in evaluation Section 6
11. EGO a O a Gora a a 0 where we omitted parentheses since _ _ was declared associative This proof requires two reverse applications of rewrite rules 9 2 1 Start Then Apply To accommodate such proofs as above CafeOBJ supports the following set of commands Syntax 73 start command start term where a term is a term of the opened module Section 9 1 or in the current context Section 8 1 1 This command sets the focus on the given term which may be printed and referred to in the subsequent commands show command Section 1 3 3 with term as argument prints the term just selected Syntax 74 apply command apply action substitution range selection where the action substitution range and selection are as follows reduce action exec print rewrite_rule where a rewrite rule is Syntaz 75 rule specification in apply command module_name number label If the action is reduce or exec the sub term specified by the range and selection is reduced If it is print the sub term is printed If it is a rewrite rule the chosen rule is applied once to the subterm In the last case the numbered or labelled rule of the module if omitted of the opened module is used from left to right if the sign is or none or right to left if We will first show a couple of examples in Section 9 2 2
12. SIMPLE NAT gt close Cafe0BJ gt You may have noticed quizzical in the above session They are not print smudges When a module is opened the system processes the subsequent declarations and commands as if they were entered during a normal module declaration and tries to tell you that it is working furiously cf an aside in Section 2 4 As you may have noticed in the above example the current implementation requires a blank period terminator for each declaration note after the operator declaration above The opened module and the current module need not be the same For example if the current module is NERD you can have a session like NERD gt open SIMPLE NAT opening module SIMPLE NAT_ done SIMPLE NAT gt select BOOL BOOL gt close NERD gt By opening SIMPLE NAT the temporary new module is set to be current as indicated by the prompt select command switches the current module to BOOL close restores the previous current module remember that the effects of declarations and commands during opening are temporary A convenient way to set the current module while it is opened is selecting the module 143 9 THEOREM PROVING TOOLS SIMPLE NAT gt select SIMPLE NAT gt As you have guessed the module name refers to the temporary module You should not use as a module name 9 1 2 Constant On the Fly Let us think awhile of the example of the previo
13. Y G Y G X substitution 1 Y G gt a a X gt 0 H 4iseqa X a Xta substitution X gt a gt GROUP gt The system lists applicable rules to the term 0 a a In this output a rule is num bered adorned with the module name the opened module cf Section 9 1 1 and a sign Remember that this form appears in arguments to apply command Section 9 2 4 You may have noticed two differences from the cases of matching terms to terms 159 9 THEOREM PROVING TOOLS e Not all possibilities are considered In the above output only one matching possibility is shown for the rule 3 even though there are two possibilities see the previous section e All the subterms of the given term is under consideration The rule 4 does not match The case where 160 the whole term but does match a subterm rules is specified is similar GROUP gt match term to rules matching rules to term 0 a a Z 1 is eq0 X X substitution X gt O tata 3 is eq X Y G Y G X substitution Y G gt 0 X gt a a 20 is eq if true then CXU else CYU fi CXU substitution CXU gt 0 a a 21 is eq if false then CXU else CYU fi CYU substitution CYU gt 0 a t a GROUP gt The last two printed rules are of BOOL actually a submodule thereof This Y i rule is always applicable in reverse since the righthand side is a single variable Prov
14. is a new prompt As you see TEST is the name of the module just selected The system maintains a module lAs you see in the example above system may load some other modules required for defining your module In this case TRUTH and BOOL are loaded in automatic These are modules which provides built in Boolean types and operations More on this at page 18 1 1 Hello Goodbye called the current module that is the focus of manipulation at the time The initial prompt Cafe0BJ gt indicates the current module is not yet supplied Or a module cafeobj is now current it is possible if confusing to define such a module Various commands such as parsing and reduction are executed under the current module For more details on current modules see Section 8 1 1 1 1 2 Quitting the System To quit CafeOBJ type quit or q for short or the end of input character usually control D at a prompt Then the interpreter terminates and the control is given back to the original shell Cafe0BJ gt quit Leaving Cafe0BJ 1 1 3 Emergency Resumption and Bug Reports In detecting errors CafeOBJ growls Cafe0BJ gt module ERROR Error was expecting the symbol not Cafe0BJ gt The above message starting with Error indicates that the system detected a syntax error in processing your input Due to irrecoverable input errors or just to mulfunctions CafeOBJ may stop abnormally and throw the contro
15. lt lt s s s s 0 s s s 0 NzNat 0 000 sec for parse 5 rewrites 0 000 sec 9 matches MULT gt You should use set command instead of rwt command the latter is recognised only in the stepper To lift the restriction set the limit to MULT gt set rwt limit MULT gt show limit rewrite limit not specified MULT gt reduce s s 0 s s s 0 reduce in MULT s s 0 s s s 0 s s s s s s 0 NzNat 0 000 sec for parse 11 rewrites 0 000 sec 19 matches MULT gt As shown above show command with 1imit argument prints the specified limit If both the pattern and limit restrictions are in force the system aborts reductions at the earliest opportunity 6 4 Faster Evaluation Such commands as reduce treat terms and rewrite rules as Lisp objects and the rewrite procedure manipulates these objects directly If the rule set is huge and or the term is or will grow large the system may become uncomfortably slow A way to overcome the discomfort is to invest in a faster machine with a larger memory of course but there is another cheaper way For faster evaluation you may encode rewrite rules into an abstract machine and reduce terms by executing that machine with the following command Syntax 53 tram command for evaluation tram reduce execute in module_expression term e 83 6 EVALUATING TERMS reduce execute may be abbreviated to red exec respe
16. reduce in FACT 4 2 2 NzNat 0 000 sec for parse 14 rewrites 0 020 sec 24 matches FACT gt The original term is parsed as a term of sort Rat as before and the result of evaluation is a term 2 of sort NzNat Indeed this result is the 2 s factorial i e 4 2 s factorial And NzNat is not dubious On the other hand if you supply a meaningless term the result remains dubious FACT gt reduce 4 3 reduce in FACT 4 3 4 3 Rat 0 010 sec for parse 1 rewrites 0 000 sec 1 matches FACT gt To summarise in Cafe OBJ 1 If a term is ill formed but potentially well formed it is regarded as a well formed term of questionable sort 2 On evaluation the potential is investigated If the result is a term which is unques tionably well formed it acquires a full citizenship Otherwise it remains an outcast 6 6 2 Stacks Stacks are ubiquitous topics in our community especially in discussing exception error handling The main reason is that their definition is compact yet reveals or conceals how top empty a raving exception is treated The module below declares a sort of non empty stacks and top and pop are declared on that sort not on the sort of all the stacks In effect top and pop are partial operators 90 6 6 Flexible Typing and Error Handling module STACK OF NAT NeStack lt Stack protecting SIMPLE NAT op empty gt Stack op push Nat Stack gt NeStack op top
17. 8 restore 5 rewrite 77 rew 77 rules 67 151 157 rule 77 153 rwt 82 83 r 77 save system 6 save 5 select 2 115 set 10 11 19 28 44 53 66 68 76 80 83 115 show 9 11 67 78 81 83 86 146 149 151 153 signature 14 28 sig 15 sorts 53 sort 124 137 start 146 stats 68 step 76 stop 77 80 81 strat 101 subst 77 subterm 147 149 157 switch 85 s 77 term 78 146 147 157 top 147 157 to 124 131 trace whole 66 71 trace 66 71 167 tram 83 84 trans 42 trns 42 unprotect 13 using 19 vars 37 var 37 53 view 124 131 whole 66 within 147 A amalgamated sum 138 arity 24 associativity 95 attribute 26 attribute of operators 95 autoloading 6 B behavioural context 60 behavioural equation 41 behavioural operator 26 behaviourally equivalent 60 block of declarations 14 boolean term 41 built in module 175 C canonical TRS 65 coarity 24 coditional equation 41 coinduction 171 comment 17 commutativity 95 compatible 162 condition of an equation 41 conditional rewrite rule 75 confluent 65 constant 24 constructor attribute 101 context behavioural 60 context module 115 context indution 171 context variable 85 current module 3 30 52 65 115 D derived operator 122 derived signature 122 E E matching 64 E strategy 101 emacs 8 equational the
18. GCD gt show context current context module special bindings term s 0 lt s s 0 Bool subterm term bindings empty selections empty pending actions 1 in gcd s 0 s s 0 at top rule ceq gcd N M gcd M N if N lt M condition s 0 lt s s 0 replacement gcd s s 0 s 0 stop pattern not specified Y GCD gt It looked certain that the rule 1 would apply so you tried it The system then told that since that rule was conditional it had to resolve the condition first show command with argument were partly explained in Sections 8 1 1 and 9 2 3 What was remained was the misterious heading pending actions This part is used exactly in a situation like now and contains terms to be further reduced after a condition the current focus has been evaluated The instance of the condition requires rules in SIMPLE NAT Section 6 2 6 so you have to continue as follows 154 9 2 Applying Rewrite Rules GCD gt show rules SIMPLE NAT rewrite rules in module SIMPLE NAT 1 eq0 M 0 2 eqN 0 N 3 eq s N sM N M 4 eq 0 lt s N true 5 eq N lt 0 false 6 eq s N lt s M N lt M 7 GCD gt apply SIMPLE NAT 6 at term condition 1 0 lt s 0 Bool GCD gt apply SIMPLE NAT 4 at term condition 1 true Bool condition is satisfied applying rule shifiting focus back to previous context result gcd s s 0 s 0 Nat Y GCD gt
19. To check the necessity of such extra equations is not easy As of now the system bets on the safer side and adds equations nonchalantly 113 Module Structure 8 1 Names and Contexts 8 1 1 Context and Current Module Import declarations define a hierarchy of modules As a directed graph it is acyclic a module cannot import itself either directly or indirectly The directed acyclic graph is called context and for a paricular module M in the graph the complete subgraph reachable from M is called the context of M You may regard the context of M as collections of sorts operators variables and axioms which can be referred to within M The concept of current module is to establish a context in the above sense Such commands as reduce and parse presuppose a context The current module is set by the following command Syntar 58 select command select module_name You are always reminded of the current module by the prompt you already have seen many session examples You may make the context follow your every step so that if you define a module or inspect its contents the current module switches to that module by the command CafeOBJ gt set auto context on The default is off The effects of this switch are illustrated in the following session 115 8 MODULE STRUCTURE Cafe0BJ gt set auto context on Cafe0BJ gt module M S ope gt S defining module M _ done M gt module N
20. You may list the commands available in this mode by the help command 76 6 3 Stepper STEP 1 Stepper command help E n ext g o lt number gt c ontinue q uit a bort r ule s subst 1 imit p attern stop lt term gt rwt lt number gt the followings show or describe set cd lt directory gt ls lt directory gt pwd lisp or lispq lt lisp gt lt command gt STEP 1 print out this help go one step go lt number gt step continue rewriting without stepping leave stepper continuing rewrite abort rewriting print out print out substitution print out print out stop pattern set unset stop pattern current rewrite rule rewrite limit count set unset max number of rewrite are subset of cafeobj interpreter commands print various info for further help type show set toplevel switches for further help type set change current directory list files in directory print current directory evaluate lisp expression lt lisp gt fork shell lt command gt Under Unix only Some of them such as show set and cd should be familiar They are not particular to the step mode Particular to the mode are the commands prefixed by rwt and stop ay in addition to The prefix may be omitted and there are longer forms for some step mode commands Here is a summary of synonyms a Pp he
21. and denotes your home directory If there is no file with the pathname the system expands the name with suffixes kbd cafe or bin and re search the directory By convention a file suffixed with cafe is assumed to contain definitions and commands written in CafeOBJ while bin indicates a file containing internal codes Normally you should prepare cafe files yourself and leave the system to create bin files see Section 1 23 Some directory traversal commands of Unix are also available Syntar 3 cd command cd pathname Syntaz 4 pwd command pwd Syntar 5 1s command ls pathname where pathnames must be those of directories The above commands act like their namesakes in Unix shells but are not exactly the same The arguments to cd 1s are not optional but necessary Also the system does not recognise bimbo as the home directory of bimbo 1 2 2 Saving and Restoring Module definitions may be saved in an internal format for efficient later retrieval The commands Syntar 6 save command save pathname Syntax 7 restore command restore pathname save restore module definitions into from the designated file Pathnames must be those of files To adhere to the system s convention file names should be suffixed with bin In place of restore command you may also use input command Section 1 2 1 save saves the c
22. binds a SIMPLE NAT to the parameter IDX and DAT via an identical view from ONE see Section 2 2 for SIMPLE NAT Section 8 2 1 for ILIST and ONE The code is equivalent to view V from ONE to SIMPLE NAT sort Elt gt Nat module NAT ILIST protecting ILIST IDX lt V DAT lt V An ephemeral view may be as succinct as a everlasting counterpart with resort to princi pality and titular coincidence To make the code more concise it is possible to identify parameters by positions not by names NAT ILIST may then be defined by module NAT ILIST protecting ILIST V V 131 8 MODULE STRUCTURE or more ephemerally module NAT ILIST protecting ILIST SIMPLE NAT sort Elt gt Nat SIMPLE NAT 4 sort Elt gt Nat Note that in the latter code view to constructs are omitted 8 3 2 Parameters as Imports A parameter may be regarded as a submodule If so regarded it poses a question of importation modes Section 2 5 and module contexts Section 8 1 1 Indeed it is possible to specify an importation mode for a parameter as in module M extending X T M Available modes are the same as with plain importations protecting extending and using The default mode is protecting You can check by feeding ILIST Section 8 2 1 and print parameters as follows CafeOBJ gt select ILIST ILIST IDX DAT gt show params argument IDX protecting ONE argument DAT protecting ONE ILIST IDX
23. eq t gt t true and for each conditional transition ctrans t gt t ifc the system declares ceq t gt t true if c These declarations correspond to one step transitions Thirdly for each operator declaration op f Sil ooo BN e the system declares ceq X1 S1 Xn Sn gt X1 S1 Xn Sn true if X1 gt X1 and and Xn gt Xn which states that _ gt _ is closed under f s application As to transitivity a straightforward declaration would not do an axiom of the form ceq X S gt X S true if X gt X S and X gt X introduces an extra variable in the condition which makes it inappropriate for the purpose of evaluation cf Section 6 1 2 Considering that the main usage of the predicate gt is to prove theorems with evaluation mechanism this fact renders such an axiom useless In its place the system add the following axiom ceq X S gt X S true if X gt X Attached to the operator _ gt _ is a systematic search procedure for determining whether the first argument transits to the second in an arbitraty number of steps More on this and related operators in Section 10 2 3 45 4 AXIOMS 4 4 3 Behavioural Equivalence Predicate The predicate for behavioural equivalence written is a binary operator defined on each hidden sort As with and gt in prev
24. gt _ _ var N Nat var C Counter hsort Counter gt Account bop add N C gt deposit C N bop read gt balance Note first the appearance of Zero NzNat et al A view defines a mapping of all the sorts and operators including those declared in imported modules As a result views easily become large And quite often they contain a large uninformative set of maps the identitiy maps like here There is a way to cut them out See Section 8 2 6 Note also the usage of variables In mapping bop add Nat Counter gt Counter 4 Even implicitly imported modules We ignore them here for your health 128 8 2 Parameters and Views to bop deposit Account Nat gt Account you need to change the order of arguments Variables and derived opeartors are used to state this permutation In the term deposit C N the variable C is interpreted as that of Account according to the sort map from Counter to Account Let us return to conditions on views This mapping does not constitute a view since withdraw and point are not in the image of the mapping This oversight is harmful It can be shown that in COUNTER the behavioural equation beq add m n c add n add m c holds for any m n of sort Nat and for any c of sort Counter while its counterpart beq deposit a m n deposit deposit a m n in ACCOUNT does not The reason is that the observation point A Account distinguishes the two terms thus
25. op s s X Nat gt NzNat op s 0 X Nat gt Nat which of course we cannot write out fully since this signature is infinite 2 Actually not so easy You have to calculate a least sort 122 8 2 Parameters and Views Signature Morphisms A signature morphism is a structure preserving mapping from a signature to another For example signature cs lt 8 J H bop f H gt S y may be mapped to signature hess SS UA K lt K Wey fF 5 Mk e T E via the mapping S gt T Ss gt T H gt K f gt g which preserves sort ordering and visibility as well as ranks of operators To be definite given signatures and X a signature morphism is a pair of mappings h of sorts and h of operators such that hs preserves and reflects visibility i e S is visible hidden iff h S is hs preserves sort ordering i e you must have hs S lt h S if S lt S hs reflects sort ordering on hidden sorts i e you must have S lt S if h S lt hs S ho preserves ranks i e an operator f with rank S 5 gt S must be mapped to an operator with rank h S1 hs Sn gt hs S e h maps behaviourals to behaviourals bop to bop and op to op and e ho is surjective on behaviourals i e for any behavioural operator g in the target signature there must be a behavioural operator f such that ho f g Specification Morphism Signature morphisms take care of
26. to 2 2 to V1 and to Oi 1 under the usual number hierarchy We also require that The terms be of visible sorts Or are they both pie 39 4 AXIOMS For terms of hidden sorts behavioural equations Section 4 2 3 should be used Labels do not affect the semantics and may be omitted If not omitted it must be of the form Syntax 45 label in axioms Ei label_name 7 66 where a label name is a character string without blanks Since most non trivial equations involve variables and since unambiguous parsing is a non trivial question in examples below we put variable declarations near equation declarations To state that 0 is a right identity of addition you may write var N Nat eq r id N 0 N or using an on the fly declaration eq r id N Nat O N Look at the second occurrence of N in this equation In general the scope of an on the fly declaration is the whole enclosing term or more precisely in the rest of the term For example the second N of N Nat s N is the same N as declared on the fly since they are both in the same term As a special rule a variable declared within an axiom is valid throughout that axiom The above equation illustrates this special rule On the fly declarations may overwrite the previous declarations For example in module S CS wv op f S gt S var X T eq X S f X the variable X was declared as of
27. trans a gt d The system does not evaluate the corresponding term to true as M gt reduce a gt d reducen Mik a gt d gt pre normalization a no more possible transition for a b gt d Bool 0 000 sec for parse 4 rewrites 0 000 sec 12 matches M gt This is because the system reduces a to an irreducible form b before trying a systematic search If it had tried a search before normalising it would have proved the theorem There is a switch that tells the system to forget about normalisation M gt set exec normalize on M gt gt reduce a gt d reduce in M a gt d transition step 1 1 O a 1 gt c lt post nomalization c term d matched to the pattern d with the substitution true Bool 0 000 sec for parse 4 rewrites 0 010 sec 6 matches M gt The result was satisfactory This switch is hopeless if interleaving applications of equations and transitions are necessary In module M CS opsabcd eq e1 a eq e2 b trans t eq e3 d Il DLO 0 o Il v Qa Il o 170 10 2 Theorem Proving Techniques to prove trans a gt gt e you have to use e1 and only that 10 2 4 Behavioural Equivalence Recall COUNTER Section 5 2 3 and let us prove a behavioural equation beq add N Nat add N Nat C Counter add N add N C As explained this equation holds iff two terms act identically on every obse
28. 1 1 It may be useful by itself as a theorem proving helper since 156 e When you use reduce command it is a good practice to write down the expected result beforehand If the actual result differs you immediately notice something is going wrong A standard way to realise this practice is to use a printable comment gt or x gt Section 2 4 as reduce s s 0 s 0 gt should be s s s 0 The system then prints reduce in SIMPLE NAT s s 0 s 0 s s s 0 NzNat 0 000 sec for parse 3 rewrites 0 000 sec 5 matches gt should be s s s 0 so that you can compare the actual and expected results easily A more sophisticated mechanism is to invoke a matching procedure And In using reduction and apply commands for theorem proving it is necessary to know what rewrite rules are applicable to what terms You can inspect the rules by show command but if the set of rules is large it is tedious A tool to list applicable rules is helpful Applicable here means having matchable lefthand side 9 3 Matching Terms 9 3 1 Match Command Syntar 78 match command match term_specifier to pattern e The last period preceded by a blank is necessary Term specifiers and patterns are as follows term_specifier top term it subterm term where a term is a usual term top or the literal term means the term set by start command subterm means the ter
29. 2 Do the Evaluation module SIMPLE NAT protecting SIMPLE NAT op _ _ Nat Nat gt Nat op _ lt _ Nat Nat gt Bool vars NM Nat eq0 M eqN 0 N eq s N sM N M eq 0 lt s N true eq N lt 0 false eq s N lt sM N lt M I o module GCD 4 protecting SIMPLE NAT op gcd Nat Nat gt Nat vars N M Nat ceq gcd N M gcd M N if N lt M eq gcd N 0 N ceq gcd s N s M gcd s N s M s M if not N lt M The definitions of the pseudo subtraction and the less than relation are more or less stan dard gcd is defined by conditional equations Note that BOOL is imported implicitly so that all the operators in it like not_ here are available To see how these definitions work continue the session in the previous section Feed the modules to the system and try as follows SIMPLE NAT gt set trace off SIMPLE NAT gt select GCD GCD gt reduce gcd s s s s s s 0 s s s s 0 reduce in GCD gcd s s s s s s 0 s s s s 0 s s 0 NzNat 0 000 sec for parse 44 rewrites 0 010 sec 113 matches GCD gt The reduction amounts to computing the greatest common divisor of 6 and 4 The statistics show that the system worked much harder than ever You may get traces as before Since the output is largish we show traces of simpler computations but this is still large 73 6 EVALUATING TERMS 74 GCD gt set trace whole on GCD gt reduce gcd s
30. 49 49 49 50 53 55 57 57 58 59 60 63 63 63 64 65 65 66 68 69 71 iv CONTENTS 6 2 6 Examples of Conditionals 2 00004 72 6 3 SEGPPOl kc A ee be ek eae ne eee ea ee ea dee 76 6 3 1 Re MOS ee ke as in SO ek A a ee Ee Ba 76 Gaz Evaluation Under the Step Mode 78 6 3 8 Controlled Reduction by Patterns 80 6 3 4 Controlled Reduction by Number of Steps 82 6 4 Faster valuation 6 is SR Ke ee wm ee ee Be Le ees 83 6 5 Context Variable 66 2 66 24 cd a Pw we we 85 6 6 Flexible Typing and Error Handling 88 66 1 Factorial of Rationale 17 co 0 04 22282 h54 650455 89 6 6 2 o TEA 90 6 6 3 Handling Errors as Errors o o eo a boa ogee 92 7 Operator Attributes 95 Tel Equational Theory Attribute a 95 TAL AROAN o sikaa dee ha wR Re g A a E 96 T1 1 2 Community a ee rada a a a 97 TL a A Ba BO PY ee ee Bee ae ee aa 97 7 1 4 Idempoteney cc eck Ae aL eS he ee BR GO a 98 1 LS Inheriting Equational Theory Attributes 98 a Pasme AME oca Oe ee aa we eR ER i a a a 99 121 Precedence o saos coe sora do a ee 99 Taa Left Right Associativity e s onore i 20422 prosas dau 100 Tea Constructor AGiribiite os a ee e a a a 101 TA Evaluation Strategy 26 cc eee a eR ee eS ee a 101 741 E Strategy Attribute o o 101 7 4 2 Default Seraheey ono A AAA ad 102 7 4 3 Lazy Evaluation oa a A a we ee eR
31. 5444400 abe do AIS Comments o sea ss ke criada a a a a CafeOBI Syntax scada RRA ees 129 130 130 132 133 135 137 137 137 137 138 139 141 141 141 144 145 146 147 149 151 153 156 157 157 159 161 161 164 165 166 168 171 172 175 177 177 177 177 178 178 178 179 vi A 2 1 A 2 2 A 2 3 A 2 4 A 2 5 A 2 6 A 2 7 CafeOBJ Codes Modules o osa Module Expression VIEWS o roe a wa wok hika Evaluation Commands DET o a Sugars and Abbreviations B Command Summary Bibliography Index CONTENTS 179 180 181 181 181 181 182 185 187 189 Introduction CafeOBJ is a specification language based on three way extensions to many sorted equa tional logic the underlying logic is order sorted not just many sorted it admits unidi retional transitions as well as equations it also accommodates hidden sorts on top of ordinary visible sorts A subset of CafeOBJ is executable where the operational semantics is given by a conditional order sorted term rewriting system These theoretical bases are indispensable to employ CafeOBJ properly Fortunately there is an ample literature on these subjects and we are able to refer the reader to e g 4 13 for basics of algebraic specifications 8 6 for order sorted logic 7 for hidden sorts 10 for coinduction 12 for rewriting logic 5 for institutions and 11 1 for term rewriting systems
32. Commands 1 3 1 Help Command and Top level Commands Help commands of CafeOBJ in general employ instead of help aide moi socorro and so on You may remember that the welcoming message contained the line Type for help saying that the topmost help command is Syntaz 11 command listing command help command which lists the top level commands They may be classified as follows Starting module declarations module Section 2 1 view Section 8 2 3 and some others introduce building blocks of CafeOBJ codes They are to be explained in detail in the rest of the manual 1 DIALOGUE WITH THE SYSTEM Checking properties of modules check Section 10 1 Managing systems quit Section 1 1 select Section 8 1 1 set Section 1 3 2 protect Section 2 1 and others Managing files input Section 1 2 1 save Section 1 2 2 and others They should be already familiar to you Peeping systems show and describe Section 1 3 3 are at your command Evaluating terms reduce execute and some others Part of set command also concerns evaluation They are all explained in Chapter 6 Helping theorem proving apply open et al They shall be explained in Chapter 9 Many commands have abbreviations We list them below For a complete list of abbrevia tions see Appendix A 2 7 module mod module mod module mod quit q show sh describe desc input in reduce re
33. DAT gt Note in passing that the new prompt shows parameters as well as the module name ILIST As stated in Section 2 5 the system does not care if you have chosen an incorrect J importation mode Since various modules are to be bound to parameters you should be especially cafeful As to contexts a parameter is included in the context graph of the module The difference from plainly imported modules is that the edge has a name For example if M imports M the edge is anonymous M M while if M has a parameter X M the edge is Ms w Moreover since a module may have the same parameter with different names a context graph is in general a hypergraph 132 8 3 Binding Parameters Some aspects of instantiation is better explained in terms of such graphs Instantiation is then a process of subgraph replacement and the usual considerations indentifying which edges with which determining targets of edges avoiding dangling edges and so on are relevant to the process of instantiation 8 3 3 Parameter Passing Since a parameterised module is a module it may be imported You may enrich ILIST Section 8 2 1 adding an operator that counts entries module ILIST EXT protecting ILIST protecting SIMPLE NAT op _ Ilist gt Nat var I Elt IDX var D Elt DAT var L Ilist eq put I D L s 0 L eq empty 0 The definition of _ is obvious but this module is interesting
34. Float and is identified with 21 0 2 1 is an element of Rat and is identified with 2 The built ins and their definitions may change 175 Summary of CafeOBJ syntax Here is a brief summary of lexical conventions and syntactic definitions used in CafeOBJ codes and commands A 1 Lexical Analysis On the lexical surface a CafeOBJ code is a sequence of tokens and separators A token is a sequence of printable ASCII characters octal 40 through 176 and is classified as either a self terminating character an identifier or an operator symbol Each class is explained below A separator is a blank character space vertical tab horizontal tab carriage return newline or from feed On the one hand any mumber of separators may appear between tokens On the other hand one or more separators must appear between any two adjacent non self terminating tokens A 1 1 Reserved Words There is no reserved word One can use such keywords such as module op var or signature etc for identifiers or operator symbols A 1 2 Self Terminating Characters A self terminating character is a printable ASCII character which by itself constitutes a token There are seven such characters 1The current system accepts Unicode characters also but this is beyond the definition of the language 2The same rule applies to terms Further if an operator symbol contains blanks or self terminating characters it is sometimes neccessary to enc
35. Module Sunt z e ss sarosa RR ee ee ee 8 4 4 Making Modules 9 Theorem Proving Tools Open Closing Modules o e 9 1 1 Why Opening Modules o 9 1 2 Constant On the Fiy oca 46 eke eR a Applying Rewrite Rules cocos mesas he S 9 2 1 Start Then SAPPY ve ak ke GE eb a ae ee ee we Re 9 2 2 Applying Apply Command 9 2 3 Choosing Bwhterms s s ose ewe e Be 9 2 4 Identifying Rewrite Rules o 9 2 5 Appyling Conditionals sc eseo ss toe o e Matehing Terms soeces eaa k aea dd A 9 3 1 Match Command gt so cor 2602 paea r Ae a Ae GO ai 8 3 2 Matching Terms to Terms o G35 Matching Terms to Pattern 10 Proving Module Properties Check Command o s s Ga wea dad ke alow oe a Ae ek Theorem Proving Techniques MAT Sineu la darOR sa Gk Sa a a ee ea 10 2 2 Nondeterministic Transitions 0 6 10 2 3 Systematic Search for Transition Relations 10 2 4 Behavioural Equivalence o a 10 2 5 Behavioural Transition oo o e c 64005405 baa ee ene at 11 Built in Modules A Summary of CafeOBJ syntax A l A 2 Lexical Analysis o 62 sarera eie ee pa o eee o e ik A L l Reserved Words s s aso cc occa 2282022 Sse y eS OE Rb A 1 2 Self Terminating Characters Bilis JAMES ada aa a aa A ALA Operator Symbols oi sa s ecd
36. NAT Counter bop read Counter gt Nat bop add Nat Counter gt Counter eq read add N Nat C Counter N read C defining module COUNTER _ system already proved is a congruence of COUNTER done Cafe0BJ gt select COUNTER COUNTER gt show axioms Equations eq read add N Nat C Counter N Nat read C Counter ceq hs1 Counter hs2 Counter true if read hs1 Counter read hs2 Counter COUNTER gt In processing COUNTER the system added an equation after checking congruence 61 Evaluating Terms CafeOBJ has an operational semantics based on term rewriting system TRS s This chapter introduces the very basics of TRSs and explains when a CafeOBJ code constitutes a TRS 6 1 Term Rewriting System 6 1 1 What isa TRS This section is an intuitive introduction to the computation model of TRS s First a preliminary Substitution A substitution is a set S of pairs v t of a variable v and a ground term t such that no two pairs contain the same variable If v t is in S t is said to be the value of v under A Instantiation Given a substitution S and a term t replacing each occurrence of each variable in t with its value under S is called the instantiation of t by S Matching Given a ground term t and a term p if there is a substitution S such that the instantiation of p by S equals t t is said to be matchable to p To compute such a substitution is called matching Given a set
37. NAT gt Note that the prompt has changed to indicate what module is current It is possible to focus on a single sort operator or imported module For example 52 5 1 Using Inspection Commands SIMPLE NAT gt show sort Nat Sort Nat declared in the module SIMPLE NAT subsort relation Nat Nat Zero NzNat SIMPLE NAT gt show op _ _ rank Nat Nat gt Nat attributes strat 1 0 2 axioms eq0 N N eq s N N s N N SIMPLE NAT gt Here the subsort relation is shown graphically Nat is an error sort and you should ignore it for now cf Section 6 6 A switch controls whether the sort of each variable is displayed show Continuing the session you get SIMPLE NAT gt set show var sorts on SIMPLE NAT gt show op _ _ rank Nat Nat gt Nat attributes strat 1 0 2 axioms eq 0 N Nat N Nat eq s N Nat N Nat s N Nat N Nat SIMPLE NAT gt This switch does not have a total control In cases when sorts are not apparent when an axiom is from an imported module or when variables are redeclared on the fly and so on the system displays them willynilly 5 1 3 Deep Inspection If you want more detailed explanations of the module contents use describe in place of show This command is useful when you are evaluating terms Chapter 6 Since we have 53 5 INSPECTING MODULES not yet explained term evaluation mechanisms you should not expe
38. R of rewrite rules computation with R as TRS proceeds as follows given a ground term t 1 pattern matching Find a rewrite rule in R such that a subterm s of t is matchable to its lefthand side 2 rewrite If such a rewrite rule is found replace s in t with the instance of its righthand by the matching substitution and go back to 1 with the resulting new term 3 If no such rewrite rule is found terminate This procedure is called evaluation or reduction of t If the procedure terminates the resultant term is said to be irreducible or normal Note well that this procedure is for ground terms only 63 6 EVALUATING TERMS If a rewrite rule is conditional in addition to matchability you also have to check the condition To check the condition its instance by the matching substitution is evaluated The rule is applicable only when the condition evaluates to a term denoting true A TRS with conditional rewrite rules is called conditional TRS Another refinement of the above procedure is to match terms not only syntactically but modulo an equational theory E Such a mathching procedure is called E matching A typical equational theory is associativity Modulo associativity on an operator _ _ for example a b c matches X b Y where X Y are variables since the former term is equal to a b c CafeOBJ does support this kind of matching cf Section 7 1 There may be cases where
39. above example carefully c continues the evaluation non stop 79 6 EVALUATING TERMS MULT gt reduce s s 0 s s s 0 reduce in MULT s s 0 s s s 0 gt gt stepper term s s 0 s s s 0 STEP 1 q s s s s s s 0 NzNat 0 000 sec for parse 11 rewrites 0 010 sec 19 matches MULT gt reduce s s 0 s 0 reduce in MULT s s 0 s 0 s s 0 NzNat 0 000 sec for parse 7 rewrites 0 000 sec 11 matches MULT gt q forces the system to leave the step mode as the above example shows For 1 and p see the next section 6 3 3 Controlled Reduction by Patterns It is possible to stop reductions when a certain pattern is found Syntax 52 stop command stop term stop oo 3 where a term is a term in the current module context Section 8 1 1 and may contain variables Do not forget the last blank period stopper This command causes reductions to stop when the reductants get to containing subterms that match the given term If no term is given this restriction is lifted Alternatively you may use set command as Cafe0BJ gt set stop pattern t where t is a term This command is fast becoming obsolete and it is advisable to use the above set command instead We continue the session with MULT Note that the step switch is still on 80 6 3 Stepper MULT gt set stop pattern 0 N Nat MULT gt reduce s s 0
40. are available Keyword Abbriviation associative assoc commutative comm idempotent idem Axioms For the keywords introducing axioms the following abbriviations can be used Keyword Abbriviation Keyword Abbriviation ceq cq bceq bcq trans trns ctrans ctrns btrans btrns bctrans bctrns Blocks of Declarations Importationss signature definitions and axioms can be clusterd in blocks imports signature and axioms respectively 183 A SUMMARY OF CAFEOBJ SYNTAX imports imports import comment ay signature signature sort record operator comment rate axioms axioms variable axiom comment at Views It is possible to identify parameters by positions not by names For example if a parametric module is declared as module FOO A1 TH1 A2 TH2 4 y the form FOO V1 V2 is equivalent to FOO A1 lt Vi A2 lt V2 Moreover view to construct in arguments of module instantiations can always be omitted So FOO A1 lt view to module_ezpr can be written as FOO A1 lt module_expr Evaluation For eval the following abbriviations are available Keyword Abbriviation reduce red bereduce bred execute exec 184 Command Summary Following is the top level commands that do not constitute CafeOBJ codes 185 B COMMAND SUMMARY command show describe set input protect unprotect ful
41. are subject to frequent changes Some arguments to set command are not switches and may range over many values An example is libpath which was appeared in Section 1 2 5 The general syntax might be Syntar 13 set command for others set a_name option value but options and values are dependent on the name and names have no common character istic other than that they refer to something We shall explain them individually as the occasions arise 1 3 3 Inspection Commands show command prints information on modules system status et al The acceptable argu ments are many so you are wise to remember that Cafe0BJ gt show lists them all cf Section 1 3 1 The general syntax is complicated It is better understood when divided into two For the first half you have Syntar 14 show command for module inspection show module_expression show all sorts ops sign axioms module_expression show vars params subs module_expression show sort sort_name op operator_name module_expression show sub number param parameter_name a11 rules module_expression show view view_name Do not bother to memorise all of these for now or ever We illustrate them after module building constructs are explained cf Chapter 5 For the second half you have Syntax 15 show command for other inspection show tree term let_variable tree subterm tree
42. as primers The logical aspects of CafeOBJ are explained in detail in 2 and 3 This manual is for the initiated and we sometimes abandon the theoretical rigour for the sake of intuitiveness For a very brief introduction we just highlight a couple of features of CafeOBJ CafeOBJ is an offspring of the family of algebraic specification techniques A specification is a text usually of formal syntax It denotes an algebraic system constructed out of sorts or data types and sorted or typed operators The system is characterised by the axioms in the specification An axiom was traditionally a plain equation essentially algebraic but is now construed much more broadly For example CafeOBJ accommodates conditional equations directed transitions and limited use of disequality The underlying logic of CafeOBJ is as follows Order sorted logic 8 A sort may be a subset of another sort For example natural numbers may be embedded into rationals This embedding makes valid the assertion that 3 equals 6 2 It also realises operator inheritance in the sense that an operator declared on rationals are automatically declared on natural numbers Moreover the subsort relation offers you a simple way to define partial operations and exception handling Rewriting logic 12 In addition to equality which is subject to the law of symmetry you may use transition relations which are directed in one way only State transitions 1 S
43. bool test term sort membership cxu id if true then CXU else CYU fi CXU if false then CXU else CYU fi CYU CXU CYU coerce to bool term equational equal cxu cyu HXU b HYU coerce to bool term equational equal hxu hyu CXU CYU coerce to bool not term equational equal cxu cyu SIMPLE NAT gt 67 6 EVALUATING TERMS The righthand sides of the rules 17 and so on contain a strange symbol and the terms that follow suspiciously resemble Lisp s S expressions These are examples of system dependent definitions of operators If you are not confident enough about implementation issues do not touch these definitions Since the axioms of SIMPLE NAT are all equations the results of reduce and execute should be the same Indeed you have SIMPLE NAT gt execute 0 s 0 execute in SIMPLE NAT O s 0 s 0 NzNat 0 010 sec for parse 1 rewrites 0 000 sec 1 matches SIMPLE NAT gt execute s 0 0 execute in SIMPLE NAT s 0 0 s 0 NzNat 0 000 sec for parse 2 rewrites 0 000 sec 3 matches SIMPLE NAT gt The statistics may be suppressed by a switch SIMPLE NAT gt set stats off SIMPLE NAT gt reduce s 0 0 reduce in SIMPLE NAT s 0 0 s 0 NzNat SIMPLE NAT gt 1 stats is not an abbreviation 6 2 3 Equations and Transitions To see the difference between execute and reduce we switch to CHOICE NAT Section 5 2 1 68 6 2 Do the Evaluation
44. but that __ was idempotent 7 7 Further Example Propositional Calculus The next example is a decision procedure of propositional logic In this example rewriting modulo associativity and commutativity is decisive CafeOBJ has a built in module PROPC which is declared as follows 108 7 7 Further Example Propositional Calculus Cafe0BJ gt show PROPC sys module PROPC principal sort Prop imports protecting TRUTH signature Prop Identifier Bool lt Prop op _ and _ Prop Prop gt Prop assoc comm constr prec 55 r assoc op _ xor _ Prop Prop gt Prop assoc comm constr prec 57 r assoc op _ or _ Prop Prop gt Prop assoc comm prec 59 r assoc op not _ Prop gt Prop strat 0 1 prec 53 gt op _ gt _ Prop Prop gt Prop strat 0 1 2 prec 61 op _ lt gt _ Prop Prop gt Prop assoc prec 63 r assoc axioms var p Prop var q Prop var r Prop eq p and false false eq p and true p eq panddp p eq p xor false p eq p xor p false eq p and q xor r p and q xor p andr eq p or q p and q xor p xor q eq not p p xor true eq p gt q p and q xor p xor true eq p lt gt q p xor q xor true F Cafe0BJ gt 66 sys module is an introductory keyword for built in modules e An atomic proposition is an element of the built in sort Identifier declared in CHAOS IDENTIFIER or of the sort Bool declared in TR
45. c lt gt a gt b and a gt c true Bool 0 010 sec for parse 25 rewrites 0 050 sec 184 matches PROPC gt It is pleasing to see that the usual logical truths are proved to be true by just evaluating 111 7 OPERATOR ATTRIBUTES the corresponding terms Here the logical basis of the language is in stark relief If you think of rewrite rules as deduction rules a computation is a proof The set of rewrite rules is sound iff all the statements reducible to true are valid It is complete iff all the valid statements are reducible to true 7 8 Limitation of the Implementation As a cautious conclusion to operator attributes we must point to the major limitations of the current implementation As mentioned earlier the treatment of idempotency is inadequate The other two problems concern the enormity of extra rewrite rules You should have noticed that to realise rewriting modulo identity or associativity the system adds equations surreptitiously Consider first the case of identities Suppose in AZ OP in Section 7 6 there were another operator declaration op first S gt S and an equation eq first X S X S X A special case of the equation is eq first X X where X is bound to phi and the identity is cancelled The completion procedure for implementing identities does add this equation as well as eq first X phi which is a specialisation to the case when X is phi Thus we get a specification
46. chain M pr gt Mi ex gt M2 pr gt M M is imported via ex mode The mode with which M is imported is the weakest among all the chains along which M is imported 8 1 3 Qualifying Names In Section 3 3 2 we have shown how to qualify terms by sort names You can also qualify sort names and operator names this time by module names CafeOBJ allows you to use the same name for different sorts A typical case is to declare sorts in different but related modules variants of stack definitions for example are likely to have a common sort name Stack So long as they do not appear in the same context those sorts do not cause confusion The problem arises when you import two modules that contain sorts of the same name It is unlikely to import both modules directly but it is definitely possible to import them indirectly To avoid confusion you can qualify names as follows Syntaz 59 reference to sort operator parameters name module_name where the name is a sort name an operator name or a parameter name Section 8 2 1 According to the above syntactical rule the references that appeared so far such as Nat could be qualified such as Nat SIMPLE NAT A module name may be a parameter name Section 8 2 1 To avoid ambiguity if an operator name contains blanks or periods it must be parenthesised as _ _ M The referent of a qualified name is the one that is in the context of the qu
47. commas aq or a a or a a a etc a and are meta syntactical brackets treating a as one syntactic category a an optional a or a Nonterminal symbols appear in italic face Terminal symbols appear in the face like this terminal and may be surrounded by and for emphasis or to avoid confusion with meta characters used in the extended BNF We will refer terminal symbols other than self terminating characters see section as keywords in this document A 2 1 CafeOBJ Codes A CafeOBJ code is a sequence of modules views and evaluation commands spec module view eval 179 A SUMMARY OF CAFEOBJ SYNTAX A 2 2 Modules where a module is module module_type module_name parameters parameter parameter _name principal_sort module_elt import sort visible_sort hidden_sort sort_decl supersorts sort_name sort_symbol quali fier record super slot slot_ name slot_rename operator arity coarity op_attrs op_attr variable var_name axiom equation cequation transition ctransition label 180 1 il i 1i module_type module name parameters principal sort module elt P module module module ident parameter protecting extending including paramter_name module_expr ident principal sort sort_name import sort record operator variable axiom com
48. detail what happened at the second apply command This command applied eq X X 0 to the subterm 0 Without saying anything a variable X would be introduced This situation often occurs when a rule is reversely applied The substitution X a avoids that You can continue and prove another theorem that 0 is a right identity so the identity Since we already showed a a equals 0 it is sound to add the equation That leads to the command sequence eqa a 0 start a t 0 apply 2 with X a at 2 apply reduce at term which mirrors the reasoning at t O at t a ta O t a a 148 9 2 Applying Rewrite Rules 9 2 3 Choosing Subterms If a term has a complicated structure it is error prone to select a subterm at once To make safer selections a command is supported Syntar 77 choose command choose selection where a selection is as in apply Section 9 2 1 This command sets the focus to the chosen subterm and its successive application narrows the focus gradually show command with subterm argument may be used to print the current subterm in focus For example if you define a module of rings as module RING 4 R op 0 gt R op _ _ R R gt R assoc comm prec 35 gt op _ R gt R op _ _ R R gt R assoc prec 31 vars X YZ R eg O PAE eq X X 0 eq X Y Z X Y X Z eq Y Z X Yx X Z2 X and after opening RING you get 149 9 THEOREM P
49. distinguished as 4 1 and 4 2 With this preparation let us define in detail the relationship between operator names and their referents In CafeOBJ an operator name refers to a group of operators rather than a single operator Given a module M consider for example an operator declaration op f Nat Nat gt Nat in M and let G be the group this operator belongs to 1 Another operator with the same name i e f 2 and whose arity is in the same connected component as Nat Nat belongs to G 2 Yet another operator with the same name but with arity outside the connected com ponent belongs to G only if it is declared in M 3 No other operator belongs to G Here the connected component of Nat Nat is taken from the product graph The operator name f 2 in the context of M refers to the group G which may contain several distinct operators due to the above rules Accordingly the qualified name 2 M refers to G Intuitively qualification by M states that the name is declared in M Hence 2 precludes operators declared in other modules But what about 1 Consider for example the code 119 8 MODULE STRUCTURE module NAT Nat op _ _ Nat Nat gt Nat module INT protecting NAT Nat lt Int op _ _ Int Int gt Int and the reference _ _ INT It certainly refers to _ _ on Int but it should also refer to _ _ on Nat since CafeOBJ re
50. does not match the lefthand side as it is since the first argument is not true But by associativity the term equals true and false and true and this equivalent term does match the lefthand side Matching modulo associativity is a procedure to find a matching substitution under arbitrary arrangement of parentheses The built in equality operator _ _ Section 4 4 1 takes care of associativity For exam ple true and false and true true and false and true evaluates to true assoc makes sense only when the operator is binary with arity of the form A A and coarity C such that C lt A y Formerly CafeOBJ admitted the cases when the arity consists of different sorts T You are warned if the above stricter condition is violated The system assumes an operator with assoc attribute to be right associative Section 7 2 unless declared otherwise 96 7 1 Equational Theory Attribute 7 1 2 Commutativity The conjunction is also commutative In CafeOBJ it is written as op _and_ Bool Bool gt Bool assoc comm Commutativity may be specified with the equation eq X Bool and Y Bool Y and X which is fine as an equation As a rewrite rule however it is diabolically problematic since it generates infinite rewrite sequences For this reason commutativity should be stated by operator attribute Like assoc comm affects evaluation For example the term false and true does not match
51. equation declaration or 7 transition declaration In the subsequent chapters we shall introduce each of them in turn A general rule about module elements is that a referent must precede in the textual order For example you cannot refer to a variable unless you declared it somewhere above Another general rule is that a module element belongs to the module where it appears and unless imported Section 2 5 it cannot be referred to in other modules Different modules with the same name may be declared but only the latest declaration is maintained You cannot recover previous declarations The system gives a warning when a previous declaration is discarded Some modules are vital for the system to behave correctly Those modules cannot be overwritten There are other special modules not so vital but worth a diligent protection An example is a module that defines natural number arithmetic called NAT cf Chapter 11 You may remove the guard from those modules by the command Syntax 18 unprotect command unprotect module_name 13 2 MODULE DECLARATION For the reverse effect you may use Syntax 19 protect command protect module_name which make it impossible to overwrite the given module You may use this command to protect your own cherished modules The following session illustrates the behaviour of the system In this session we only use the syntax introduced so far CafeOBJ g
52. has a strong typing discipline Although useful for static analyses strong typing is sometimes too restrictive There are cases where type mismatch could never happen even though expressions are syntactically illegal Or rephrasing in the lexicon of TRS s apparently ill formed terms may reduce to well formed terms CafeOBJ appraises such phenomena to offer a reasonably strong typing discipline Consider a case when you try to apply an operator Oy sf gt to a term of sort T S and T differ so such an attempt should be rejected Unless that is the relation S lt T holds Note well that if TESIS holds f can definitely apply to terms of T That is an essence of order sorted logic What we are saying here is that if S is a subsort of T and a term t is of sort T f t may become by evaluation a well formed term since t may reduce to a term t of sort S 88 6 6 Flexible Typing and Error Handling One way to accommodate the above case is to use so called retract operators c f 9 CafeOBJ has adopted another approach Let us see how it works 6 6 1 Factorial of Rationals A usual definition of the factorial is as follows module FACT protecting RAT op _ Nat gt NzNat ca 0l 1 ceq N Nat Nx N 1 if N gt 0 where the factorial is declared as a postfix operator _ as is the convention RAT is a built in module of rationals You may point out that rationals are irrelev
53. i e the signature It is possible to list declarations in imported modules also For an example for example s sake Cafe0BJ gt module SHADOW NAT protecting SIMPLE NAT defining module SHADOW NAT _ done Cafe0BJ gt show sorts SHADOW NAT CafeOBJ gt show all sorts SHADOW NAT visible sorts Zero Zero lt Nat NzNat NzNat lt Nat Nat Zero NzNat lt Nat CafeOBJ gt 51 5 INSPECTING MODULES SHADOW NAT simply imported declarations of SIMPLE NAT and added nothing The plain sorts argument prints nothing while all sorts prints sort declarations in the imported SIMPLE NAT all does not print anything in the implicitly imported modules Even if you II 7 import BOOL explicitly the system still refuses to print the declarations in them In case of axioms instead of crying all to show command you may change a switch called all axioms as CafeOBJ gt set all axioms on If you are inspecting a particular module it is convient to set it as current Section 8 1 1 so that the module name may be omitted Cafe0BJ gt select SIMPLE NAT SIMPLE NAT gt show sorts visible sorts Zero Zero lt Nat NzNat NzNat lt Nat Nat Zero NzNat lt Nat SIMPLE NAT gt show ops O OE CO aaa poe oca rank gt Zero O A E C A E T EE rank Nat gt NzNat atinada O E rank Nat Nat gt Nat attributes 1 strat 1 0 2 gt axioms eq 0 N N eq s N N s N N SIMPLE
54. is another common module level operation The com bined whole is called module sum Syntax 68 module sum module_expression module_expression module_expression x A module represented by a module sum consists of all the module elements in the summands If submodules are imported more than once it is assumed to be imported once and is shared throughout Section 8 1 2 This construction is sometimes called amalgamated sum or shared sum From this definition it follows that 138 8 4 Module Expression module A protecting B C is equivalent to module A protecting B protecting C 8 4 4 Making Modules Module expressions are often used in isolation To create a module it is often the case that you simply import a module represented by an expression as module LOVE protecting oo where is a module expression The purpose of this declaration is to give a name to a module defined by the expression C est tout In such a case an abbreviation is handy Syntar 69 make command make module_name module_expression make evaluates the module expression and confer the resulting module with the given name In fact this is a shorthand of the protecting importation as above You may want to try this Cafe0BJ gt make LOVE SIMPLE NAT defining module LOVE _ done CafeOBJ gt show LOVE module LOVE imports protecting SI
55. like in 1 and 1 options By default if an apparent single file name is given as argument to input command the system searches the current directory then standard library directories The standard library directories are fixed at the time of installation By default of defaults they are usr local cafeobj 1 4 1ib usr local cafeobj 1 4 exs which are searched in this order If the search paths are modified the sytem searches a the current directory b the paths given by the user from left to right and c the above default paths in case of or 1 options The current directory has a privileged status It is always searched first and II E cannot be suppressed by 1 options or set command To inspect the current search paths type Cafe0BJ gt show switch libpath see Section 1 3 3 for show command in general 1 2 6 Requiring and Providing If you are familiar with emacs you may fancy the following pair of commands for configu ration management Syntax 9 require command require feature pathname Syntax 10 provide command provide feature require requires a feature which usually denotes a set of module definitions Given this command the system searches for a file named the feature and read the file if found If a pathname is given the system searches for a file named the pathname instead provide discharges a feature requirement once provided all the subse
56. pop push s 0 empty top empty Nat 0 010 sec for parse 1 rewrites 0 000 sec 1 matches STACK OF NAT gt 6 6 3 Handling Errors as Errors The above definition of natural number stacks does not say much about what to do with errors It simply demarcates the error boundary If you want to be more specific about handling errors a standard way is to declare specific error elements constants and equalise errors to them In case of the stacks the code would look something like op gt Nat op gt Stack eq top empty eq pop empty where is meant to be a bottom element A more elaborate way is to declare such constants as op zero divisor gt Nat op top of empty stack gt Nat They are intended to be error messages An error sort is automatically declared for each connected component of the sort graph and has an internal name that starts with In the examples of factorials and stacks the names derived from single sorts as Rat and Nat In general an error sort may have a complicated name like SortA SortB SortC The summands of this name are maximal sorts in a relevant connected component In making explicit references you may use a more compact notation just put a question mark before a sort name in connected components For example if you declared LA lt B A lt the error sort name is internally B C but may be referred to as either A B or C 92 6 6 Flexible Ty
57. s s s s s s s s s s s 0 NzNat 0 010 sec for parse 118 rewrites 0 020 sec 226 matches MULT gt Compilation is done only once when tram command is first used on the given module You may just compile a module as a preparation by Syntar 54 tram command for compilation tram compile exec module_expression u If the module expression is omitted the current module is assumed If exec is given transitions as well as equations are compiled i e for exec For this command e al1 and a are all synonymous to exec 84 6 5 Context Variable reduce and execute use different sets of rules Therefore if you have compiled a module already for reduce and try tram with execute option the system recompile the module Do not forget the last period preceded by a blank Compilation into and execution of abstract machines are taken care of by an indepent program called tram or brute So you have to tell the system where it is The command Cafe0BJ gt set tram path home irene bin tram directs the system to the given path for this program The default is usr local bin tram tram and brute have quite different architectures and they both have limitations For detail see README in the distribution package There is another switch related to tram although you may never use it The command Cafe0BJ gt set tram
58. s s s s s s s s s s 0 NzNat 0 000 sec for parse 145 rewrites 0 010 sec 277 matches MULT gt show term al s 0 s s 0 s s s 0 Nat MULT gt A context variable once bound may be used as a subterm in commands reduce parse let itself etc Note that let binds syntactically reduce commands above did not change the values of a1 or a2 show command was used to print the binding of a1 To list all the bindings use show command again MULT gt show let bindings a2 s s s 0 s 0 s s 0 s s s 0 s s s s s 0 al s 0 s s 0 s s s 0 MULT gt let in the above command may be replaced by binding Context variables are local to each context Continuing the above session 86 6 5 Context Variable MULT gt select SIMPLE NAT SIMPLE NAT gt let al 0 setting let variable ai to O Zero SIMPLE NAT gt show let bindings al 0 SIMPLE NAT gt select MULT MULT gt show let bindings a2 s s s 0 s 0 s s 0 s s s 0 s s s s s 0 al s 0 s s 0 s s s 0 MULT gt As shown above context variables in MULT and SIMPLE NAT are kept separately and the same name may be used for different bindings As explained context variables belong to individual modules Tf you attempt to bind a context variable without setting a current m
59. signatures Modules contain axioms as well and specification morphisms are defined to preserve axioms As an exam ple consider MONOID Section 5 2 3 and SIMPLE NAT Section 2 2 If SIMPLE NAT indeed specifies natural number addition it is associative and has identity 0 hence constitutes a monoidal structure This fact can be confirmed by 1 Specifying a mapping of sorts and operators that is a signature morphism and 2 Showing that under that mapping the translated axioms of MONOID hold in SIMPLE NAT A specification morphism is a signature morphism that satisfies such conditions as 2 above A precise definition would require the precise notion of satisfaction which is beyond this 123 8 MODULE STRUCTURE exposition note that you have to consider transition relations and behavioural equivalence in addition to equality In its place and for intuitive illustration we shall elaborate on the above monoid example after introducing concrete language constructs 8 2 3 View A view specifies ways to bind actual parameters to formal parameters Given a parameter i e a module T and a module M a view V from T to M is a specification morphism from T to M the derived specification of M with one modification the operator mapping must be surjective only for non derived behavioural operators i e those originally in M To spell out the definitions of the previous section therefore a view is a pair of structure preser
60. sort T but re declared on the fly as of sort S Remember that overwriting variable declarations terra firma are illegal Section 4 1 On the fly declarations are not subject to this prohibition Moreover on the fly declarations may themselves be overwritten The following example uses X first as of sort S then as of T module S CS opi S T gt T eq X S X T X 40 4 2 Equation Declaration In spite of the above remark it is advisable not to overwrite on the fly s by II on the fly s It would easily lead to confusion Accordingly the system gives a warning when it encounters such cases 4 2 2 Conditional Equation Declaration An equation may be conditional A conditional equation is of the form Syntar 46 conditional equation declaration ceq label term term if boolean_term u Labels and terms are as in eq As stated often enough the last blank period lets the system know the end of a term and is a must Note that a declaration starts with ceq not eq ceq may be abbreviated to cq Like the last period and if demarcate terms You should put blanks around them In former versions conditions were preceded by if not if A boolean term is a term of sort Bool which is declared in a built in module called BOOL to be more precise in a built in module imported by BOOL A conditional equation states that the two terms are equal if the boolean term is true i e i
61. that in order sorted rewriting an application of a rewrite rule may introduce an ill formed term For a contrived example module NONCOMPAT fs lt 8 J opak gt S5 op b gt 5 opf S gt S eqa b is not compatible since f a which is well formed rewrites to f b which is ill formed As this example shows non compatibility is caused by a rewrite rule that raise s the sort of aterm This is not a necessary condition of compatibility however In the absence of the operator f the above module is compatible The system checks a necessary and sufficient condition of compatibility as Cafe0BJ gt check compatibility NONCOMPAT gt gt started compatibility check gt gt module corresponding TRS is NOT compatible rewrite rule a b violates the compatibility and following operator s can possibly be affected eS gt Cafe0BJ gt module COMPAT Le lt 8 J opa ES opb b gt SY eqa b I defining module COMPAT _ done Cafe0BJ gt check compatibility COMPAT gt gt started compatibility check gt gt module is compatible Cafe0BJ gt 162 10 1 Check Command I As shown in Section 6 6 the current implementation regards a term like f b above as well formed although of a questionable sort The above definition should be rephrased in this setting in terms of error sorts Laziness If the first argument is laziness the system checks if the given operator can be evaluated lazil
62. that realise or surrogate these relations CafeOBJ provides four predicates for this purpose e for equality e gt for transition relations e b for behavioural equivalence The latter three are mainly used in theorem proving cf Section 10 2 ey ia In addition the system supports a sort predicate is 4 4 1 Equality Predicate 19 k The predicate for ordinary equality written is a binary operator defined on each visible sort An explicit declaration of the operator would be of the form op _ _ S S gt Bool or 43 4 AXIOMS pred T SS for each sort S _ _ is defined in terms of evaluation Chapter 6 For ground terms t t of sort S t t equals true iff t t evaluate to a common term It takes care of equational theories such as associativity Section 7 1 Due to this definition _ _ works correctly only if the term rewriting system is terminating and confluent Section 6 1 2 The converse of _ _ returns false on the same arguments is _ _ which returns true iff _ The exact mechanism for defining these operators is tricky but all are declared and de fined in a built in module BOOL This module contains usual boolean operators such as conjunction and as mentioned earlier is implicitly imported by other modules Section 2 5 Note the difference between equations such as eqN 0 N and applications of th
63. the lefthand side of eq X Bool and false false but an equivalent term true and false does _ _ takes care of commutativity as well as associativity so true and false and true true and true and false evaluates to true comm makes sense only when the operator is binary and its arity sorts are the same Formerly CafeOBJ admitted the cases when the arity sorts have a common i supersort 7 1 3 Identity 66 _and_ has true as left and right identity which is written in CafeOBJ as op _and_ Bool Bool gt Bool assoc comm id true The attribute id true is equivalent to the following equations XER eq X Bool and true X eq true and X Bool In fact since comm is also given one of the above is enough Identity attributes affect evaluation Under the above operator declaration false and true is without evaluation identified with false id makes sense only when the operator is binary the arity sorts and the coarity sort are the same and the identity term belongs to that sort 97 7 OPERATOR ATTRIBUTES Formerly CafeOBJadmitted the cases when the coarity sort is different The current implementation of CafeOBJ applies a completion procedure to realise matching modulo identity The procedure often generates a great many of equations leading to severe performace degeneration or even to non termination To prohibit unwanted completion use idr ins
64. the same two elements a more re stricted structure essentially partial orders and monotonic functions serves as well 58 5 2 Some Typical Modules CafeOBJ gt module CHOICE NAT 4 extending SIMPLE NAT op _l_ Nat Nat gt Nat vars N N Nat trans N N trans N N gt N defining module CHOICE NAT _ _ done CafeOBJ gt select CHOICE NAT CHOICE NAT gt show axioms Equations ceq cvi Nat cv2 Nat gt cv3 Nat cv4 Nat true if cvi Nat gt cv3 Nat and cv2 Nat gt cv4 Nat ceq s cv1 Nat gt s cv2 Nat true if cvl Nat gt cv2 Nat ceq cvi Nat cv2 Nat gt cv3 Nat cv4 Nat true if cvi Nat gt cv3 Nat and cv2 Nat gt cv4 Nat eq N N gt N true eq N N gt N true Rules trans N N gt N trans N N gt N CHOICE NAT gt show subs extending SIMPLE NAT protecting RWL CHOICE NAT gt As shown above congruence axioms are added and a module called RWL is imported auto oe matically RWL is the module that declares _ By the way where is the reflexivity axiom Well it is hidden in the module JI RWL The current implementation provides a universal reflexivity axiom and each module does not acquire a new axiom But you should think as if it did 5 2 3 Non isomorphic Models There are cases when your favourite models are not unique Examples abound in defining algebraic structures Monoids may be defined
65. the switch is on every time a module is redefined every context surrounding it is forced to reflect the change at once If you are so inclined you may change the prompt once and for all Cafe0BJ gt prompt Haskell gt Haskell gt In the reset of the session the prompt would not change until you invoke the command 1 again 8 1 2 Module Sharing It is possible that some modules are imported several times For example the declarations module MO module MOO protecting MO module M01 protecting MO module M001 protecting M00 protecting M01 makes M001 import MO twice The basic convention is that in such cases MO is regarded as imported only once and its single copy is shared throughout This convention works fine when a module is imported with protecting mode since a module then has essentially the same models everywhere The problem arises when extending or using modes appear somewhere In general importation modes are determined as follows Let us write M m gt M if M directly imports M with importation mode m When M directly or indirectly imports M there are several chains M mi gt Mil m2 gt 22 m Ma Mh lFor an obvious reason the above change does not force the system to accept Haskell 117 8 MODULE STRUCTURE to M Each such chain determines the mode with which M imports M as the weakest among all the mi s For example in the
66. up to iso model tight denotation In the other it denotes a class of models loose denotation The latter is the case when a module is used as parameter see Section 8 2 1 when it defines behavioural properties Section 5 2 4 and so on We do not go into the detail in this manual but the distinction is very important You should consult 3 or other technical materials at least once Sometimes it is necessary or convenient to restrict the r le of a module Alternative module declarations below allow you to do that Syntax 23 module for tight denotation module module_name module_element x yy Syntax 24 module for loose denotation module module_name module_element yy The syntax inside is the same as declarations that start with module 16 2 4 Comment When a module is declared with module it always denotes a unique model When declared with module it always denotes a class of models 2 4 Comment A comment of CafeOBJ is one of the followings a From to the end of line eol b From gt to the eol c From to the eol d From gt to the eol Comments may be inserted either between module declarations or between module elements A comment that starts with gt or gt is displayed when it is input to the system This facility is useful when a file is being read or when you want to state the ex
67. used to avoid name conflicts CafeOBJ does not allow slots of the same name to be inherited twice If there is no conflict slot mappings may be omitted An example of inheritance using Date of the previous section is record Time Date 4 hour Nat minute Nat This code declares Time to have slots year month and day as well as hour and minute Access functions year set year and so on are applicable to terms of Time exactly as they are to those of Date The effects of the declaration are equivalent to 35 3 SIGNATURE record Time year Nat month Nat day Nat hour Nat minute Nat Here is another example which needs slot renaming record Week 4 day Nat record Time Date day gt day of the month Week day gt day of the week ct hour Nat minute Nat Since day was the slot name of both Date and Week each slot was accorded a more accurate distinct name 36 Axioms CafeOBJ inherits the essences of algebraic specification techniques where axioms are given as equations Several extensions however lead to the following complications 1 Equa tions may be conditional 2 Not only equations but transitions are available 3 Visible sorts and hidden sorts demand different kinds of equivalences so that as well as ordinary equations behavioural equations are available All of these extensions are orthogonal as witnessed by 8 2 syntatical constructs 4 1
68. where phi first a a first a b phi holds This result is somewhat unexpected As a TRS the two equations annihilate the Church Rosser property A different problem arises if you modify the declaration of xor in PROPC Section 7 7 as op _xor_ Prop Prop gt Prop assoc comm id false i e adding the identity attribute Then in the presence of the equation eq p and q xor r p and q xor p andr the completion procedure adds eq p and r p and false xor p and r 112 7 8 Limitation of the Implementation which is a special case where q is replaced by false This equation is hazardous since you now get an infinite rewrite sequence a and b gt a and false xor a and b gt a and false xor a and false xor a and b gt Even if such a hazard is avoided performance may be compromised by hundreds of extra unwanted equations If you encounter misbehaviours then id is a possible suspect If it is the culprit change to idr which does not force completion As to associativity a fateful combination with sort ordering may generate dozens of unnec essary equations For example in the built in module INT Nat is a subsort of Int and the addition _ _ is declared on both sorts As a consequence an equation eq0 I 1 induces an extra equation eq 0 I aclE aclE l This equation has a lefthand side that is costly to match yet adds nothing to the power of evaluation
69. 0 010 sec 12 matches MULT gt The pattern restriction forced the reduction to terminate As shown above show command with stop argument prints the specified pattern You should use this command instead of p the latter is recognised only within the stepper It is not possible to specify more than one patterns or more complicated pat terns using e g regular expressions If demands are strong the future versions may enhance the pattern description facility 6 3 4 Controlled Reduction by Number of Steps It is possible to control reductions by limiting rewrite steps Enter the stepper again 82 MULT gt set step on MULT gt set stop pattern MULT gt reduce s s 0 s s s 0 reduce in MULT s s 0 s s s 0 gt gt stepper term s s 0 s s s 0 STEP 1 rwt 10 STEP 1 c gt gt aborting rewrite due to rewrite count limit 10 lt lt s s s s s s 0 s s s 0 NzNat 0 000 sec for parse 10 rewrites 0 020 sec 18 matches MULT gt 6 4 Faster Evaluation rwt command in the stepper forced the reduction to abort after 10 rewrite steps Note that unlike g command the system aborted the reduction not just suspended it It is possible to limit rewrite steps outside the stepper MULT gt set step off MULT gt set rwt limit 5 MULT gt reduce s s 0 s s s 0 reduce in MULT s s 0 s s s 0 gt gt aborting rewrite due to rewrite count limit 5
70. 1 or 1 which belongs to both NonPos and Nat Thus a general solution requires a complete equational calculus which is beyond the power of CafeOBJ It is for this reason that the system always bets on the safer side even if the results are dull the system and you will not lose a penny since the modified module has exactly the same model s as before when you take reducts If one of NonPos or Nat were empty the system would have done nothing For example if you delete the declaration op 1 gt Nat from INTB Nat is not inhabited any more the system adds nothing this time For those who only want to be warned of the danger it is also possible just to check if the signature is regular cf Section 10 1 3 3 2 Parsing Terms As suggested above a symbol sequence may be parsed in more than one ways A salient example is a constant symbol With the two declarations below empty is a term both of Stack and Set op empty gt Stack op empty gt Set 29 3 SIGNATURE In such cases you have to supply additional information by qualification Other ambiguities may be eliminated by parentheses Let us see a couple of examples To see whether a term is unambiguous the following command is handy Syntax 35 parsing command parse in module_expression term on If in option is omitted the current module cf Section 8 1 1 is assumed Module ex pressions are explained in Section
71. 4 4 Internalising Axioms Note that if is not turned out to be congruent no axiom defines In such a case is not even reflexive pl Another predicate for behavioural equivalence is b which is to behavioural equations 4 as is to plain ones and is defined to true iff both hand sides evaluate to a common 119 term The difference between and b is in the applicability of behavioural axioms See 6 2 1 for detail 4 4 4 Sort Predicate The system supplies a predicate that checks whether a given term is of a given sort It is of the form t is S and evaluates to true if t belongs to S You can supply explicit axioms for the predicate An example is vars N N Nat ceq N N is NzNat true if N is NzNat ceq N N is NzNat true if N is NzNat This feature is introduced as a surrogate of membership relation We stress that it is a surrogate not a real thing You should not use this feature unless absolutely necessary There are switches such as mel sort related to this predicate They are also highly tentative and you should not use them unless absolutely necessary 47 Inspecting Modules It is time we show some examples that combine all of the declarations explained so far This chapter also illustrates the module inspection command show Section 1 3 3 5 1 Using Inspection Commands 5 1 1 Printing Whole Modules W
72. 8 4 It is enough here to know that a module name is a module expression Do not forget the last period preceded by a blank This is the only way for the system to detect the end of a term usual parsing techniques would not do due T to flexible term constructs The same convention is used in other commands and declarations To see how this command works here is an example where an ambigouous term is parsed module SIMPLE INT protecting SIMPLE NAT Nat NegInt lt Int op _ NzNat gt NegInt op _ _ Int Int gt Int op _ _ Int Int gt Int op s Int gt Int vars M M Int The above module gives a signature for integer operations SIMPLE NAT was in Section 2 2 vars declares variables Section 4 1 After declaring the above module you may get a session like Cafe0BJ gt parse in SIMPLE INT M M s 0 Warning Ambiguous term please try check regularity command if the signature is regular there possibly be some name conflicts between operators and variables Lal 2 Tat Ming gt hay M Int M Int s 0 2 Tat Ming gt bay M Int M Int s 0 Error no successfull parse ambiguous term SyntaxErr If you set a switch verbose to on you see a more visible tree structure of possible parses like 30 3 3 Terms Cafe0BJ gt set verbose on Cafe0BJ gt parse in SIMPLE INT M M s 0 Warn
73. AM gt reduce tl s 0 zeros reduce in NAT STREAM t1 s 0 zeros tl s 0 zeros Stream 0 000 sec for parse 0 rewrites 0 000 sec O matches NAT STREAM gt Compare the above result to the case when breduce is invoked instead Since this com mand is to get an behaviourally equivalent term the system applies behavioural equations indiscriminately as NAT STREAM gt breduce tl s 0 zeros behavioural reduce in NAT STREAM tl s 0 zeros zeros Stream 0 000 sec for parse 1 rewrites 0 000 sec 1 matches NAT STREAM gt 70 6 2 Do the Evaluation 6 2 5 Evaluation Traces We continue the session of the previous section The statistics contained the number of rewrites and match attempts Reduction of O s 0 and s 0 0 in Section 6 2 2 amounts to computing 0 1 and 1 0 respectively and the statistics showed that the efforts of computation were greater with 1 0 You probably know why To confirm your reasoning try trace switches CHOICE NAT gt select SIMPLE NAT SIMPLE NAT gt set trace whole on SIMPLE NAT gt reduce 0 s 0 reduce in SIMPLE NAT 0 s 0 1 0 s 0 gt s 0 s 0 NzNat 0 000 sec for parse 1 rewrites 0 000 sec 1 matches SIMPLE NAT gt reduce s 0 0 reduce in SIMPLE NAT s 0 0 1 s 0 0 gt s 0 0 2 s 0 0 gt s 0 s 0 NzNat 0 000 sec for parse 2 rewrites 0 010 sec 3 matches SIMPLE NAT gt The system printed the r
74. CafeOBJ User s Manual ver 1 4 8 Draft Ataru T Nakagawa Toshimi Sawada Kokichi Futatsugi NOTE This manual is out of date and is subject to change Changes from Version 1 3 The main changes from version 1 3 are as follows In addition to Gnu Common Lisp CMU Common Lisp and Allegro Common Lisp can be used as a platform Faster rewrite engines are now available and can be invoked from CafeOBJ The predicate gt for transition relations gets a more powerful support A couple of new switches are added for this reason Behavioural axioms can be used in equational reduction and an operator attribute coherent is added for this purpose A behavioural reduction command is introduced Sort predicates are introduced Contents Contents ii Introduction vii Legende o e e bee kh Vek Se a ee ge a ee ee e a viii 1 Dialogue with the System 1 11 Hello Go dby so eae enma a ia aaa a 1 1 01 SEM or rc Se e a ed 1 11 2 Quitting the System so secarse eras a 3 1 1 3 Emergency Resumption and Bug Reports 3 1 2 Piles and Libraries o cocoa a wee A Re 4 1 2 1 Heading Files oo naa ae RE Eee ed a E a a 4 1 2 2 Saving and Restoring 5 123 Initialisations and Options gt as o e so sese ca aws wewu 6 1 2 4 Bawi CREES 03 baw shew ai de a nee gad O 7 1 235 Module Libraries cocoa sacosa toe eu a awe 1 2 6 Requiring and Providing 5 es er ied e sas ds 8 1 3 Some
75. E 103 7 4 4 Interpreting E Strategies o 104 feo a kk ADA eR Ba ee EE ee PAG A Ae ee 104 7 5 1 2 o A a Swe Re ee EE ER 105 7 6 Operator Attributes and Evaluations aooo a 105 7 7 Further Example Propositional Calculus 108 7 8 Limitation of the Implementation 112 8 Module Structure 115 8 1 Names and Contexts 666 coro nio bace ee ee es 115 3 1 1 Context and Current Module o 115 8 1 2 Module Sharing os occiso A 117 S15 malla Names coa ee ee We ee A da Hes 118 8 1 4 Referring to Operators a oc sew ra moe rorta aa a 118 8 2 Parameters and Views h oaoa ea a 120 8 2 1 Parameterised Module 00 2 000 ee 120 8 2 2 Preview Not Preview 121 8 2 3 TI e a d ane a ai a aA a a e e E a e i g ae SRE 124 8 2 4 Wiewe GADE 5 ck he a ee id e e a 125 8 2 5 Wot Quite a VEW oa as be alee da hoi 127 CONTENTS 8 3 8 4 9 1 9 2 9 3 10 1 10 2 8 2 6 Pitch VIEWS o e s sacro ee kA Binding Parameters o oo os caoba a oee de E e a a a Se es 8 3 1 Instantiation of Parameterised Modules 8 3 2 Parameters as Imports 8 3 3 Parameter Passing ee ess 8 3 4 Parameters with Parameters 200 8 3 5 Qualifying Parameter Names 004 Module Expression ee ee 8 4 1 Module Name i si ramea caged a a a 8 4 2 Renaming a k a ee ee 8 4 3
76. Helpful Commands lt s eacad we e deae a e ea 9 1 3 1 Help Command and Top level Commands 9 1 3 2 Switch Togpling Command 2 606 kasga cso sad ddoi 10 1 53 Inspection Commands lt lt weds erdd e a a n 11 2 Module Declaration 13 2l Overall SETE coda GA SRA a PE a A 13 2 2 Blocks ima Module ca c ca epora a a e Ree ee e 14 2 3 Tight Modules Loose Modules o 16 2 4 COMETE on Dee ha baa a eae e de de beet A e a 17 25 Llimport Declaration lt lt sa coe ea ge be See eee A 18 3 Signature 21 ae Sort Declaration so coccia EN 21 SLI Bort Declaration 22 cansi iee Re e e ee PA Se ia 21 do Loa Subsort Declaration cosa A ea ee 22 CONTENTS 6 2 5 Evaluation Traces 3 2 Operator Declaration co oro ae ee RE RAD eR Dal Operator Declaration oo ewe ee es haa Behavioural Operator Declaration 3 2 Predicate Declaration oa s oco 2 446 444 ba vee edad 3 3 TOE poe ok ge OR ea ee e le es we eS dl Well formed Terms o a 3 0 2 Parsing Fernie 2 aa ane e e dd Qualilying Tera osos a a A A 3 4 Record Declaration esaa 5 ocre rosas ses 3 4 1 Plain Record Declarabi ti o ccc ke cea o 3 4 2 Inheriting Records sa ca s a caci ero a a EG a 4 Axioms 4 1 Variable Declaration 2 4 4 4 once a ee ee 4 2 Equation Declaration o lt o spro 252k be eee ee ee a 4 2 1 Unconditional Equation Declaration 4 2 2 Conditional Equation Declaration
77. ICE NAT gt reduce a b gt c reduce in a b gt c true Bool 0 000 sec for parse 6 rewrites 0 000 sec 13 matches CHOICE NAT gt close Cafe0BJ gt 166 10 2 Theorem Proving Techniques For another simple example suppose you want to prove another simple fact that If t transits to u t transits to u t for any t Cafe0BJ gt open CHOICE NAT opening module CHOICE NAT done CHOICE NAT gt ops abc gt Nat CHOICE NAT gt trans a gt c CHOICE NAT gt reduce a b gt c b reduce in a b gt c b true Bool 0 000 sec for parse 4 rewrites 0 000 sec 15 matches CHOICE NAT gt close Cafe0BJ gt Note that when using _ gt _ evaluation should be by reduce command not by execute cpmmand Although _ gt _ represents transition relations the reasoning is within pure equational logic e There are a couple of switches that control the reduction procedure for _ gt _ One is to get a trace For illustration you may rerun the first above session 167 10 PROVING MODULE PROPERTIES declaring a b c and assert a gt c as before CHOICE NAT gt set exec trace on CHOICE NAT gt reduce a b gt c reduce in a b gt c transition step 1 1 O a b 1 gt a O a b 1 gt b CERCA AD 1 gt c b transition step 2 1 x x x x x x O a 2 gt c t
78. MPLE NAT y Cafe0BJ gt 139 Theorem Proving Tools The TRS engine Chapter 6 may be used as a lightweight theorem prover In addition the current version of the system supports a couple of commands that act as theorem proving tools 9 1 Open Closing Modules There are commands to modify module declarations To start modifying a module use the command Syntax 70 open command open module_name This command enables you to declare new sorts operators equations and so on Just type declarations after this command You cannot however change or delete the existing declarations To finish the modification use the command Syntaz 71 close command close 9 1 1 Why Opening Modules The effects of declarations supplied in between open and close commands are temporary e An open command creates a new module This module contains a copy of declarations in the given module e Until the module is closed all the declared sorts equations etc are added to the new module e close expunges the new module So close makes all your efforts banish What is the sense of it all Well this open closing mechanism is an ecological tool to 1 make hypotheses 2 prove by evaluation your 141 9 THEOREM PROVING TOOLS favourite theorems upon the hypotheses 3 finish the proof and delete the hypotheses 17 start again with new hypotheses For example consider the familiar module SIM
79. Nat lt 0 false N Nat gt 0 0 lt 0 gt false rule eq not false true 2 lt 6 1 gt 7 1 lt 7 not false gt true match success 2 gcd s s 0 s s 0 gt ged s s 0 s s 0 s s 0 Note the appearances of 2 gt The number indicates the depth of recursion evaluating conditions may lead to recursively evaluating conditions and so on and on Most of the out put should be self explanatory The above trace shows two conditional rules were checked first unsuccessfully and second successfully 79 6 EVALUATING TERMS 6 3 Stepper By taking traces you may inspect in detail how reductions proceed and modify axioms if they are not going as expected The set of commands introduced in this section is for controlling reductions in more detail and help you debug modules 6 3 1 Step Mode You may enter into leave the step mode by a switch Cafe0BJ gt set step on In this mode evaluation commands apply rewrite rules step by step We first define multi plication module MULT 4 protecting SIMPLE NAT op _ _ Nat Nat gt Nat vars NM Nat eqO0 N 0 eq s N M M N M After feeding SIMPLE NAT and MULT you may get the following session Cafe0BJ gt select MULT MULT gt set step on MULT gt reduce s s 0 s s s 0 reduce in MULT s s 0 s s s 0 gt gt stepper term s s 0 s s s 0 STEP 1 The new prompt indicates you are in the step mode
80. OID from MONOID to SIMPLE NAT sort M gt Nat op e gt 0 op 2 e SP y This mapping is certainly a signature morphism since by replacing M with Nat the ranks of e and _ _ match 0 and _ _ respectively And we can show that for variables X Y and Z of sort Nat the equations 125 8 MODULE STRUCTURE ea Oe ss WO ZS Ma 0 lt 22 eqO X X eqX O X hold under the theory of SIMPLE NAT but this requires a non trivial proof we shall come to this later Now consider another monoid natural numbers under multiplication view NAT AS MONOID from MONOID to MULT 4 sort M gt Nat op e gt s 0 op gt MULT was in Section 6 3 1 Here Mis mapped to the same sort Nat as before but the operators are mapped differently Note first that _ _ refers to two distinct operators over M and Nat Further note that the constant e is mapped to s 0 which is not a constant declared in MULT It is a derived operator and this view shows why a view is defined to be a mapping to the derived specification To show that NAT AS MONOID defines a specification morphism we need to prove eq X Y Z X Y Z eq s 0 X X eq X s 0 X Note finally that we may as well replace SIMPLE NAT by MULT as the target of NAT AS MONOID since MULT imports every declaration of SIMPLE NAT This fact confirms the observation that there can be more than one views between two modules We now turn to som
81. OP gt select ACZ OP ACZ OP gt reduce phi a phi b phic reduce in ACZ OP phi a phi b phi c 1 gt 1 rule eq ident14 phi X ID S X ID S X ID S gt a b phi phi c 1 lt 1 phi a phi b phi c gt a b phi phi c 1 gt 2 rule eq ident14 phi X ID S X ID S X ID S gt ab phi c 1 lt 2 a b phi phi c gt ab phic 1 gt 3 rule eq ident14 phi X ID S X ID S X ID S gt abc 1 lt 3 a b phi c gt ab c DECEO 0 010 sec for parse 3 rewrites 0 010 sec 5 matches ACZ 0P gt Again phi s were eliminated but different rewrite rules were used and relying on commu tativity the system changed the order of listing at the first step Adding idempotency we get 107 7 OPERATOR ATTRIBUTES ACI OP gt module ACIZ OP LS ops a b c phi gt S op __ S S gt S assoc comm idem id phi defining module ACIZ _ _ done ACI OP gt reduce in ACIZ OP phi a phi b phic reduce in ACIZ OP phi a phi b phi c 1 gt 1 rule eq AC U idem S U idem S AC U idem S AC gt phi a b c U idem S gt phi 1 lt 1 phi a phi b phi c gt phi abc 1 gt 2 rule eq ident16 phi X ID S X ID S X ID S gt abc 1 lt 2 phi a b c gt ab c anb 6 NS 0 000 sec for parse 2 rewrites 0 000 sec 9 matches ACI OP gt phi s were stripped but the reason for the first step when two phi s were eliminated at once was not that phi was the identity
82. PLE NAT reprinted here module SIMPLE NAT Zero NzNat lt Nat op 0 gt Zero op s Nat gt NzNat op _ _ Nat Nat gt Nat vars N N Nat eqO N N eq s N N s N N Suppose you want to show that 0 is a right identity of _ _ also Using the standard structural induction you can prove it easily by showing 1 0 0 equals 0 and 2 for any M if M 0 equals M s M 0 equals s M A score of this proof may be written using open command as open SIMPLE NAT op a gt Nat eqat0 a reduce 0 0 reduce s a 0 close When a module is opened the system changes the prompt beginning with as Cafe0BJ gt open SIMPLE NAT opening module SIMPLE NAT done SIMPLE NAT gt After opening module elements and various commands can be input The above score adds a new constant a to represent any natural number and an equation for induction hypothesis and invlokes reduction commands base case and induction step The system evaluates 0 0 and s a 0 as usual and returns the results 0 and s a 142 9 1 Open Closing Modules SIMPLE NAT gt op a gt Nat SIMPLE NAT gt eqat tO a SIMPLE NAT gt reduce 0 0 reduce in 0 0 O Zero 0 000 sec for parse 1 rewrites 0 000 sec 2 matches SSIMPLE NAT gt reduce s a 0 reduce in s a 0 s a NzNat 0 000 sec for parse 2 rewrites 0 000 sec 4 matches
83. R subterm f 0 0 R bindings empty selections Ty Wek ee RI All CB SI 2 o pending actions none stop pattern not specified RING gt 9 2 4 Identifying Rewrite Rules We have not shown how to obtain the number that designates a specific rewrite rule Re turning to GROUP you may print rewrite rules or axioms so regarded as follows 151 9 THEOREM PROVING TOOLS Cafe0BJ gt open GROUP opening module GROUP_ done GROUP gt show rules rewrite rules in module GROUP 1 eqo0 X X 2 eq XK xXK 0 GROUP gt Rules of any module may be printed by supplying an extra argument GROUP gt show rules RING rewrite rules in module RING 1 eqO X X 2 eq XK xXK 0 3 eqX Y Z X Y X Z 4 eq Y Z X Y X Z2 X GROUP gt It is also possible to print all the rules including those declared in imported modules by specifying all as in GROUP gt show all rules The numbering of the above is used to specify rewrite rules For example you encountered in Section 9 2 2 a command GROUP gt apply 1 at 1 The specified rule according to the output above was 1 eq0 X X and the minus sign was added to apply this rule in reverse You may decorate a rule number with a module name like GROUP gt apply GROUP 1 at 1 which will apply the same rule as before Axiom labels may also be used to designate rules For example if the above equation
84. ROVING TOOLS ZRING gt op f_ R gt R RING gt start f f 0 f f 0 f f f f 0 Ce EFEFEF Er CG fa 2 C a O af 2 amp G OD o RING gt choose 2 RING gt show subterm EA Cf Cf 0 CCE Cf 0 CCE 0 CCE Cf 0 Cf Cf 0 0 R RING gt choose 2 RING gt show subterm Cf 0 CE Cf Cf 0 CC 0 CE CE 0 0 R RING gt choose 1 2 RING gt show subterm C 0 0 R RING gt show term UE E O amp E Gi Ge EE Ge Ge OI amp Ue E E f 0 CCE 0 Cf Cf Cf Cf 0 CCE CF 00 0 0 R YRING gt The last command was used to print the entire term that had been started This command was also useful in the stepper cf Section 6 3 2 You may also print the subterm in a tree form as 150 9 2 Applying Rewrite Rules RING gt show subterm tree Cf GE f 0 Cf Cf f 0 R RING gt The current term subterm etc can also be printed by show command as cf Sections eL 9 25 RING gt show context current context module 7 special bindings term f 0 Cf Cf 0 E Cf Cf 0 a E EEE DM gt E E GENO EEE E 0 0 Cf Cf 0 0
85. S defining module N _ done N gt show M module M imports protecting BOOL signature rs Op ert S M gt show N module N imports protecting BOOL signature S N gt Notice that the prompt changed to M N each time M N was defined or inspected The current module hence context can be shown as follows N gt show context current context module N special bindings term none subterm no subterm selection is made by choose bindings empty selections empty pending actions none stop pattern not specified N gt The output contains the states that are local to the current context For example under 116 8 1 Names and Contexts bindings are listed context variables Section 6 5 The others concern theorem proving tools to be explained Chapter 9 show command is also used to print contexts To print the context of M type Cafe0BJ gt show module tree M A submodule of a module is identified by a name so during a session it is possible for the definition of a submodule to change when you redefine that submodule or when you unintentionally use the same name for a different module In such a case the system does not take any housekeeping exercise until necessary until for example an evaluation command is entered You may make the system to be more diligent by flicking a switch Cafe0BJ gt set auto reconstruct on When
86. UTH Identifier contains char acter strings Bool contains true and false e Propositional connectives are and or gt not lt gt and xor exclusive or e An irreducible term is constructed out of and xor true false and identifiers It is in disjunctive normal form by regarding xor as disjunction In particular tautologies are reducible to true e The precedences of connectives are ordered as not and xor or gt lt gt Evaluations in this module proceed as follows Firstly a gt b lt gt not b gt not a 109 7 OPERATOR ATTRIBUTES states a gt b 7b gt a a tautology equivalence of contrapositives 110 Cafe0BJ gt select PROPC PROPC gt set trace on PROPC gt reduce a gt b lt gt not b gt nota reduce in PROPC a gt b lt gt not b gt not a 1 gt 1 1 lt 1 1 gt 2 1 lt 2 1 gt 3 1 lt 3 1 gt 4 1 lt 4 1 gt 5 1 lt 5 1 gt 6 1 lt 6 1 gt 7 1 lt 7 1 gt 8 1 lt 8 1 gt 9 1 lt 9 rule eq p Prop gt q Prop p Prop and q Prop xor p Prop xor true p Prop gt a q Prop gt b a gt b gt a and b xor a xor true rule eq p Prop gt q Prop p Prop and q Prop xor p Prop xor true p Prop gt not b q Prop l gt not a not b gt not a gt not b and not a xor not b xor true rule eq not p Prop p Prop xor true p Prop gt b not b gt b xor true ru
87. Variable Declaration Axioms require representations of classes of elements as well as specific elements You have to be able to say e g that the successor of any natural number is greater than that number A variable represents this any In CafeOBJ every variable belongs to a sort and represents an arbitrary term of that sort Variables are declared as follows Syntar 42 variable declaration var ariable_name sortzname vars list_of variable_names sort_name A variable name is a character string and a list of variable names is blank separated Here is an example var N Nat vars ABC Nat In former versions var and vars are interchangeable This version becomes linguistically more strict var is for exactly one variable while vars is for one or more variables 37 4 AXIOMS In former versions commas could be used as separators so that the above declaration may be replaced with vars A B C Nat But this construct no longer works the system would regard as another variable A simple way to know the typing discipline of a language is to see variable declarations CafeOBJ adopts a strong typing discipline in that each variable has a syntactically deter mined type sort Another point of view comes from the definition of well formedness A term is well formed iff it has a unique least parse Section 3 3 1 A variable is a term Hence it must have a unique least sort the sor
88. Y lt LIST AS STACK The result is a module with parameter X originated from LIST This module defines trays of lists of Elt Note that LIST AS STACK omits the map from Elt of X to itself This is an example of implicit submodule mapping cf Section 8 2 6 You may further instantiate LIST TRAY by binding something to X which is ONE the module of an arbitrary set In case of b you bind something to X of STACK which is the module ONE For example module NAT TRAY protecting TRAY X Y lt view to SIMPLE NAT sort Elt gt Nat creates a module whose trays consist of stacks of natural numbers trays of mathemati cians perhaps Note that X Y is a qualification of a parameter name by another parameter name cf Section 8 1 3 NAT TRAY is not parametric as a result of the instantiation STACK becomes in effect a plain submodule of NAT TRAY 6 It has been a ritual to embed elements as one length lists with a subsort declaration This practice is not recommended since you may unable to get pushouts as desired See the Haxhausen s paper in AMAST 96 for detail 136 8 4 Module Expression 8 3 5 Qualifying Parameter Names Parameter names may conflict when a parameterised module imports another parame terised module To disambiguate parameter names you may qualify them by module names Section 8 1 3 For example in module AXE ab ooo module C X DJ protecting A X is both the parameter na
89. _ NeStack gt Nat op pop_ NeStack gt Stack eq top push X Nat S Stack eq pop push X Nat S Stack ou U Ps top push s s 0 empty is well formed It parses and reduces as Cafe0BJ gt select STACK OF NAT STACK OF NAT gt parse top push s s 0 empty top push s s 0 empty Nat STACK OF NAT gt reduce top push s s 0 empty reduce in STACK OF NAT top push s s 0 empty s s 0 NzNat 0 000 sec for parse 1 rewrites 0 000 sec 1 matches STACK OF NAT gt Without introducing error sorts the term top pop push s 0 push s s 0 empty is ill formed top requires non empty stacks as arguments but the coarity of pop is Stack which contains the empty stack CafeOBJ regards this term like 4 2 as well formed but of an error sort Nat On evaluation it reduces to a well formed term of a valid sort STACK OF NAT gt parse top pop push s 0 push s s 0 empty top pop push s 0 push s s 0 empty Nat STACK OF NAT gt reduce top pop push s 0 push s s 0 empty reduce in STACK OF NAT top pop push s 0 push s s 0 empty s s 0 NzNat 0 000 sec for parse 2 rewrites 0 000 sec 2 matches STACK OF NAT gt A meaningless term as before remains meaningless 91 6 EVALUATING TERMS STACK OF NAT gt parse top pop push s 0 empty top pop push s 0 empty Nat STACK OF NAT gt reduce top pop push s 0 empty reduce in STACK OF NAT top
90. advice if you are in doubt enclose with parentheses Parentheses i E help you avoid many parsing ambiguities 25 3 SIGNATURE 3 2 2 Behavioural Operator Declaration For hidden sorts you need a special kind of operators called behavioural operators Syntar 31 behavioural operator declaration bop standard_operator_symbol list_of_sort_names gt sort_name bop mixfiz_operator_symbol list_of_sort_names gt sort_name Standard operator symbols mixfix operator symbols lists of sort names and sort names are as in op in the previous section It is required that e The arity of a behavioural operator contain exactly one hidden sort Intuitively you may regard a hidden sort as consisting of objects which have internal states Then a behavioural operator is an attribute or a method if you really really want to adopt the parlance of a certain community As an illustration consider bank account objects whose balances change upon deposits and withdrawals Account bop deposit Account Nat gt Account bop withdraw Account Nat gt Account bop balance Account gt Nat Here deposit withdraw are operations that modify internal states balances of ac counts so they are methods while balance reads the current balances of accounts so an attribute The above intuition tells you why a behavioural operator should have exactly one hidden sort in its arity It does n
91. alifier Nat SIMPLE NAT refers to the sort Nat in the context of SIMPLE NAT Note that this does not imply that Nat is declared in SIMPLE NAT it only says that somewhere in the context of SIMPLE NAT Nat is declared If in the context of SIMPLE NAT more than one Nat are declared the qualifier fails to identify which In that case you have to be more specific The above qualification of operator names are for referring to operators in show II commands mappings etc You cannot use qualification in writing a term 8 1 4 Referring to Operators Operator names appear in renaming and view declarations both are to be explained In these constructs a single name may refer to more than one operators due to overload 118 8 1 Names and Contexts ing Special care needs to be taken therefore to see which operator names refer to which operators Note first that you have to distinguish operators with different number of arguments as op f Nat gt Nat and op f Nat Nat gt Nat This problem does not arise if operators are mixfix since their symbols contain placeholders e _ s All in all you have this definition Syntax 60 operator name mixfiz_operator_symbol standard_operator_symbol y number_of_arguments You should not insert blanks between the operator symbol and or between and the number of arguments Using this form the above two declarations may be
92. an unam biguous static mapping CafeOBJ extends the concept in two directions An operator 23 3 SIGNATURE may transform an element into another Such an operator is defined by transition relations Section 4 3 Moreover an operator may change an internal state of an element Such an operator is defined from an observational viewpoint 3 2 1 Operator Declaration Like the other strongly typed languages CafeOBJ requires you to make explicit the do mains and codomains of operators and only allows terms constructed accordingly Since CafeOBJ is order sorted however well formedness involves subtle considerations see Sec tion 3 3 1 In addition to domains and codomains operator declarations determine term constructs CafeOBJ allows you to employ various notations in writing terms such as infix e g 2 4 prefix 4 and postfix 2 Hence in declaring operators you have a way to adopt your favourite notational practice If you do not show any preference you get a standard notation for function application For example given a ternary operator f a term thereof is constructed out of parenthesised comma separated arguments such as f a b c A declaration for such an operator is called standard Syntax 29 standard operator declaration op standard_operator_symbol list_of_sort_names gt sort_name A standard operator symbol is an arbitrary character string that does not contain an un derb
93. and say more on this construct later Section 9 2 4 Substitutions are of the form Syntax 76 substitution specification in apply command with variable term 146 9 2 Applying Rewrite Rules This option is necessary only when the action is a rewrite rule and binds variables that appear in the rule see the next section for why this option exists Ranges and selections are as follows range within at within means at or inside the sub term specified by the selection while at means exactly at the sub term selection selector of selector x selector top term subterm C number_list sublist i Ea subset 39 top and term mean the entire term subterm means the pre chosen subterm see the next section For the other alternatives e The list of numbers separated by blanks within indicates a subterm by tree search For example 2 1 means the first argument of the second argument if a b c is the term of concern it means b e The selector makes sense only with associative operators and indicates a subterm in a flattened structure For example if _ _ was declared associative and given a term a b c d e 2 4 means b c d while 2 2 means b The latter case can be abbreviated to 2 e The selector makes sense only with associative and commutative o
94. ant to the factorial They are and this module is certainly artificial it is only declared to show that we can compute the factorial of rationals Well sometimes The sort ordering in RAT defines the graph All these sorts are of familiar kind Rat Int Nat are the sorts of rationals integers and natural numbers respectively and Nz means non zero Zero is a one point set containing 0 Unlike our SIMPLE NAT naturals may be written 1 43 107 etc in this built in module RAT defines the division op _ _ Rat NzRat gt Rat Now I Int J Int is ill formed since I J is a rational while _ takes only natural number arguments But CafeOBJ parses it as well formed as follows CafeOBJ gt parse in FACT I Int J Int I J Rat Recall that the result of parsing is a pair of a parenthesised term and its least sort Here the least sort is shown to be a questionable Rat The naming convention is implementation dependent and should not bother you but you should be bothered to know to that the name denotes an error sort over Rat i e a sort consisting of error elements as well as rationals For any integers I and J then I J is well formed although its sort has a dubious name It follows that 89 6 EVALUATING TERMS 4 2 is well formed Try parsing then evaluating the term and you get Cafe0BJ gt select FACT FACT gt parse 4 2 4 2 Rat FACT gt reduce 4 2
95. ar _ A list of sort names is a blank separated list and designates the arity of the operator The sort name after gt designates its coarity Sort names in arities and coari ties may be qualified cf Section 8 1 3 The pair of the arity and the coarity is called the rank of the operator An operator with the empty arity is a constant It is possible for a standard operator symbol to contain blanks For example in op a constant of sort S gt S the whole a constant of sort is a symbol More precisely the system treats the symbol as a blank separated list of non blank character strings and arbitrary numbers of blanks may be inserted But parsing terms that contain such symbols tends to be erroneous and you of ten have to enclose the symbol with parentheses For this reason it is advisable not to use blanks unless your aesthetics so forces If not standard a declaration is called mizfiz Syntax 30 mixfix operator declaration op mixfiz_operator_symbol list_of_sort_names gt sort_name A mixfix operator symbol may contain underbars Arities and coarities are the same as in standard operator declarations In fact the only difference from standard declarations is the presence of underbars Underbars reserve the places where arguments are inserted The 24 3 2 Operator Declaration leftmost underbar is for the first argument the next leftmost the second and so on The numb
96. as 59 5 INSPECTING MODULES module MONOID via ope gt M op _ _ MM gt M vars XYZ M eq X Y Z X Y Z eqe xX X eqX xe X When you write down the above module what is intended is not only a trivial monoid the singleton e But that is exactly the tight denotation of this module which you would get if it were declared with module In this case a module should accommodate any model so long as it has an associative binary operator with an i e the identity element A module introduced with module is always interpreted as such Another example uses behavioural operators module COUNTER protecting SIMPLE NAT Counter bop read Counter gt Nat bop add Nat Counter gt Counter eq read add N Nat C Counter N read C Your intention is to define a counter that is incremented by the operator add Tight deno tation would lead to the model where e g for a fixed counter c add s 0 add s s 0 c add s s 0 add s 0 c are different elements Intuitively this model says that adding 1 then 2 is different from adding 2 then 1 When your sole concern is the return values of read this model works fine adding 2 then 1 increments the counter by 3 so does adding 1 then 2 But there is no reason to preclude a model where the above two terms denote the same element the order of addition is immaterial Hence this module was introduced with modul
97. ator is a constructor of the coarity sort For example op nil gt List constr op __ List List gt List constr states that nil and __ are constructors of List The idea of constructors is very important for many purposes especially for theorem proving The current system however does not take advantage of this concept in any way To the system constr is a comment 7 4 Evaluation Strategy CafeOBJ allows the user to specify evaluation strategies of terms In general evaluation is nondeterministic In selecting which rule to apply to which subterm there is a certain license And the selection affects performance It may even decide whether the evaluation terminates 7 4 1 E Strategy Attribute Many recent functional programming languages are using lazy evaluation strategies There are several arguments for this trend but unfettered laziness is not recommended like in everyday life One way to avoid its harmful effects is to incorporate in compilers a mecha nism to intermingle eager evaluation strategies so long as it does not change the results of computation To see if it affects the results strictness analyses are employed In CafeOBJ you need not be thoroughly lazy or eager It allows you to assign different strategies to different operators This means that you can have the best of both worlds or eat and have a cake at once Moreover the system computes default strategies case by case based on a rapid strictnes
98. behavioural equivalence is not preserved under this mapping even though the single axiom of COUNTER is preserved You should have ensured that no additional observation is imposed on the image of Counter The conditions on views are sufficient for this purpose And note well that if you pay respect to the conditions behavioural equivalence is preserved whenever the explicitly given finite axioms are preserved 8 2 6 Succinct Views Fully to spell out the necessary maps may lead to unwieldy views In the previous section you already get a hunch that imported sorts and operators induce explosion In fact it is possible to omit some obvious maps the system guesses the missing pieces by the following rules Unless explicitly written otherwise 1 If the source and target modules have common submodules all the sorts and modules declared therein are assumed to be mapped to themselves 2 If the source and target modules have sorts and or operators with identical names they are mapped to their respective namesakes and 3 If the source module has a single sort and the target has a principal sort the single sort is mapped to the principal The rules 1 and 2 are obviously helpful they allow you to omit the obvious A principal sort is declared within the header part of a module declaration as follows Syntaz 64 module with principal sort module module_name list of parameters principal sort sort_name mod
99. ct to understand the following output It is enough to know the flavour of difference between show and describe SIMPLE NAT gt describe op _ _ name SE module SIMPLE NAT number of arguments 2 default attributes rewrite strategy not specified syntax precedence not specified computed prec 41 form arg 41 arg 41 theory rank Nat Nat gt Nat module SIMPLE NAT theory rewrite strategy 1 2 0 precedence 41 lower oprations Nat Nat gt Nat axioms rank Nat Nat gt Nat module SIMPLE NAT theory rewrite strategy 1 0 2 0 precedence 41 axioms equation 1hs 0 N Nat rhs N Nat top operator Nat Nat gt Nat equation lhs s N Nat N Nat rhs s N Nat N Nat top operator Nat Nat gt Nat SIMPLE NAT gt 54 5 1 Using Inspection Commands 5 1 4 Inspecting Records As explained in Section 3 4 1 a record declaration has the same effects as several related declarations of sorts and operators You may be anxious to know how the system handles record declarations If you are put the record Date into a module declaration and inspect it CafeOBJ gt module DATE 4 protecting SIMPLE NAT record Date year Nat month Nat day Nat defining module DATE _ done Cafe0BJ gt select DATE DATE gt show sorts visible sorts Date Date lt RecordInstance RecordDate RecordDate lt RecordId Slotyear Slotyear lt AttrId Slotmonth Slotmonth
100. ctively The command acts like reduce or execute and reduces the given term If the module expression is omitted the reduction occurs in the current module if The compiled code does not distinguish behavioural axioms as such and reduce Z option acts like breduce command Upon accepting the command the system 1 Compiles the rewrite rules of the module into an abstract machine if they have not been compiled already Then it 2 Runs the abstract machine on the given term The output you get is more or less the same as when reduce or execute commands are used For example with MULT Section 6 3 1 you have MULT gt tram reduce s s s 0 s s s s s 0 s s s s s 0 reduce in MULT s s s 0 s s s s s 0 s s s s s 0 s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s 0 NzNat rtime 3 utime 3 stime O rewrite 118 gc 0 MULT gt For comparison the corresponding ordinary evaluation works as follows MULT gt reduce s s s 0 s s s s s 0 s s s s s 0 reduce in MULT s s s 0 s s s s s 0 s s s s s 0 s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s
101. d execute exec b reduce bredl Other abbreviations may be accepted by the system But unless explicitly stated in the manual correct behaviours are not guaranteed Some of the commands takes many different kinds of arguments It is unlikely for you to remember all In such cases the system interprets the argument as your desperate call For example Cafe0BJ gt set prints a list of arguments acceptable to set command to be introduced immediately 1 3 2 Switch Toggling Command The system maintains various kind of switches By definition a switch is two valued on and off The following command changes the value of a switch Syntax 12 set command for switches set switch_name 4 on off As explained in Section 1 3 1 you get a list of available switches by just typing Cafe0BJ gt set and the current value of switches are listed by CafeOBJ gt show switches 10 1 3 Some Helpful Commands for show command see Section 1 3 3 A switch that affects the general behaviour of the system is verbose After this switch is turned on the system suddenly becomes talkative in responding to many commands such as show and describe Another such switch is quiet If this switch is on the system does not bother you with messages other than blatant error messages Other switches are relevant to the specific commands of the system and will be explained as the need arises Available switches
102. de 76 strong typing 38 structural induction 142 165 subsort 22 substitution 63 supersort 22 switch 10 T term qualification 32 term rewriting system 44 63 terminating 65 tight denotation 16 trace of evaluation 66 71 transition 42 TRS 63 U unconditional equation 39 V variable 37 view 124 visible sort 21 W well formed term 27 193
103. den ignored _ done 3 1 2 Subsort Declaration You may define a partial order over sets of sorts which is interpreted as set inclusion Such an order is denoted with lt If A lt B we say A is a subsort of B and B a supersort of A To declare this relation you use Syntax 28 subsort declaration E list_of_sort_names lt list_of_sort_names lt list_of_sort_names J list_of_sort_names lt list_of_sort_names lt list_of_sort_names enclose visible sorts and hidden ones as before A list of sort names is as in a sort declaration but it can be qualified qualification is explained in Section 8 1 3 The above syntax means that each sort in the first list is a subsort of each sort in the second each sort in the second is a subsort of each sort in the third and so on Note that lt although looking a strict relation is non strict and means less than or equal to or subset of or equal to For example the usual inclusion of natural numbers Nat into integers Int and Int into rationals Rat may be written down as Nat lt Int lt Rat or Int lt Rat Nat lt Int 22 3 2 Operator Declaration or Nat Int lt Rat Nat lt Int For a briefer description you may put more than one declarations within a single bracket pair using commas for separation For examp
104. e as above 5 2 4 Inspecting Hidden Sorts Two terms of a hidden sort is equal or behaviourally equivalent iff they behave the same under any behavioural context cf 7 or observation An observation is a term of a visible sort which contains exactly one occurrence of one variable of the hidden sort So an observation is a special derived operator see Section 8 2 2 In the example of COUNTER the observations for Counter is of the form read X read add m X read add m add m X 60 5 2 Some Typical Modules where X is a variable of sort Counter and m m are arbitrary terms of sort Nat For this special case therefore the above definition means that two terms t t of sort Counter are behaviourally equal iff the equations eq read t read t eq read add m t read add m t eq read add m add m t read add m add m t hold Unlike equality over visible sorts equality over hidden sorts are unlikely to be determined by straightforward reduction two terms may well turn out to be behaviourally equivalent even if they have different irreducible forms It is still possible however to use reduction to help prove behavioural equivalence As explained in Section 4 4 3 the system associates a binary predicate _ _ to each hidden sort and declare an axiom You may inspect the detail as the following example shows Cafe0BJ gt module COUNTER 4 protecting SIMPLE
105. e and declare such operators on least sorts after if necessary adding new common subsorts What the system checks is a sufficient but not necessary condition There are cases the system is overprotective As an example consider module INTB NonPos Nat lt Int op _ _ NonPos NonPos gt NonPos op _ _ Nat Nat gt Nat op _ _ Int Int gt Int op 1 gt Nat op 1 gt NonPos 28 3 3 Terms INTB is regular a term is of the form of a binary tree where all the nodes contain and all the leaves contain 1 or 1 and is of sort NonPos iff every leaf is 1 of sort Nat iff every leaf is 1 and of sort Int iff otherwise If you invoke regularize command however you get a modified module module INTB NonPos Nat lt NonPos Nat lt Int op _ _ NonPos Nat NonPos Nat gt NonPos Nat op _ _ NonPos NonPos gt NonPos op _ _ Nat Nat gt Nat op 8 Ite do gt Tnt op 1 gt Nat op 1 gt NonPos Y The reason is as follows If Nat NonPos are both inhabited there is a danger that their intersection is not empty If it is indeed non empty an application of _ _ on any terms in it creates a term both of sort Nat and of NonPos So it is safe to add a new common subsort and declare _ _ on it To check the non emptiness is too hard to solve mechanically For example if you insert an equation Section 4 2 1 eq 1 1 into INTB there does exist an element namely
106. e nothing less so you can declare on the fly wherever you can write a term For the exact scope of on the fly declarations see the next section 4 2 Equation Declaration 4 2 1 Unconditional Equation Declaration A plain equation is an axiom Anticipating conditional cases we call it unconditional Syntar 44 unconditional equation declaration eq label term term The last period preceded by a blank is a must It is the way to notify the system of the end of a term separates the lefthand side from the righthand in equations is used by the system to detect the end and start of a term You should supply blanks on both ends as in eqX O0 X J Without blanks the system thinks the lefthand side is continuing For example eq X 0 X causes the system to treat the entire text after eq and the subsequent text until it encounters a lonely as the term on the lefthand side Since an equation is a statement that the two sides are equal they must belong to a common universe of discourse For example to say that Marie Antoinette equals 3 1416 is nonsense In many sorted logic this consideration is formalised as two terms must be of the same sort CafeOBJ which is based on order sorted logic is more accommodating The sorts of the terms must belong to the same connected component in the graph defined by the sort ordering Accordingly 1 may be equal to 1 0
107. e first recall SIMPLE NAT which defines natural number addition Section 2 2 module SIMPLE NAT Zero NzNat lt Nat op 0 gt Zero op s Nat gt NzNat op _ _ Nat Nat gt Nat vars N N Nat eqO N N eq s N N s N N Everything in this module has been already explained so you should know that this is indeed a standard recursive definition of addition A subtle point is in the use of subsort relation Here the set of natural numbers is the union of Zero which contains 0 and nothing else and NzNat which contains s 0 s s 0 and so forth Suppose this definition is in the file simple nat cafe Then you may get the following session 49 5 INSPECTING MODULES Cafe0BJ gt input simple nat processing input simple nat cafe defining module SIMPLE NAT _ done Cafe0BJ gt show SIMPLE NAT module SIMPLE NAT 4 imports protecting BOOL signature Nat Zero NzNat lt Nat NzNat NzNat lt Nat Zero Zero lt Nat op 0 gt Zero op s Nat gt NzNat op Ae Nat Nat gt Nat i strat Cl ON2 F axioms var N Nat var N Nat eqO N N eq s N N s N N Cafe0BJ gt When invoked with a module name show command prints the entire contents of the module You may notice that e Block constructs imports signature and axioms Section 2 2 are used even though you did not use them e The module BOOL is imported automatically As explained ea
108. e for ground terms the system allows variables within terms to be reduced Here is an example corresponding to the second reduction above SIMPLE NAT gt reduce s X Nat 0 I reduce in SIMPLE NAT s X Nat 0 s X Nat 0 NzNat 0 000 sec for parse 1 rewrites 0 000 sec 6 matches SIMPLE NAT gt But note that the system does not treat non ground terms as such It treats variables as if they were constants and would not attempt unification 9 2 Applying Rewrite Rules In Section 9 1 it was shown that reductions can be used to prove some theorems For more demanding theorems they are inadequate Consider the additive group theory written in CafeOBJ module GROUP 4 CG op 0 gt G op _ _ G G gt G assoc op C gt G var X G eq0 x X Ge 20 r A 0 Suppose you want to show that X is also a right inverse so the inverse Using open you may write a score as open GROUP opa gt amp reduce a a or using a constant on the fly just reduce in GROUP a G a But the result of reduction is simply CafeOBJ gt reduce in GROUP a G a reduce in GROUP a G a G Geis lt gt AGE 0 000 sec for parse 0 rewrites 0 000 sec 8 matches CafeDBJ gt 145 9 THEOREM PROVING TOOLS which is no wonder since no equation has a matching lefthand side In fact a standard proof goes as follows a a Orar La s EDESA Ga s
109. e operator _ _ such as N 0 The sign in the former denotes an equivalence relation and this relation per se steer a wide of syntactic manipulation _ _ is an operator that generates terms which are subject to manipulation within the language processors Still they are related as follows if the underlying term rewriting system is confluent and terminating X X holds iff X X true does 4 4 2 Transition Predicate The predicate for transition relation written gt is a binary operator defined on each visible sort As with in the previous section an explicit declaration would be of the form pred _ gt _ SS for each sort S This predicate is in fact declared on the universal sort in a module called RWL RWL is imported implicitly when a module contains transition declarations Section 4 3 As with BOOL Section 2 5 it is possible to switch off this implicit importation by the command CafeOBJ gt set include RWL off A transition relation is reflexive transitive and is closed under operator application When RWL is imported the system supplies a set of axioms Firstly for each visible sort S an axiom 44 4 4 Internalising Axioms eq X S gt X true is declared In fact a single equation declared in RWL works for any S This axiom states reflexivity Secondly for each unconditional tranision trans t gt t the system declares
110. e the term is parenthesised to reveal connectivity Int on the right of is its least sort 3 3 3 Qualifying Terms Ambiguity that arises from operator connectivity e g M M s 0 above can be eliminated by parentheses On the other hand ambiguity caused by over loading cannot be so easily eliminated It requires additional sort information Hence term qualification as Syntax 36 sort qualified term O term sortname This version unlike former versions allows blanks around The following terms are all valid and parsed as the same empty Stack empty Stack empty Stack empty Stack Be sure to put parentheses around the qualified CafeOBJ allows inline variable declarations such as M Nat s 0 where M is regarded at this place only as a variable of sort Nat Without parentheses e g empty Stack is regarded as a new variable For example consider the following module declarations 32 3 4 Record Declaration module OCTAL 4 OctalDigit ops 01234567 gt OctalDigit IP module HEX 4 HexDigit ops 0123456789 gt HexDigit ops ABCDEF gt HexDigit E module HEX OCTAL 4 protecting OCTAL protecting HEX p Since HEX OCTAL contains declarations either in OCTAL or in HEX the digits 0 through 7 are ambiguous there they are constants both of OctalDigit and HexDigit Indeed try parsing 0 and you get a warnin
111. e whole term if there is a rewrite rule that defines the operator such that in the place of the argument a non variable term appears For example given a binary operator f and suitable variables X and Y in the place of the first argument is a variable in eq X Y h X while it does not in eq f g X Y h Y If all the rewrite rules are of the former type the first argument need not be evaluated immediately Since any term of a relevant sort matches a variable matching possibilities are unaffected Furthermore if the only rewrite rule defining f is eq X Y h Y you are well advised to evaluate it later or never the righthand side does not contain X so evaluating it is futile On the other hand if there are rules that contain non variable terms in the argument place the result of evaluating the argument affects matchability so it is safe to evaluate it first To be on the safe side the default strategy always ends with 0 Former ver JI sions added last zeros even for user supplied stategies We concluded that this practice reminded us of overprotective nannies and abandoned it If an operator definition is recursive CafeOBJ may ignore an explicit E strategy and apply recursive rules successively This is a kind of optimisation To avoid this behaviour give an E strategy that does not have O at the head of the list 102 7 4 Evaluation Strategy 7 4 3 Lazy Evaluation CafeOBJ provides tw
112. eduction traces They show that the first reduction immediately cancelled a right identity zero while the second reduction which could not rely on the knowledge that zero is also a left identity took two rewrites to get the result Sometimes more elaborate traces are desirable 71 6 EVALUATING TERMS SIMPLE NAT gt set trace whole off SIMPLE NAT gt set trace on SIMPLE NAT gt reduce s 0 0 reduce in SIMPLE NAT s 0 0 1 gt 1 rule eq s N Nat N Nat s N Nat N Nat N Nat gt 0 N Nat gt O 1 lt 1 s 0 0 gt s 0 0 1 gt 2 rule eq 0 N Nat N Nat N Nat gt 0 1 lt 2 0 0 gt 0 s 0 NzNat 0 000 sec for parse 2 rewrites 0 000 sec 3 matches SIMPLE NAT gt This time each rewrite step was explained in more detail The three lines starting with 1 gt correspond to a single step They show the rewrite rule i e equation or transition applied the substitution used and the replacement trace whole switch traces the entire term while replacements shown by trace switch focus on the changed subterms This difference was illustrated by the last step of this example where trace whole printed 2 s 0 0 gt s 0 while trace printed 2 0 0 gt 0 6 2 6 Examples of Conditionals To illustrate the r le of conditions we first define an operator that computes greatest common divisors by filling more meat in the bony SIMPLE NAT 72 6
113. em to process definitions and commands their effects are slightly different Modules defined in prelude files whether standard or user supplied are treated as preludes This difference reveals itself when e g reset command Section 1 1 is invoked Finally if you are disinclined to remember all of the above just memorise the help option cafeobj help lists the available options 1 2 4 Batch CafeOBJ If you do not want to pay much attention to the system you may run the system non interactively An option batch causes the system to run on the batch mode and the system terminates immediately This is useful in processing a large file For example cafeobj batch goliath gt cafe out forces the system to read and process goliath or goliath bin or goliath cafe or goliath mod while you have an afternoon tea 1 2 5 Module Libraries As suggested in the previous section Cafe OBJ maintains a list of search directories Some of them are standard You may change the list by 1 or 1 options as explained in Section 1 2 3 You may also change it during the session with set command Section 1 3 2 For example Cafe0BJ gt set libpath usr home maria cafe usr home tania cafe adds the two directories to the search list while Cafe0BJ gt set libpath usr home maria cafe usr home tania cafe 1 DIALOGUE WITH THE SYSTEM replaces the search list by the twosome Each pathname should be separated by
114. emonstrate that certain properties called inductive properties hold for the term generated models of a module including its initial model Recall that module denotes such a model while module has both tight and loose denotations Since SIMPLE NAT was declared with module what was proven in Section 9 1 1 is a property that does not necessarily hold when SIMPLE NAT denotes loose models With this proviso structural induction is certainly a useful technique and you are often powerless without it Let us show a couple of examples For the sake of variety we use the predicate _ _ here The following sequence proves associativity of _ _ proving associativity of _ open SIMPLE NAT ops abc gt Nat reduce 0 a b O a b eq a b c at t b c hypothesis reduce s a b c s a b tec close The session goes as follows Cafe0BJ gt open SIMPLE NAT opening module SIMPLE NAT_ done SIMPLE NAT gt ops a b c gt Nat SIMPLE NAT gt reduce 0 a b O a b E reduce in O a b 0 a b true Bool 0 000 sec for parse 3 rewrites 0 000 sec 11 matches SIMPLE NAT gt eq a b c at b c SIMPLE NAT gt reduce s a b c s a b c reduce in s a b c s a b c true Bool 0 010 sec for parse 5 rewrites 0 000 sec 26 matches SIMPLE NAT gt close Cafe0BJ gt 165 10 PROVING MODULE PROPERTIES
115. en rewritten so far to cadr cons 1 cdr cons 2 cons 3 ni1 This term does not match the lhs as it is because the second argument of the outmost cons is dominated by cdr not by cons It does match however if the second argument is reduced with the usual rule for cdr to cons 3 nil 2 in the strategy states that the second argument is to be evaluated just at such moments Negative integers cannot be used if the operator is declared associative or commutative In such cases reduction on demand as explained above is nigh impossible to implement 103 7 OPERATOR ATTRIBUTES 7 4 4 Interpreting E Strategies To understand the exact meaning of E strategies it is instructive to know the overall algo rithm of evaluation It is shown below Remember that an E strategy is a list of integers Given a term f 1 Let l be the E strategy of the dominant operator of t 2 If l is empty exit with t as result Otherwise let n be the first element of l 2 1 If n 0 search a rewrite rule applicable to the whole t If one such is found replace t with the substitution instance t and go back to 1 2 2 If n gt 0 call this procedure recursively with the n th argument of t as input Replace the argument with the result and proceed to 3 2 3 If n lt 0 mark the n th argument of t as on demand and proceed to 3 3 Remove the first element from and go back to 2 Note that after the step 2 1 the control is back t
116. er of underbars must match the number of sort names in the arity The single underbar cannot be an operator symbol it would introduce invisible 1 operator applications Such a declaration is ignored and you are ridiculed by the system For example addition is usually written in the infix notation Declare op _ _ Nat Nat gt Nat and terms such as N M s 0 N are admissible Another representative example is a conditional expression op if_then_else_fi Bool Nat Nat gt Nat According to the definition this declaration allows you to write if N lt M then N else M fi and if true then O else s 0 fi Since CafeOBJ allows operator overloading it is possible to use the same operator symbol for different operators For example the symbol _ _ may be overloaded as follows op _ _ Nat Nat gt Nat op _t_ Set Set gt Set An operator symbol whether standard or mixfix does not only define term constructs but acts as an operator name What an operator name refers to is a nontrivial question due to overloading possibilities see Section 8 1 4 for detail You can declare several operators simultaneously if they have exactly the same rank use ops instead of op as ops _ _ _ _ Nat Nat gt Nat which means the same as op _ _ Nat Nat gt Nat op _ _ Nat Nat gt Nat Note that in simultaneous declarations parentheses are sometimes necessary to separate operator symbols A general
117. erm c matched to the pattern c with the substitution true Bool 0 000 sec for parse 6 rewrites 0 000 sec 13 matches CHOICE NAT gt There are three transitions from a b that is trans N N N trans N N gt N trans a gt c respectively yielding a b and c b The first branch further transits to c which matches the given destination 10 2 3 Systematic Search for Transition Relations _ gt _ can often be used directly Continuing the example of CHOICE NAT Cafe0BJ gt select CHOICE NAT CHOICE NAT gt reduce 0 s 0 s s 0 s s s 0 s s s s 0 gt s s s 0 reduce in CHOICE NAT O s 0 s s 0 s s s 0 s s s s 0 gt s s s 0 true Bool 0 010 sec for parse 51 rewrites 0 020 sec 51 matches CHOICE NAT gt 168 10 2 Theorem Proving Techniques This was a very easy case since all the arguments to _ _ are are irreducible and only pure transition steps are involved A more demanding case is CHOICE NAT gt reduce 0 s 0 s s 0 s s s 0 0 s s s s 0 gt s s 0 s s s 0 s 0 reduce in CHOICE NAT O s 0 s s 0 s s s 0 0 s s s s 0 gt s s 0 s s s 0 s 0 true Bool 0 000 sec for parse 35 rewrites 0 000 sec 78 matches CHOICE NAT gt where the the system need to compute _ _ along the way If
118. ers were enclosed with square brackets 4 Do not forget to put blanks before and after For example the following modules define indexed lists where both indices and data may come from arbitrary sets module ONE Elt module ILIST IDX ONE DAT ONE 4 Ilist Elt DAT lt ErrD op undef gt ErrD op empty gt Ilist op put Elt IDX Elt DAT Ilist gt Ilist op _ _ Ilist Elt IDX gt ErrD vars I I Elt IDX var D Elt DAT var L Ilist eq put I D L I if I I then D else L I fi eq empty 1 undef Observe how the same module ONE is used as different parameters Inside ILIST sorts and operators of a parameter may be referred to with qualified names like Elt DAT cf Section 8 1 3 As an aside the current version of CafeOBJ has a built in module called TRIV which is the same as ONE above Using this built in you may as well have written module ILIST IDX TRIV DAT TRIV M Further error sorts such as ErrD are implicitly declared Section 6 6 so you need not declare ErrD as above 8 2 2 Pre view Not Preview This section contains a preliminary to the following sections and is rather technical To bind actual parameter modules to formals we need ways to relate two modules Since modules denote structures we rely on the idea of structure preserving mappings Such mappings are usually called homomorphisms Intuit
119. es cf set command Section 1 3 2 Various options control the initial state of the system q This option prohibits reading cafeobj p pathname Instead of the standard prelude file which is set up during installation the system reads the given pathname which must be a file The suffix convention is applicable here p pathname The sytstem reads the given pathname in addition to the standard prelude file 1 pathname list In processing input command the system searches the pathname list to locate the specified file For default search paths see Section 1 2 5 All the pathnames must be directories and the list must be separated by 1 pathname list Pathnames are added to the search directory list For example cafeobj p usr cern particle muon bin 1 usr cern 1lib std usr cern lib muon usr home eva cafe makes the system 1 read the standard prelude file 2 read muon bin in addition 3 set the search directories as given and 4 read the initialisation file cafeobj if it exists You may also make the system read files by giving them as arguments For example 6 1 2 Files and Libraries cafeobj lemmai lemma2 has the same effects as typing Cafe0BJ gt input lemmal messages from the system Cafe0BJ gt input lemma2 messages from the system at the beginning of the session Note that even though p options file name arguments and cafeobj all cause the syst
120. es equational theory attributes such as associativity Section 7 1 and tries all the possibilities as GROUP gt match O O O to X G Y G match success substitution X gt 0 Y G gt 0 0 gt gt More y n y match success substitution X gt 0 0 Y G gt 0 No more match GROUP gt Remember that _ _ was declared associative Modulo associativity there are two ways of matching the above two terms 158 9 3 Matching Terms It is possible for a term to contain variables both as a term specifier and as a pattern For example it is legal to try match X G 0 to O X G But this does not acts as expected GROUP gt match X G 0 to O0 X G no match GROUP gt match is a matching procedure not a unification If a term to the left of to contains a variable it is treated as a pseudo constant In the above example X acts as a constant and cannot be substituted by 0 9 3 3 Matching Terms to Pattern We next deal with the cases when the pattern designates a set of rules For illustration we add several equations before invoking matching GROUP gt open GROUP opening module GROUP_ done GROUP gt ops ab gt G GROUP gt eq X G Y G Y X GROUP gt eq a X G a Xz a GROUP gt start O tata GROUP gt match term to rules matching rules to term 0 a a 1 iseq0 X X substitution X gt a a 3 is eq X
121. esult of the second parse The current implementation accepts precedences between 0 and 127 inclusive Out of bound precedences cause warnings and are ignored 7 2 2 Left Right Associativity 1 assoc states that the operator which must be binary associates to the left and r assoc to the right A typical usage is as follows Under the declaration i ar SS Ss X S X X has two parses X X X X X X If you declare Qo 8 ES 8 SS OC the parse is uniquely determined as X X X while oo 2 S S SES SOCIA dictates the parse to be X X X When equational theoretic associativity assoc is declared the system has to decide how to decide connectivity In that case X X X is equal to J X X X anyway but it is necessary to decide on one or the other to store and manipulate terms In the current implementation the system assumes right associativity Left right associativity is allowed only on operators whose arities are both supersorts of the coarity Note that the conditions for assoc and for 1 assoc r assoc differ 1 assoc or r assoc is a parsing instruction There is no inherent reason to prohibit these attributes as long as you feel like it In fact the above condition only states that if it does not hold the attribute is almost meaningless 100 7 3 Constructor Attribute 7 3 Constructor Attribute The attribute constr states that the oper
122. ewhat artificial examples For the sake of brevity let us define a module without axioms module NAT INT Nat lt Int op _ _ Nat Nat gt Nat op _ _ Int Int gt Int Then we have a view view ID from NAT INT to NAT INT 4 sort Nat gt Nat sort Int gt Int op MU P ar which is just the pair of identity mappings Note that the operator map denotes two maps for _ _ on Nat and that on Int This is an example of overloaded operators being bundled into one Section 8 1 4 We have other endomorphisms 126 8 2 Parameters and Views view U from NAT INT to NAT INT 4 sort Nat gt Nat sort Int gt Nat Go sh gt 5 E view L from NAT INT to NAT INT 4 sort Nat gt Int sort int gt Int G A se E Zar U collapses Nat and Int into Nat Recall that the conditions on signature morphisms only require preservation of weak sort ordering Nat lt Nat holds so U does define a signature morphism The case of L is similar collapsing the two sorts into Int Even with relatively simple structures like this you have a couple of different views between modules 8 2 5 Not Quite a View We show why the conditions on views see Section 8 2 2 on specification morphisms are reasonable It is easy to see why you have to preserve ranks and sort ordering For example given a module module FUNCTION CSi op i S gt T y and a self mapping sort S gt i sort T gt S op f gt f it
123. fault view i e identity map ping from X i e ONE to IDX and DAT both ONE is bound to the parameters IDX and DAT The result of the instantiation is the sort of indexed lists whose indices and data belong to the same parametric sort Let us show a session that reveals what is going on Cafe0BJ gt module ILIST X ONE protecting ILIST X X defining module ILIST _ _ _ done CafeOBJ gt select ILIST ILIST X gt show params argument X protecting ONE ILIST X gt show subs protecting ILIST IDX lt X DAT lt X ILIST X gt The module ILIST has a parameter X and imports an instance of ILIST to whose param eters X are bound We continue the session and create an instance of ILIST ILIST X gt module ILIST NAT pr ILIST X lt view to SIMPLE NAT 4 sort Elt gt Nat defining module ILIST NAT _ done ILIST X gt 134 8 3 Binding Parameters ILIST NAT is a module of indexed lists whose indices and data are both natural numbers which is the same module as ILIST NAT in the previous section Finally you may use this parameter passing mechanism to get an alternative definition of enriched indexed lists as follows module ILIST EXT IDX ONE DAT ONE protecting ILIST IDX DAT protecting SIMPLE NAT op _ Ilist gt Nat var I Elt IDX var D Elt DAT var L Ilist eq put I D L s 0
124. ference from the previous traces is the presence of cond steps As explained in Section 6 1 1 the system reduces conditions when it checks applicability of conditional rewrite rules The above trace was the result of following all of those recursive evaluations For brevity we now resort to a very simple computation and show only the initial part of the initial trace GCD gt set trace whole off GCD gt set trace on GCD gt reduce gcd s s 0 s s 0 reduce in GCD gcd s s 0 s s 0 1 gt 1 apply trial 1 rule ceq gcd N Nat M Nat gcd M Nat N Nat if N Nat lt M Nat 2 gt 1 al 2 lt 1 2 gt 2 2 lt 2 2 gt 3 2 lt 3 1 gt 4 1 gt 4 M Nat gt s s 0 N Nat gt s s 0 rule eq s N Nat lt s M Nat N Nat lt M Nat M Nat gt s 0 N Nat gt s 0 s s 0 lt s s 0 gt s 0 lt s 0 rule eq s N Nat lt s M Nat N Nat lt M Nat M Nat gt 0 N Nat gt 0 s 0 lt s 0 gt 0 lt 0 rule eq N Nat lt 0 false N Nat gt 0 0 lt 0 gt false rewrite rule exhausted 1 apply trial 2 rule ceq gcd s N Nat s M Nat gcd s N Nat s M Nat s M Nat al 2 gt 4 2 lt 4 2 gt 5 al 2 lt 5 2 gt 6 if not N Nat lt M Nat M Nat gt s 0 N Nat gt s 0 rule eq s N Nat lt s M Nat N Nat lt M Nat M Nat gt 0 N Nat gt 0 s 0 lt s 0 gt 0 lt 0 rule eq N
125. g CafeOBJ gt parse in HEX OCTAL O Warning Ambiguous term please try check regularity command if the signature is regular there possibly be some name conflicts between operators and variables O sss ssssssssSsssssaSsSasassss 0 Al 8 a Octal Digiti aa 0 Error no successfull parse ambiguous term SyntaxErr Cafe0BJ gt To eliminate this ambiguity you may qualify by sorts Try again with CafeOBJ gt parse in HEX 0CTAL 0 OctalDigit and the system will oblige with O OctalDigit 3 4 Record Declaration A record declaration defines a record type data structure A record type consists of fields and an element of the type is completely determined by the value of each field In CafeOBJ a field is called slot 33 3 SIGNATURE 3 4 1 Plain Record Declaration A record declaration without inheritance see the next section is as follows Syntax 37 plain record declaration record record_name list_of_slot_declarations y where a list of slot declarations is a blank separated list A slot declaration has the following construct Syntaz 38 slot declaration slotname sortzname where a slot name is a character string and a sort name is the name of an already declared sort For example if Nat is a sort of natural numbers with usual digit notations record Date year Nat month Nat day Nat is a sloppy definition of records that c
126. gards an overloaded operator on subsorts as the restriction On Nat two _ _ s must behave identically Hence the rule 1 8 2 Parameters and Views One of the salient features of CafeOBJ is a parameter mechanism By putting aside certain sorts and operators as parameters you can declare a generic module A parameter unit is itself a module so that on top of syntactical requirements semantic constraints may be imposed on actual parameters To instantiate a parameterised module is to replace the parameters with modules that satisfy the syntactic and semantic constraints 8 2 1 Parameterised Module To declare a parameterised module attach a parameter interface to the module declaration construct Syntax 61 parameterised module module module_name list_of_parameters module_element yy A list of parameters is comma separated A parameter has the following construct Syntax 62 parameter importation_mode parameter_name module_name A parameter name is an arbitrary character string and is used to refer to the parameter module in the module body The module name after describes requirements that must be satisfied by the actual parameters The same module may act as distinct parameters 120 8 2 Parameters and Views and parameter names distinguish them For importation modes which are optional see Section 8 3 2 1 In ancient times paramet
127. ians CafeOBJ has two kinds of sorts hereafter called visible sorts and hidden sorts We leave it to you to decide whether the sort of politicians is visible or hidden 3 1 1 Sort Declaration The simplest sort declaration is as follows Syntaz 26 visible sort declaration E list_of_sort_names 1 A sort name is an arbitrary character sequence and a list of sort names is a list of such names separated by blanks For example Nat declares a single visible sort Nat while Nat Int Rat 21 3 SIGNATURE declares visible sorts Nat Int and Rat By replacing and with and respectively you get a hidden sort declaration Syntax 27 hidden sort declaration x list_of_sortnames In declaring operators Section 3 2 1 and axioms Chapter 4 you have to distinguish visible sorts and hidden sorts They give rise to different kinds of models and are totally disjoint Syntactically you must not use the same name for both a visible and a hidden sort The current implementation simply ignores dual declarations For example in the presence of a visible sort S the declaration S is silently ignored But declaring diffrent type produces a warning message for example Cafe0BJ gt module M S S defining module M Warning declaring a visible sort S there already be a sort with the same name but of differenct type visible hid
128. in that it imports a pa rameterised module without instantiation Let us see how the system treats such a module After feeding ILIST EXT you get Cafe0BJ gt select ILIST EXT ILIST EXT IDX DAT gt show params argument IDX ILIST protecting ONE argument DAT ILIST protecting ONE ILIST EXT IDX DAT gt show param IDX module IDX ILIST ONE imports protecting BOOL signature Elt ILIST EXT IDX DAT gt Look first at the new prompt In the previous section after the parameterised ILIST was selected the prompt changed to ILIST IDX DAT gt 133 8 MODULE STRUCTURE to indicate that the current module had two parameters The selection here of ILIST EXT also led to the prompt suggesting parameters As the show commands showed this module indeed has parameters IDX and DAT which are both the module ONE Since ILIST EXT is thus parameterised you can instantiate it just as you instantiate ILIST For example module NAT ILIST EXT protecting ILIST EXT IDX lt view to SIMPLE NAT sort Elt gt Nat DAT lt view to SIMPLE NAT sort Elt gt Nat defines a module of enriched indexed lists whose indices and data are both natural numbers In importing parameterised modules you can bind parameters to parameters passing parameters as in the following construction module ILIST X ONE 4 protecting ILIST X X Remember that this shorthand notation means that the de
129. ing Ambiguous term Please select a term from the followings GI Mate Tag gt May 02 02 0 0 gt ESTO Eme s NzNat M Int M Int 0 Zero RT ie Time gt Mig secs ean Sas See SSS Ene M Int a a M Int s NzNat 0 Zero Error no successfull parse ambiguous term SyntaxErr CafeOBJ gt If the term is ambiguous as in this example the system gives a warning as showed in the above And if you set switch select term to on you have an option to select a parse from possible choces Cafe0BJ gt set verbose off Cafe0BJ gt set select term on CafeOBJ gt parse in SIMPLE INT M M s 0 Warning Ambiguous term please try check regularity command if the signature is regular there possibly be some name conflicts between operators and variables Please select a term from the followings MM 2 Dam az gt Ways 0 9222 M Int M Int s 0 2 2 Tats Maz gt Taig 0 00 2202 M Int M Int s 0 Please input your choice a number from 1 to 2 default is 1 2 Taking the second as correct M M s 0 Int Cafe0BJ gt The number after the message Please is your input The system is impatient If you hesitate long it automatically selects the default in the above case 1 31 3 SIGNATURE The result of the parsing was Gl WP E0 e de wher
130. ing Module Properties 10 1 Check Command Some of the module properties are checkable syntactically within reasonable computation cost Syntar 79 check command check regularity compatibility module_expression check laziness operator_name A module expression may be omitted if the current module Section 8 1 1 is set regularity may be abbreviated to reg or regular compatibility to compat and laziness to lazy Regularity If the first argument is regularity the system checks if the module is reg ular Using INTB in Section 3 3 1 you can obtain the following message CafeOBJ gt check regularity INTB gt gt start regularity check gt gt The following sorts may be required for regularity Nat NonPos lt NonPos Nat gt gt The following operators may be required for regularity _ Nat NonPos Nat NonPos gt Nat NonPos Cafe0BJ gt while with SIMPLE NAT the system reports nothing as Cafe0BJ gt check regularity SIMPLE NAT gt gt start regularity check signature of module SIMPLE NAT is regular Cafe0DBJ gt 161 10 PROVING MODULE PROPERTIES Unlike regularize command Section 3 3 1 this command does not modify the signature Compatibility If the first argument is compatibility the system checks if the TRS defined by the module is compatible i e every application of every rewrite rule to every well formed term results in a well formed term Note
131. ion Commands There are three commands for evaluating terms Syntar 49 reduce command reduce in module_expression term eu Syntar 50 breduce command breduce in module_expression term n Syntax 51 execute command execute in module_expression term As is ever the case the period after a blank is a must reduce can be abbreviated to red breduce to bred and execute to exec Module expressions are introduced in Section 8 4 and we only consider module names here These commands evaluate the term with a TRS defined by the given module or by the current module Section 8 1 1 if the module expression is omitted These three commands differ on 1 which axioms constitute the TRS and 2 applicability of some rewrite rules 1 For reduce or breduce only possibly conditional possibly behavioural equations are taken to constitute the TRS Transitions are excluded This ensures that under certain conditions Section 6 1 2 reduce gives a decision procedure for equational theory For execute all the axioms constitute the TRS 65 6 EVALUATING TERMS 2 For reduce or execute a rewrite rule that come from a behavioural axiom is applicable only when the redex in enclosed in an observation This ensures the soundness of evaluation For breduce there is no such restriction The point 1 comes from the fact that reduce b
132. ious sections an explicit declaration would be of the form pred _ _ S55 for a given sort S Remember that behavioural operators are declared with bop and each such operator has exactly one hidden sort in its arity Section 3 2 2 On the assumption that a a implies f1 a f1 a for any attribute f and for any a if turns out to be congruent wrt all the method s the system declares an axiom eq A A f1 A f1 A and and fn A fn A where f1 fn are the attributes Recalling an example of bank accounts Account bop deposit Account Nat gt Account bop withdraw Account Nat gt Account bop balance Account gt Nat the above assumption is ceq balance A Account balance A Account if A A and is congruent if two equations eq deposit a n deposit a n true eq withdraw a n withdraw a n true hold on the hypothesis that eq a a true for arbitrary a a and n If the switch accept proof is on the default is off the system tries to prove these two equations by evaluation Chapter 6 If _ _ does turn out to be a congruence the system adds the axiom ceq A Account A Account if balance A balance A Intuitively this axiom states that two terms of Account are indistinguishable if they are indistuiguishable by a single application of balance 46
133. irable typically when you state theorems or want to define behavioural operators in terms of others 4 3 Transition Declaration Equality is an equivalence relation obeying three basic properties of binary relations re flexivity symmetry and transitivity Dropping one of these properties engenders interesting relations Partial equivalence is one of them By dropping symmetry we get a transition relation The following constructs define such a transition relation As with equations there are conditional and unconditional transitions and ordinary and behavioural ones Crossing these you get Syntax 48 transition declaration trans label term gt term ctrans label term gt term if boolean_term btrans label term gt term bctrans label term gt term if boolean_term 0 n u Syntactically transitions are the same as equations if you replace the equality sign by the arrow gt Similar restrictions apply here also For example the sorts of two terms must be in the same connected component trans may be abbreviated to trns ctrans to ctrns btrans to btrns and bctrans to bctrns The following little example illustrates the difference between equations and transitions module CHOICE State ops ab gt State op _l_ State State gt State vars X Y State trans X Y gt X trans X Y gt Y _ _ denotes an indeterminate s
134. is hard to know where to locate the image of f The conditions on hidden sorts and behavioural operators ensure the preservation of visibil ity mapping hiddens to hiddens behaviourals to behaviourals and observations The following counterexample illustrates the reason why views must reflect hidden sort ordering and be surjective on behavioural operators Recall the module COUNTER Section 5 2 3 and consider a module of bank accounts 3 Remember that lt denotes less than or equal to 127 8 MODULE STRUCTURE module SUBTRACT protecting SIMPLE NAT op _ _ Nat Nat gt Nat vars N N Nat eqO N 0 eqN O N eq s N s N N N module ACCOUNT protecting SUBTRACT Account bops deposit withdraw Account Nat gt Account bops balance point Account gt Nat var N Nat var A Account eq balance deposit A N balance A N eq balance withdraw A N balance A N eq point deposit A N point A s 0 _ _ on Nat is the usual pseudo subtraction you have already seen this definition in Section 6 2 6 as a preparation to declare GCD An account has a balance and a bonus point The bonus point increases each time you make a deposit If you identify a counter reading with the amount of your fortune it seems plausible to define a view by the following mapping sort Zero gt Zero sort NzNat gt NzNat sort Nat gt Nat op 0 gt 0 ops gt s op _t_
135. ively in 121 8 MODULE STRUCTURE module M S module M S module N TU the modules M and M are essentially the same since the difference lies only in the naming and M or M may be embedded in N since N defines an enlarged two sorted structure The following definitions are nothing more than the statements of the obvious like this tiny example They are complicated only because CafeOBJ is founded on a rich logical base Derived Operators A derived operator is just a term regarded as an operator For example under the module MULT Section 6 3 1 and for variables X and Y of sort Nat s 0 s s X s O X s X s Y and X X are all terms hence derived operators The important point here is that each such term can be assigned a rank inductively We have term rank s 0 gt NzNat s s X Nat gt NzNat s 0 X Nat gt NzNat s X s Y Nat Nat gt Nat X X Nat gt Nat It is easy to calculate the rank of a derived operator the sorts of the variables constitute the arity and the coarity of the dominant operator is the coarity Further given a signature the derived signature is the one containing every derived oper ator Thus if we denote derived operators by terms the derived signature of MULT looks like Zero NzNat lt Nat op 0 gt Zero op s Nat gt NzNat op _ _ Nat Nat gt Nat op _ _ Nat Nat gt Nat op s 0 gt NzNat
136. l Report SRI CSL 92 03 SRI International 1992 Jacobs B and Rutten J A Tutorial on Co Algebras and Co Induction EATCS Bulletin No 62 EATCS 1997 pp 222 259 Klop J W Term Rewriting Systems A Tutorial EATCS Bulletin No 32 EATCS 1987 pp 143 182 Meseguer J Conditional Rewriting Logic Deduction Models and Concurrency Proc 2nd International CTRS Workshop Lecture Notes in Computer Science 516 1991 pp 64 91 Meseguer J and Goguen J A Initiality induction and computability Algebraic Methods in Semantics Cambridge University Press 1984 pp 459 541 187 Index The first page number is usually but not always the primary reference to the indexed topic Keywords Commands gt 17 17 hidden sort declarations 22 for remaning 137 rules 157 module sum 138 gt 17 LF rules 157 bin suffix 5 cafeobj 6 cafe suffix 5 mod suffix 5 term stopper 30 76 abort 77 a 77 79 continue 77 ic 17 79 go 77 8 77 78 help 77 th 77 limit 77 21 77 next 77 in 77 78 pattern 77 p 77 80 q 77 80 rewrite 77 rew 77 rule 77 T T 19 stop 77 subst 77 s 77 79 lt 131 lt 22 46 44 gt 44 43 gt in transitions 42 b 47 in equations 39 77 help command 9 BOOL 19 41 RWL 44 visible sort declaratio
137. l away to an error environment Cafe0BJ gt C Correctable error Console interrupt Signalled by CAFEOBJ TOP LEVEL If continued Type r to resume execution or q to quit to top level Broken at SYSTEM TERMINAL INTERRUPT Type H for Help CHAOS gt gt The above session was obtained by typing the interrupt code usually Control C at the initial prompt forcing CafeOBJ to stop willy nilly The prompt CHAOS gt gt indicates you plunged into an error environment The above message may look familiar to you if you are a user of GCL The message was from GCL and the error environment is a GCL error loop Following the instructions from GCL you may resume the CafeOBJ session with q as 2 Error loops of CMU Allegro and MacLisp work more or less similarly and the same recover command q works 1 DIALOGUE WITH THE SYSTEM CHAOS gt gt q Cafe0BJ gt The message There may be irrecoverable cases when q or similar commands of other Common Lisp systems fails to work Then try cafeobj t This is a more robust means to return to CafeOBJ If for goodness you are unable to return to CafeOBJ even then exit GCL control D normally works and start from scratch If the system still works fine but if you happen to have destroyed some vital module definitions try CafeOBJ gt reset which restores the definitions of built in modules Chapter 11 and preludes Section 1 2 3 This command does not affect o
138. l_reset open close start parse cd quit period shell_call provide require ls compile compile_option eof save restore clean_memo dribble select lisp_call help autoload find match term_specifier match_pattern apply select check regularise 186 II II II II II II II II II II II II II II II II II li Vi li show describe set input check regularise save restore save_system protect unprotect clean_memo reset full_reset parse lisp _call select open close start apply match choose find provide require autoload eof prompt quit cd ls pwd help shell_call dribble period compile show help module contents switches describe help module contents set set_help set_switch set_other input file name protect module_name unprotect module name full reset full reset open module_expression close start term parse context term cd file name quit e e n qy shell command provide feature require feature file name 1s file name tram compile compile_option module_expression exec eof save file name restore file name clean memo dribble file name select module_expresion lisp lispq S_expression opn autoload proc name find rule rule rule match term specifier to match_pattern top term it subterm
139. le I am a language construct The definitions inside the box are by way of notations as follows are meta syntactical brackets separates alternatives means zero or more repetitions of the preceding construct means one or more repetitions x means zero or more repetitions separated by commas means one or more repetitions separated by commas enclose optional constructs The above symbols to appear as they are are enclosed by quotes as Symbols in the typewriter font appear as they are x is literally x In case this convention is ambiguous e g when a parenthesis appears in isolation symbols are quoted as in 8 For example A represents sequences of one or more A s separated by commas viii Dialogue with the System Availability You may obtain a complete distribution package from the following site http www 1dl jaist ac jp cafeobj system html The current version works under i386 Linux i386 MacOSX version 10 5 or later and win32 Binary package of these platforms can be obtained from the above site You can also download source code of the system from the same place 1 1 Hello Goodbye 1 1 1 Starting Up After installation type cafeobj to your shell to invoke the system Then the CafeOBJ in terpreter starts up producing a welcoming message 1 1 DIALOGUE WITH THE SYSTEM cafeobj loading standard prelude L
140. le eq not p Prop p Prop xor true p Prop gt a not a gt a xor true rule eq p Prop and q Prop xor r Prop p Prop and q Prop xor p Prop and r Prop p Prop gt b xor true q Prop gt true r Prop gt a b xor true and a xor true gt b xor true and true xor b xor true and a rule eq p Prop and true p Prop p Prop gt b xor true b xor true and true gt b xor true rule eq p Prop and q Prop xor r Prop p Prop and q Prop xor p Prop and r Prop p Prop gt a q Prop l gt true r Prop gt b b xor true and a gt a and true xor a and b rule eq p Prop and true p Prop p Prop gt a a and true gt a rule eq AC xor p Prop xor p Prop AC xor false AC gt true xor a xor a and b p Prop l gt true xor b b xor true xor a xor a and b xor b xor true xor true gt true xor a xor a and b xor false 1 gt 10 rule eq p Prop xor false p Prop p Prop gt a and b xor true xor a 1 lt 10 true xor a xor a and b xor false gt a and b xor true xor a 7 7 Further Example Propositional Calculus 1 gt 11 rule eq p Prop lt gt q Prop p Prop xor q Prop xor true p Prop gt a and b xor a xor true q Prop gt a and b xor true xor a 1 lt 11 a and b xor a xor true lt gt a and b xor true xor a gt a and b xor a xor true xor a and b xor true xor a xor true 1 gt 12 rule eq AC xor p Prop xor p Prop AC xor false AC gt t
141. le the last declarations above may be abbre viated to Nat Int lt Rat Nat lt Int It is also possible to combine sort and subsort declarations into a single bracket pair as Nat Int Rat Nat lt Int lt Rat which is equivalent to Nat Int Rat Nat lt Int lt Rat In subsort declarations if new sort names appear they are assumed to be declared implicitly If Nat Int and Rat have not been declared therefore Nat lt Int lt Rat and ul Nat Int Rat Nat lt Int lt Rat are interpreted identically Beware especially of mistyping upper lower cases For example if you imported a sort Nat and declared NAT lt Int NAT is regarded as a newly declared sort not an imported one It is abnormal for subsort relation to be circular and if they were circular you should not expect the system to behave correctly Subsort relation is set inclusion so circular relation means that all the sorts involved are the same But CafeOBJ does not recomment such indirect renaming and may refuse to support this interpretation Note that it is impossible to make a visible sort a subsort of a hidden sort or vice versa You cannot put a hidden sort in plain brackets nor a visible sort in asterisked brackets This impossibility reflects the fact that visible sorts are disjoint from hidden sorts 3 2 Operator Declaration In traditional algebraic specification languages an operator is a function i e
142. lements are too few nor a colossal sum N N N too many You want exactly the set 0 1 2 to be the model of your specification In the terminology of CafeOBJ such a module should be interpreted to have tight deno tation it has exactly one model the usual term model A module introduced with module is always so interpreted So perhaps it is more to your taste if we have written module SIMPLE NAT As another example of tight denotation consider indeterminate choice cf Section 4 3 of natural numbers 1 The current implementation imports a builtin sort of the same name so you need a lot of qualifications for this example to work correctly 57 5 INSPECTING MODULES module CHOICE NAT extending SIMPLE NAT op _ _ Nat Nat gt Nat vars N N Nat trans N N N trans N N gt N In the model you have in mind O s 0 may transit to 0 O s 0 may transit to s 0 but O s 0 should not transit to s s 0 module ensures that the last transition is not in the model To cope with transition rela tions the model must have a 2 categorical structure otherwise everything is a straight forward extension to usual algebraic semantics 5 2 2 Inspecting Transition Axioms When you declare a transition a couple of axioms are automatically generated Section 4 4 2 Let us use CHOICE NAT for illustration 2 In fact since Cafe OBJ does not distinguish transitions between
143. les X and Y X Y are allowed while s 0 s X Y X X 124 8 2 Parameters and Views are not A variable declaration is as in Section 4 1 like vars X Y Nat where sort names are those in the source module You may sometimes omit commas between view elements but it is safer always II to put them For a view declaration to define a specification morphism the maps must satisfy the condi tions for signature morphisms and the actual parameter must satisfy the translated axioms of the formal See 8 2 2 And we remark that e If operators are overloaded a single map determines a correspondence between all the overloaded operators at once e A view may be endomorphic and not necessarily be the identity mapping at that and e A view need not be onto nor one to one The system only checks syntactic conditions To check theory inclusion you II H need a powerful theorem prover which is lacking in the current system Equational theory attributes Section 7 1 act like axioms when views are con sidered associativity for example is an axiom that must hold in the actual parameter In the spirit of checking only syntactic conditions the system ig nores these attributes The system does not check every syntactic conditions 8 2 4 Views Galore We illustrate the definitions and remarks by several examples A first example maps MONOID to SIMPLE NAT Sections 5 2 3 and 2 2 view NAT AS MON
144. lose a term with such operator as top by parentheses for disambiguation 177 A SUMMARY OF CAFEOBJ SYNTAX A 1 3 Identifiers An ident identifier is a sequence of any printable ASCII characters other than self terminating characters period double quote The CafeOBJ reader is case sensitive and Nat and nat are different identifiers idents appear as module names view names parameter names sort names variables names slot names and labels A 1 4 Operator Symbols An operator_symbol is a sequence of any ASCII characters including non printables except EOT control D An underbar has a special meaning in an operator symbol It reserves the place where an argument is inserted A single underbar _ cannot be an operator symbol A 1 5 Comments A comment is a sequence of characters which begins with one of the following four character sequences PY gt Dix de gt and that ends with a newline character In between a comment may contain only printable ASCII characters and horizontal tabs Comments may act as separators but their appearance is restricted See the next section 178 A 2 CafeOBJ Syntax A 2 CafeOBJ Syntax We use an extended BNF grammar to define the syntax The general form of a production is nonterminal alternative alternative alternative The following extensions are used a alist of one or more as a alist of one or more as separated by
145. lp next go continue abort rule subst limit pattern rewrite stop A IES OrunHR MQ 900 B NY rwt rwt help next go continue abort rule subst limit pattern rewrite stop The command names are tentative and are subject to change 77 6 EVALUATING TERMS 6 3 2 Evaluation Under the Step Mode Continuing the session in the previous section we illustrate the effects of each command STEP 1 n gt gt stepper term s s s 0 s 0 s s s 0 STEP 2 n gt gt stepper term s s 0 s 0 s s s 0 STEP 3 n gt gt stepper term s 0 s 0 s s s 0 STEP 4 n prints a kind of traces but beware that the printed term is a subterm under replace ment You may print the current form of the entire term as STEP 4 show term s s s 0 s 0 s s s 0 NzNat STEP 4 Or you may get a better if longer trace if that is what you want by setting trace whole to on Starting from the first step the output is MULT gt set trace whole on MULT gt reduce s s 0 s s s 0 reduce in MULT s s 0 s s s 0 gt gt stepper term s s 0 s s s 0 STEP 1 n 1 s s 0 s s s 0 gt s s s 0 s 0 s s s 0 gt gt stepper term s s s 0 s 0 s s s 0 STEP 2 n 2 s s s 0 s 0 s s s 0 gt s s s 0 s 0 s s s 0 gt gt stepper term s s 0 s 0 s s s 0
146. lt AttrId Slotday Slotday lt AttrId DATE gt SIMPLE NAT Section 2 2 should be familiar The record Date was indeed declared as a sort as we stated But it seems that a lot more sorts are involved They are used to define the operators To see what operators were declared you may inspect further But hold your breath 55 5 INSPECTING MODULES DATE gt show ops rank RecordDate gt Date attributes constr rank RecordDate Attributes gt Date attributes constr O O TROL OEP EOT Date heer tate eee eer ener meee RA rank gt RecordDate attributes constr ee ORE STU seater eo RRL Set A makeDate ee a aa iene went A en see eh eee rank Attributes gt Date axioms eq makeDate ATTRS 6 Attributes make record instance date attrs 6 RE ETE makeDate se feat sevens aletas OA E A TEN rank gt Date axioms eq makeDate make record instance date rank gt Slotyear attributes constr rank Date gt Nat axioms eq year RID 5 RecordDate VAR SLOTYEAR 2 Slotyear VAL 11 Nat ATTRS 6 Attributes VAL 11 Nat Pores O eae cL eg NTN gees EAS a Cota oct Olea rank Date Nat gt Date axioms eq set year RID 5 RecordDate VAR SLOTYEAR 2 Slotyear VAL 11 Nat ATTRS 6 Attributes NEW VAL 12 RID 5 RecordDate VAR SLOTYEAR 2 Slotyear NEW VAL 12 ATTRS 6 Attributes The print continues for month set month and so on We do no
147. m to be a rewrite rule 1 Every variable that occurs in the righthand side or in the condition must occur in the lefthand side also Otherwise the terms under computation may become non ground 2 The lefthand side must not be a single variable Otherwise every term of a relevant sort is matchable so the computation never stops 64 6 2 Do the Evaluation For order sorted TRS there might be other constraints such as sort decreasing property But CafeOBJ does not impose such a constraint There are two important properties of TRSs If computation always terminates the TRS is said to be terminating If whenever a term is rewritten to two different terms they can be further rewritten to a same term the TRS is said to be confluent If terminating and confluent it is canonical In general the declarative meaning of an axiom set differs from the operational one i e TRS But there is a coincidence if we restrict ourselves to tight denotation and equations If the set regarded as TRS is canonical i e terminating and confluent Two ground terms are equal iff they are reducible to a common term For this reason it is important to distinguish a subset of a TRS derived only from equations cf reduce command in Section 6 2 1 It also follows that for loose denotation reduction per se does not suggest anything of much import For theorem proving it is useful see Section 10 2 6 2 Do the Evaluation 6 2 1 Evaluat
148. m selected by choose commands it is the same as subterm if choose was used and is the same as top otherwise Unlike former versions the current version do not require enclosing parentheses i S for a term If you are cautious put them anyway They are harmless pattern all rules rules rules term where a term is a usual term rules rules or rules lists rewrite rules applicable to the specified term rules means the rules with matching lefthand sides rules means those with matching righthand sides and rules means both If optional all is given all the rules in the current context including those declared in built in modules are inspected If a pattern is a term matching is attempted and if successful the matching subsitution is printed Is a pattern is rules rules or rules the list of applicable rules together with corresponding matching substutitions are printed 9 3 2 Matching Terms to Terms We use GROUP Section 9 2 for examples 157 9 THEOREM PROVING TOOLS CafeOBJ gt select GROUP GROUP gt match O 0 to X G 0 match success substitution X gt 0 No more match GROUP gt match 0 O to X G Y G match success substitution X gt 0 Y G gt 0 No more match GROUP gt match 0 toO 0 no match GROUP gt As shown above the system prints the substitution when matching succeeds The system recognis
149. me of A and that of C and is ambiguous in C You may refer to X of A by X A The plain X in C refers to X of C This means that a sort or operator name may be qualified by a parameter name which itself is qualified by a module name Since a term may be qualified by a sort name also see Section 3 3 2 a chain of qualifications such as a S P M n is possible If there is any ambiguity qualifier is considered right associative 8 4 Module Expression Syntactically an instantiation of parameterised modules is an expression involving module names There are other kinds of such expressions Expressions over module names are called module expressions A module expression represents a module and may appear in import declarations or in several commands Here we summarise the syntax of module expressions 8 4 1 Module Name The simplest module expressions are module names Syntax 66 module constant module name A module represented by a module name is the module itself 8 4 2 Renaming Renaming is to change sort or operator names creating a new module Syntax 67 renaming module_expression map x where a map is 137 8 MODULE STRUCTURE map sort sort_name gt sort_name hsort sort_name gt sort_name op operator_name gt operator_name bop operator_name gt operator_name Maps are as expected sort maps visible sor
150. ment protecting extending including using module_expr visible_sort hidden_sort P sort_decl J T sort_decl sort_name supersorts lt sort_name sort_symbol qualifier ident un module_expr qualifier record sort_name super slot comment P sort name slot rename J slot name sort_name slot name term sort mame ident slot_name gt slot_name op bop operator_symbol sort name sort_name P op_attr P constr associative commutative idempotent id idr term arity gt coarity op_attrs strat natural prec natural assoc r assoc coherent var var_name sortname vars var_name sort_name ident equation cequation transition ctransition eq beq label term term ceq bceq label term term if term trans btrans Y label term gt term ctrans bctrans label term gt term if term P ident A 2 CafeOBJ Syntax A 2 3 Module Expression A module_expr is module_expr module_name sum rename instantiation module_expr sum module_expr module_expr rename module_expr rename_map y instantiation module_expr ident quali fier lt aview rename_ma
151. more than one rules match with more than one subterms so the above procedure is in fact hardly a procedure at all Which one to choose and when is a significant issue CafeOBJ allows you to control the selection operator by operator See Section 7 4 6 1 2 How a Module Defines a TRS The axioms of CafeOBJ are equations and transitions which define equivalence and transi tion relations In operational semantics these axioms are regarded uniformly as directed rewrite rules as follows If we denote a rewrite rule by t gt t for relevant terms t t and b eq t t isa rewrite rule t gt t ceq t t if b is a rewrite rule t gt t with the condition b trans t gt t is a rewrite rule t gt t ctrans t gt t if b is a rewrite rule t gt t with the condition b Behavioural axioms are translated similarly Then the TRS defined by a module is the set of axioms regarded as rewrite rules as above Note that the axioms of the imported modules are included in this definition For example SIMPLE NAT Section 2 2 defines a TRS that contains two rewrite rules O N gt N s N N gt s N N where N N are variables of sort Nat Since BOOL is implicitly imported its axioms as rewrite rules are also in this TRS show command may be used to list all the rules see examples in Section 6 2 2 Two kinds of axioms are excluded from TRS s solely by syntactic criteria For an axio
152. nal theory attribute which defines an equivalence relation among terms 2 a parsing attribute which specifies connectivity 3 an evaluation attribute which controls the evaluation procedure or 4 neither of these Operator declarations introduced by ops bop bops pred may also have this optional construct 7 1 Equational Theory Attribute CafeOBJ admits four equational theory attributes as follows For an infix operator 1 Associativity or x y 2 x y z for any x y and z Specified with associative or assoc 2 Commutativity or x y y for any z and y Specified with commutative or comm 95 7 OPERATOR ATTRIBUTES 3 Idempotency or x x x for any z Specified with idempotent or idem 4 Existence of the identity here written 0 or 0 xz x and z 0 z for any z Specified with id 0 7 1 1 Associativity oe We proceed to a couple of examples for futher illustration The conjunction _and_ is associative In CafeOBJ it is written as op _and_ Bool Bool gt Bool assoc which means No ambiguity arises with or without parentheses For example true and false and true has two parses true and false and true true and false and true but by associativity they are equal During evaluation terms are matched modulo associativity For example in evaluat ing true and false and true in the presence of eq true and X Bool X the given term
153. ncluding module_expression protecting etc are called importation modes and indicate how to import the designated module You may abbreviate the modes to pr ex inc and us respectively A module expression is a designation of a module and is explained later Section 8 4 For the current purpose it is enough to know that an individual module name is by itself a module expression To illustrate the meaning of import declarations here is a contrived example 18 2 5 Import Declaration module BARE NAT Nat op 0 gt Nat op s Nat gt Nat F module BARE NAT AGAIN protecting BARE NAT The declaration of BARE NAT AGAIN is equivalent to module BARE NAT AGAIN Nat op 0 gt Nat op s Nat gt Nat i e it is a copy a sad shadow of BARE NAT Only the name is changed To explain the precise meaning of importation modes we have to delve into a model theoretic theatre which is situated outside of this manual So let us offer only a cursory glance here The modes state to what extent the intended models of the imported modules are preserved within those of the importing modules Intuitively when M is imported protecting is the strongest commandment This mode requires all the intended models of M be preserved as they are extending allows the models of M to be inflated but does not allow them to be collapsed including does not introduce any rest
154. nguish transitions and equations during evaluation and acts faithfully only when certain conditions are satisfied For detail see 12 6 2 4 Using Behavioural Equations As a matter of course behavioural equations can be used to prove behavioural equivalence With judicious use they can also be used to prove equality Consider the following example 69 6 EVALUATING TERMS module NAT STREAM protecting SIMPLE NAT Stream bop __ Nat Stream gt Stream bop hd Stream gt Nat bop tl Stream gt Stream op zeros gt Stream var N Nat var S Stream eq hd N S N beq t1 N S S eq hd zeros 0 beq tl zeros zeros A behavioural equation asserts that t1 n s is behaviourally equivalent to s for any n and s but does not assert that they are equal Therefore on the one hand it is incorrect to reason that t1 s 0 zeros equals zeros from this axiom On the other hand it is correct to reason that hd t1 s 0 zeros is equal to hd zeros and hence to 0 since hd being an observation on Stream gives the same answer if applied to behaviourally equivalent terms In processing reduce the system tries to apply behavioural equations as rewrite rules only when the redex is under an observation as shown below CafeOBJ gt select NAT STREAM NAT STREAM gt reduce hd t1 s 0 zeros reduce in NAT STREAM hd tl s 0 zeros O Zero 0 010 sec for parse 2 rewrites 0 000 sec 3 matches NAT STRE
155. ns 21 home directory 5 abort 77 all 152 157 apply 146 associative 95 assoc 95 96 100 at 147 auto 115 117 axioms 15 axs 15 a 77 if regularize bceg 41 bcq 41 bctrans 42 bctrns 42 beg 41 binding 86 bops 26 bop 26 124 137 bpred 27 breduce 65 btrans 42 btrns 42 cd 5 ceq 41 check 161 choose 149 clean memo 104 close 141 commutative 95 comm 95 97 compatibility 161 compile 84 conditions 155 constr 101 context 115 116 151 154 continue 77 cq 41 ctrans 42 ctrns 42 Gat depth 87 describe 12 eof 4 eq 39 execute 65 83 exec 146 167 169 extending 19 from 124 go 77 g 77 help 77 hsort 124 137 h 77 id 96 97 idempotent 96 idem 96 98 idr 98 113 190 if 41 imports 14 include 44 include BOOL 19 including 19 input 4 in 4 it 157 l assoc 99 100 laziness 161 let 85 86 limit 77 82 83 169 ls 5 1 77 make 139 match 157 memo 104 105 module 13 120 next 77 n 77 off 10 of 147 on 10 open 141 ops 25 op 24 95 124 137 p sort 130 param 137 parse 30 pattern 77 80 prec 99 pred 27 principal sort 129 print 87 146 prompt 117 protecting 19 protect 14 provide 8 pwd 5 p 77 q 77 r assoc 99 100 reconstruct 117 record 34 35 reduce 65 83 146 155 regularity 161 regularize 28 arity equational theory attribute require
156. o 1 and the rest of the current strategy is discarded Note also that when a negative integer appears the corresponding argument is just marked and nothing else is done The mark reveals its effects only during matching 7 5 Memo To evaluate similar terms repetitively is tedious to humans but acceptable to the system To evaluate the same terms repetitively however is sometimes too much even to the system It silently complains by taking long time in responding For the sake of efficiency it helps if you state in advance that such and such evaluations are likely to occur quite often and that remembering the previous results is a good idea Hence an attribute called memo This operator attribute tells the system to remember the results of evaluation where the operator appeared More specifically if you declare op f k SS S gt S memo and evaluate a term containing f k t1 t2 t3 the system take note of 1 f k t1 t2 t3 itself 2 f k r1 r2 r3 where ri s are the results of evaluating ti s and 3 the result of evaluating 1 If the need arises to evaluate 1 again the system gets the result 3 immediately This mechanism not only speeds up the computation it also saves memory space when you evaluate terms that contain common subterms The memo attribute can only specified on functions i e operators not defined by rules See for rules The system does or does not remember the evaluation results after each e
157. o ways to specify lazy evaluation a Omit the arguments to be evaluated later or b Put the corresponding negative integers Delayed cons is thus declared as either op cons Sexp Sexp gt Sexp strat 0 a or op cons Sexp Sexp gt Sexpt strat 1 2 b With the former declaration both arguments are not evaluated unless they get outside of cons For example suppose car is defined as op car Sexp gt Sexp strat 1 0 vars X Y Sexp eq car cons X Y X and you try to reduce the term car cons 1 0 nil where nil is the usual constant According to the given E strategies 1 The argument of car is to be evaluated first 2 But the argument is dominated by cons whose arguments are not to be evaluated since 1 2 are not in the E strategy So cons 1 0 nil is returned as it is 3 The evaluation for car continues and the next argument in the E strategy in fact 0 the whole term is to be evaluated 4 Using the equation marked the whole term is rewritten to 1 0 5 Evaluation continues with this term With the declaration b both arguments are not evaluated until so forced Evaluation is forced when the argument is involved in matching For example to see the applicability of the equation rewrite rule eq cadr cons X cons Y Z Y it is necessary to know whether the second argument of the outer cons is dominated by cons Suppose a term has be
158. oading usr local cafeobj 1 4 prelude std bin Cafe0BJ system Version 1 4 8 PigNose0 99 p18 built 2010 Jul 5 Mon 0 50 01 GMT prelude file std bin Hook 2010 Jul 5 Mon 6 59 56 GMT Type for help Hook Containing PigNose Extensions built on International Allegro CL Enterprise Edition 8 2 Mac OS X Intel Jul 5 2010 9 49 Cafe0BJ gt For a moment ignore the message cafeobj gt is a prompt for your requests You may type modules views parsing instructions reduction commands and so on each of which shall be gradually introduced in the rest of the manual As a first experiment try feeding a trivial module definition you need not worry about the meaning for now module TEST Elt defining module TEST processing input usr local cafeobj 1 4 lib bool mod processing input usr local cafeobj 1 4 1ib truth mod defining module TRUTH reading in file truth done reading in file truth ccx imiag modulo lbeccoooooococooosoosconoocnpocccnooooos done _ done Cafe0BJ gt Your input is up to the first newline character The rest is from the system It shows that the system has accepted the definition put this module somewhere in its memory to be available hereafter You may continue to feed other modules or check if indeed the module is correctly stored As a further trial type CafeOBJ gt select TEST TEST gt The command select takes as argument a module name TEST gt
159. odule the system complains it has no way to know whither the term came By the way you encountered not so small a term when a2 was reduced It is very simple for the system to print such terms accurately they may sometimes cause you nausea or headache If you expect the terms to be large and need to see only their broad outline you can use a switch Cafe0BJ gt set print depth 10 tells the system to print terms up to the depth 10 as trees The default is unlimited and the depth of is interpreted as such Continuing the above session then you get 87 6 EVALUATING TERMS MULT gt set print depth 10 MULT gt reduce a2 reduce in MULT s s s 0 s 0 s s 0 s s s 0 s s s s s 0 s s s s s s s s s s NzNat 0 000 sec for parse 145 rewrites 0 010 sec 277 matches MULT gt set print depth MULT gt reduce a2 reduce in MULT s s s 0 s 0 s s 0 s s s 0 s s s s s 0 s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s 0 NzNat 0 000 sec for parse 145 rewrites 0 010 sec 277 matches MULT gt 6 6 Flexible Typing and Error Handling CafeOBJ
160. ome of the authors feel that some of these technical terms are queer But to avoid confusion we basically keep to the established terminology vil INTRODUCTION are naturally formalised by those relations In particular transition relations are useful to represent concurrency and or indeterminacy Hidden sorts 7 You have two kinds of equivalence One is a minimal equivalence that identifies terms elements iff they are the same under the given equational theory Another equivalence employed for so called hidden sorts is behavioural two terms are equivalent iff they behave identically under the given set of observations We would also like to emphasise a very useful feature of CafeOBJ Parameters There are many sorts that are inherently generic Stacks lists sets and so on have operations that act independently of the properties of base data elements A more tricky case is priority queues which require base elements to have an order relation You may define these sorts by parameterised modules where base elements are parameterised out A parameter may be subject to constraints For example the parameter of a priority queue module may be declared an ordered set not an arbitrary set Legends Restrictions particulars and prejudices of the current implementation shall be highlighted by preceding as Woe betide those who do not heed this warning while syntactical definitions are shown as Syntax 1 tit
161. on is a new module obtained by replacing occurrences of parameter sorts and operators by actuals If as a result of instantiation a module is imported twice it is assumed to be imported once and shared throughout Section 8 1 2 5 You may buy out Monaco but it is another matter 130 8 3 Binding Parameters Syntactically instantiation binds a view to a parameter Syntax 65 instantiating parameterised module module_name C binding 9 There are two distinct kinds of binding constructs Instantiation by Declared Views You may bind an already declared view to a param eter binding parameter_name lt view_name If a module M has a parameter X T and a view V from T to M is declared V may be bound to X with the effect that 1 The sort and operator names of T that appear in the body of M are replaced by those in M in accordance with V and 2 The common submodules of M and M are shared Instantiation by Ephemeral Views It is possible to declare and bind a view simulta neously bindin arameter_name lt view g p view view to module_name view_element x y where F encloses the same constructs as in view declarations The view is valid only within the instantiation For example module NAT ILIST 4 protecting ILIST IDX lt view to SIMPLE NAT sort Elt gt Nat DAT lt view to SIMPLE NAT 4 sort Elt gt Nat
162. ons about convenience and tolerable performance dictate otherwise Some frequently used data types are defined in built in modules In addition the system relies on a couple of kernel modules which are located near its jugular A few commands such reset Section 1 1 are closely related to these modules Listed below are the kernels and built ins As explained in Section 1 2 3 you may supply your own built ins or even override the standard built ins Systems Some modules are vital to the behaviour of the system Unless you are ready to help us tune the system they need not concern you Booleans The module BOOL and the sort Bool have appeared frequently Actually Bool is declared in a submodule imported by BOOL And RWL is a module that declares transition predicate _ gt _ Numbers The system supports usual arithmetics within a usual number system The modules involved are NAT INT RAT and FLOAT Strings QID quoted identifier CHARACTER STRING define operations on characters and strings Pairs A simple pair triple and quadruple are defined in 2TUPLE 3TUPLE and 4TUPLE Miscellaneous For historical reasons PROPC Section 7 7 TRIV Section 8 2 1 are built in modules There are also a set of library modules and examples in the distribution package Elements in built in sorts are defined as corresponding Lisp objects and the 7 system may compute them by stealth For example an expression 2 1e1 is an element of
163. onsist of years months and days Sloppy because it admits e g 554 32 1984 as a date In ordinary programming languages once a record is declared notation functions to access fields are automatically determined The dotted notation d day where d is a record variable and day is a field name is typical CafeOBJ also provides access functions In fact a record is nothing more than a special sort The effects of a record declaration are as follows e A sort with the record name is declared A record is a sort so the name can appear wherever a sort name can e A mixfix operator is declared so that a term of the form record name slot namel valuei slot name2 value2 is an element of record name Using the above example Date year 1984 month 1 day 1 is a term of sort Date Moreover the slot value pairs in the braces may be written in whatever order and you may even omit some of them Thus Date month 1 day 1 year 1984 Date year 1984 are well formed terms of sort Date Note that Date in these terms is part of an operator symbol not the sort name which happens to be the same character string e For each slot two access functions are declared and defined In case of Date it is as if the declarations op year Date gt Nat op set year Date Nat gt Date similarly for month and day 34 3 4 Record Declaration are given Accordingly to get the value of year slot from a term d of
164. ontents of prelude files see Section 1 2 3 as well as module 4 definitions given during the session restore reestablishes those definitions as they are saved and the effects may be different from reading the file with input command It is safer to use restore command to read saved files 3The older systems prior to version 1 4 8 used a diffrenct suffix compatibility mod This is also supported for 1 DIALOGUE WITH THE SYSTEM You can also save the entire image of the system including the state of module definitions into a dump file by the following command Syntax save system command save system pathname save system dumps the image of Common Lisp so do not abuse this command And due to the restictions of Common Lisp systems this command may not work 1 2 3 Initialisations and Options Recall Section 1 1 that the initial system message contained loading standard prelude Loading mnt1 lang cafeobj 1 4 prelude std bin In starting up CafeOBJ autoloads a set of modules called standard preludes They define frequently used data types and house keeping data cf Chapter 11 You may initialise the system to your taste with options and initialisation files If a file named cafeobj is under your home directory the system reads the file as if you type Cafe0BJ gt in cafeobj after the startup This initialisation is useful to change default values of modes and switch
165. opening module W COUNTER_ done 7W COUNTER gt ops mn p gt Nat W COUNTER gt op c gt Counter W COUNTER gt op addn Counter gt Counter W COUNTER gt reduce read add m n c gt read add m c Ex reduce in read add m n c gt read add m c true Bool 0 010 sec for parse 6 rewrites 0 010 sec 32 matches W COUNTER gt trans read addn add m n c gt read addn add m c W COUNTER gt reduce read add p addn add m n c gt read add p addn add m c reduce in read add p addn add m n c gt read add p addn add m c true Bool 0 000 sec for parse 4 rewrites 0 000 sec 11 matches W COUNTER gt close Cafe0BJ gt The command sequence is quite similar to the one in the previous section Or relying on x you may be rest assured by just one reduction 173 10 PROVING MODULE PROPERTIES W COUNTER gt reduce read add m n c gt read add m c which by itself is a proof by coinduction A difference from the case of behavioural equiv alence is that the system does not suppy an axiom like eq hs1 Counter hs2 Counter read hs1 Counter read hs2 Counter so you have to be satisfied by handfeed reduction commands for each attribute 174 Built in Modules You may define any data types in CafeOBJ so in principle the need for built in data types does not arise So is the principle but considerati
166. options someoptionsoftram makes the system supply someoptionsoftram as options whenever tram is invoked In normal usage you need not know which options tram or brute takes 6 5 Context Variable To help ease reading and writing terms a context variable facility is supported Syntaz 55 let command let identifier term The last period preceded by a blank is a must An identifier is a character string and a term is a term in the current context Section sec p2 current module This command binds the given term to the identifier in the current context The example below illustrates the usage and shows how to print the binding state 85 6 EVALUATING TERMS MULT gt let al s 0 s s 0 s s s 0 setting let variable ai to s 0 s s 0 s s s 0 Nat MULT gt let a2 s s s 0 al s s s s s 0 setting let variable a2 to s s s 0 s 0 s s 0 s s s 0 s s s s s 0 Nat MULT gt reduce al reduce in MULT s 0 s s 0 s s s 0 s s s s s s 0 NzNat 0 000 sec for parse 5 rewrites 0 010 sec 8 matches MULT gt reduce a2 reduce in MULT s s s 0 s 0 s s 0 s s s 0 s s s s s 0 s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s
167. ory attribute 95 191 normal term standard operator declaration error sort 89 evaluation 63 evaluation strategy 101 G ground term 63 hidden sort 21 homomorphism 121 I idempotency 96 identity 96 import declaration 18 importation of views 130 importation mode 18 inductive property 165 initialisation file 6 instantiation 130 instantiation of a term 63 irreducible term 63 K kernel module 175 L laziness 163 least sort 27 left associativity 99 loose denotation 16 M matching 63 method 26 mixfix operator declaration 24 module 13 module element 13 module expression 137 module name 13 module sum 138 modulo equatioanl theory 96 192 normal term 63 observation 60 operator 23 operator attribute 95 option for startup 6 P parameter 120 parsing attribute 95 partial operator 90 partial order over sorts 22 precedence 99 predicate 26 prelude 6 principal sort 129 Q qualified term 32 rank 24 record declaration 33 record inheritance 35 reduction 63 regular 161 regular signature 27 renaming 137 right associativity 99 S shared sum 138 signature 14 21 signature morphism 123 slot 33 sort 21 specification morphism 123 stack 90 standard library 8 standard operator declaration 24 well formed term well formed term standard prelude file 6 standard preludes 6 step mo
168. ot make sense to retrieve attributes from two objects And it is nonsense to talk about attributes of nothing Technically behavioural operators and only them make behavioural contexts see Section 5 2 4 There is a counterpart to ops with which you may declare several behavioural operators at once Two of the above declarations may be replaced by bops deposit withdraw Account Nat gt Account Note that an operator symbol may be overloaded among behavioural operators and or among the mixture of usual and behavioural operators Note further that a non behavioural operator declaration with op is not required to contain or not to contain hidden sorts You may declare non behavioural operators on hidden sorts as op deposit Account Nat gt Account The effects are however very different Do take care 3 2 3 Predicate Declaration A predicate in CafeOBJ is nothing more than an operator which has a special sort Bool as its coarity This sort is contained in the module BOOL which is imported everywhere 26 3 3 Terms Section 2 5 Bool is important in several respects and is accorded a privilege by the following shorthand constructs Syntar 32 predicate declaration pred standard_operator_symbol list_of_sort_names pred mizfiz_operator_symbol list_of_sort_names Operator symbols etc are as in operator declarations Predicate declarations are equivalent to operator declarations with coari
169. p sort_map op map sort_map sort hsort sort_name gt ident op map op bop op_name gt operaotr_symbol op_name operator_symbol operator_symbol qualifier aview view_name module_expr view to module_expr view_elt view name ident view elt sort_map op view variable op_view op_map term gt term When a module expression is not fully parenthesized the proper nesting of subexpressions may be ambiguous The following precedence rule is used to resolve such ambiguity sum lt rename lt instantiation A 2 4 Views and a view is view view view_name from module_expr to module_expr E view_elt rs sea A 2 5 Evaluation Commands and an eval is un eval reduce behavioural reduce execute context term context in module_expr The interpreter has a notion of current module which is specified by a module_expr and establishes a context If it is set context can be omitted A 2 6 Terms A term is a sequence of any ASCII characters except EOT 181 A SUMMARY OF CAFEOBJ SYNTAX A 2 7 Sugars and Abbreviations Module type There are following abbreviations for module_type Keyword Abbriviation module mod module mod module mod Module Declaration make is a short hand for declaring module of name module_name which imports module_expr with protecting mode make make module_name module expr make FOO BAR
170. pected results of evaluations For example if you are excessively uneasy about what is going on you may prepare a file that contains gt immediately above TEST module TEST gt just entered into TEST gt now sort declaration Elt this comment should be supressed gt sort declaration ended gt operator declaration starts op a gt Elt this comment should be supressed gt operator declaration ended gt finishing TEST declarartion F gt finished and feed the file call it test here to the system The result is as follows 17 2 MODULE DECLARATION CafeOBJ gt in test processing input test cafe gt immediately above TEST defining module TEST just entered into TEST now sort declaration sort declaration ended operator declaration starts operator declaration ended finishing TEST declarartion _ done gt finished Cafe0BJ gt As shown above gt is stripped when the comment appeared within a module declaration As an aside you may have noticed a couple of s in the system messages These dots 6 99 indicate that the system is running hard More dots mean more labour _ and just before done were also from the system 2 5 Import Declaration An import declaration is sic to import declarations from another module Syntax 25 import declaration protecting extending using i
171. perators and indicates a subterm in a multiset structure For example if _ _ was declared associative and commutative and given a term b c d e f both 2 4 and 4 2 means a subterm c x e while 4 means e Note that the above selections are indeed subterms If _ _ is associative the connectivity is immaterial in whatever way the term was originally given If it is commutative in addition even the order is immaterial top is obsolete and is here only for historical curiosity 9 2 2 Applying Apply Command apply command has a very complicated syntax It is better to explain its behaviours by examples We use the group theory presented at the start of this section 6 To show X is a right inverse you may use the following sequence of commands 147 9 THEOREM PROVING TOOLS open GROUP opa gt G start a a apply 1 at 1 apply 2 with X a at 1 apply reduce at term The numbers of rewrite rules are printed by show command See Section 9 2 4 After two applications of reversed rules reduction yields the desired result as follows NAT gt open GROUP opening module GROUP done GROUP gt op a gt G GROUP gt start a a GROUP gt apply 1 at 1 result 0 a t a G GROUP gt apply 2 with X a at 1 meets E Porat atra a 2 amp GROUP gt apply reduce at term result 0 G GROUP gt Look in more
172. ping and Error Handling Unlike the former versions the current version admits error sorts such as Nat in operator declarations Since names of error sorts in fact their existence at all are implementation dependent you should avoid mentioning error sorts unless absolutely necessary 93 Operator Attributes Some properties of operators such as associativity can be stated as axioms but if they are so common it is convenient to be able to use shorthand notations Moreover some properties such as commutativity are better not to be given by axioms since if regarded as rewrite rules such axioms violate desirable properties of the TRS CafeOBJ has a construct for endowing operators with common properties Such properties are called operator attributes Some of them affect denotational semantics others affect only parsing yet others concern solely with evaluation Operator attributes are specified with an optional construct of operator declarations that were explained in Section 3 2 Syntaz 56 operator declaration with attributes op operator_symbol list_of_sort_names gt sort_name attribute_list where operator symbols et al are as before Section 3 2 We delayed the introduction of this construct since it is better explained after evaluation commands An attribute list is a list of operator attributes separated by blanks An attribute is either 1 an equatio
173. put from the system has three parts showing the system s understanding of what to do the line starting with the result of evaluation the second line and what looks like statistics in parentheses The result is of the form term sort where sort is the least sort Section 3 3 1 of term You may print the rules of SIMPLE NAT as follows SIMPLE NAT gt show rules rewrite rules in module SIMPLE NAT 1 2 eq eq O N N s N N s N N SIMPLE NAT gt Note that all the axioms of the implicitly imported BOOL are also in the TRS but were not printed above It is possible to print all the rules including those declared in the imported modules by an extra argument to show SIMPLE NAT gt show all rules rewrite rules in module SIMPLE NAT 1 OMAN ODO ARUN PPP rRP PRP RB NOoonP WN RF OO 18 19 20 8 21 22 eq eq eq eq eq eq eq eq eq eq eq eq eq eq eq eq eq eq eq cel eq eq Oo N N s N N s N N not true false not false true false and A Bool false true or A Bool true true and also A Bool A Bool A Bool and also true A Bool false and also A Bool false A Bool and also false false true or else A Bool true A Bool or else true true false or else A Bool A Bool A Bool or else false A Bool A Bool implies B Bool not A Bool or B Bool true xor true false CXU Id SortId coerce to
174. quent requirements of a feature are assumed to have been fulfilled already For example you may be at the point of reading a file that refers to a module of lists Suppose your convention is to store a set of container modules lists bags sets and so on in a single file Suppose further that for various reasons you have a couple of alternative definitions of those modules stored in files container 1 cafe container 2 cafe etc Then it is convenient to insert the command provide container 1 3 Some Helpful Commands in each file so that once one of them read in the system knows that a module of lists is already supplied To see which features have been provided type CafeOBJ gt show features see Section 1 3 3 for show command To continue the above example provided there is a file container 1 mod that defines lists bags et al and contains the provide command line as above you may get the following session Cafe0BJ gt provide numbers Cafe0BJ gt require container container 1 processing input container 1 cafe defining module LIST_ done defining module BAG_ done defining module SET_ done CafeOBJ gt require container container 1 Cafe0BJ gt show features container numbers The first invocation of require made the system read the file while the second invocation caused nothing Also since numbers was explicitly provided the system presumes the feature as given 1 3 Some Helpful
175. reduce is to get a term equal be haviourally equivalent to the input while execute is to get a term that the input may eventually transit to The point 2 comes from the fact that breduce is to get a term behaviourally equivalent to the input while reduce is to get a term equal to the input These points are illustated in Sections 6 2 3 and 6 2 4 During evaluation it is sometimes desirable to see the rewrite sequences not just the results For example to enhance efficiency you may want to know where redundant computations of subterms occur For this purpose CafeOBJ provides trace switches which can be set by CafeOBJ gt set trace whole on by which the resultant term of each rewrite step is printed or CafeOBJ gt set trace on by which the rule substitution and replacement are printed The effects of these switches shall be illustrated by examples below 6 2 2 Replacing Equals by Equals Recall SIMPLE NAT Section 2 2 again make it current and do some evaluations SIMPLE NAT gt reduce O reduce in SIMPLE NAT 0 O Zero 0 000 sec for parse 0 rewrites 0 000 sec O matches SIMPLE NAT gt reduce O s 0 reduce in SIMPLE NAT 0 s 0 s 0 NzNat 0 000 sec for parse 1 rewrites 0 000 sec 1 matches SIMPLE NAT gt reduce s 0 0 reduce in SIMPLE NAT s 0 0 s 0 NzNat 0 010 sec for parse 2 rewrites 0 000 sec 3 matches SIMPLE NAT gt 66 6 2 Do the Evaluation The out
176. rictions using simlilar to including allows total destruction To prove model theoretic properties is very hard and the system does not check 1 whether indeed these restrictions are observed It is on the user to choose correct modes As a special case a couple of built in modules are implicitly imported with protecting mode In particular BOOL is of practical importance It defines Boolean operators It is imported to admit conditional axioms You may prohibit implicit importation by set command as Cafe0BJ gt set include BOOL off but be careful Boolean operators are indispensable to write conditional axioms Section 4 2 2 and an attempt to use them will cause errors if BOOL is not imported Import declarations define a module hierarchy We shall probe it later Chapter 8 19 Signature A signature decides what is and is not a well formed term see Section 3 3 1 for detail A very basic definition would tell you that it consists of sort name s and operator symbol s paired with ranks A signature for CafeOBJ is more elaborate As briefly stated in the introductory chapter e The set of sorts may be partially ordered under inclusion and e There are two distinct kinds of sorts with different concepts of equivalences These complications are reflected in the syntactic elements in several ways 3 1 Sort Declaration A sort is a set of classified elements such as a set of designers of supermodels and of politic
177. rlier BOOL defines Boolean operators and is imported unless prohibited by a switch Section 2 5 e There is a bracketed text after the declaration of _ _ to be explained later Section 7 This is an operator attribute Display of sort declarations is often knotted This is due to implementation i restriction an optimal display is very hard to define anyway 5 1 2 Print Part of Modules To print partial contents such as sort declarations only of a module you may supply further arguments to show command Continuing the above session you get 50 5 1 Using Inspection Commands CafeOBJ gt show sorts SIMPLE NAT visible sorts Zero Zero lt Nat NzNat NzNat lt Nat Nat Zero NzNat lt Nat Cafe0BJ gt show ops SIMPLE NAT A AN AE Race Ce its oN Peete pe eam O Oe Gans aaa Ceo OR rank gt Zero E E EA CUA E E E ARA E oO tors ea O ER rank Nat gt NzNat SER Sess Ree TER E S ey ONS CREAT E rare Cees RS o See ae ko rank Nat Nat gt Nat strat 1 0 2 axioms eqO N N eq s N N s N N Cafe0BJ gt The arguments sorts ops etc specify the parts of the module to be shown To summarise the mostly obvious sorts sort and subsort declarations ops operator declarations vars variable declarations axioms axiom declarations params parameter declarations to be introduced later subs import declarations for sub modules sign sorts and ops combined
178. rue p Prop gt true xor a and b xor a 1 lt 12 a and b xor a xor true xor a and b xor true xor a xor true gt true xor false 1 gt 13 rule eq p Prop xor false p Prop p Prop gt true 1 lt 13 true xor false gt true true Bool 0 000 sec for parse 13 rewrites 0 140 sec 75 matches PROPC gt Observe that associativity and commutativity are frequently used To trace everything makes the exposition rather long so we omit traces in the sequel PROPC gt set trace off PROPC gt reduce not a or b lt gt not a and not b reduce in PROPC not a or b lt gt not a and not b true Bool 0 000 sec for parse 11 rewrites 0 020 sec 70 matches PROPC gt reduce c or c and d lt gt c reduce in PROPC c or c and d lt gt c true Bool 0 000 sec for parse 7 rewrites 0 190 sec 34 matches PROPC gt reduce a lt gt not c reduce in PROPC a lt gt not c a xor c Prop 0 000 sec for parse 4 rewrites 0 010 sec 15 matches PROPC gt reduce a and b xor c xor b anda reduce in PROPC a and b xor c xor b and a c Identifier 0 010 sec for parse 2 rewrites 0 000 sec 21 matches PROPC gt reduce a lt gt a lt gt a lt gt a reduce in PROPC a lt gt a lt gt a lt gt a true Bool 0 010 sec for parse 9 rewrites 0 000 sec 18 matches PROPC gt reduce a gt b and c lt gt a gt b and a gt c reduce in PROPC a gt b and
179. rvation This theorem may be proved by induction on the length of observations called context induction Since add read are the only method and attribute respectively every observation is an application of read after a finite number of applications of add A necessary command sequence is as follows Since the proof uses associativity and commu tativity of _ _ on Nat which were proven in Section 10 2 1 they are stated as equations open COUNTER ops m n p gt Nat op c gt Counter op addn Counter gt Counter eqmt tn nt m eq N Nat M Nat P Nat N M P reduce read add m add n c read add n add m c eq read addn add m add n c read addn add n add m c reduce read add p addn add m add n c read add p addn add n add m c close Alternatively you may use _ _ Section 4 4 3 and get a proof by coinduction 171 10 PROVING MODULE PROPERTIES Cafe0BJ gt open COUNTER opening module COUNTER_ done COUNTER gt ops mn gt Nat COUNTER gt op c gt Counter COUNTER gt eqm n nt m COUNTER gt eq N Nat M Nat P Nat N M P COUNTER gt reduce add m add n c add n add m c reduce in add m add n c add n add m c true Bool 0 000 sec for parse 9 rewrites 0 000 sec 37 matches COUNTER gt close Cafe0BJ gt The reduction went as desired since the system automaticall
180. s analysis In accordance to a certain folklore we sometimes say E strategy for evaluation strategy E strategies are operator attributes and are written in this form Syntax 57 evaluation strategy strat integer_list An integer list is a list of integers separated by blanks Each integer in the list represents an argument 1 is the first argument 2 is the second and so on and 0 is the whole term E strategies determine the order of evaluation As an informative example a built in con ditional is declared as follows op if_then_else_fi Bool Int Int gt Int strat 1 0 gt This E stragety ordains that the first argument conditional part be evaluated first then the whole argument Notice that the second and third arguments then and else parts 101 7 OPERATOR ATTRIBUTES do not appear in the list These arguments are not evaluated unless the whole term is evaluated and they are no longer arguments Depending on the result of evaluating the first argument one of these arguments is entirely irrelevant to the final result so this strategy is clearly reasonable Another example is an eager strategy op _ _ Int Int gt Int strat 1 2 0 gt The E strategy requires the two arguments be evaluated before the whole term 7 4 2 Default Strategy If no explicit E strategy is given the default strategy is computed as follows For each argument Evaluate the argument before th
181. s help disambiguate parsing They are either 1 Precedence specified by prec integer or SP y P ger 2 Left or right associativity specified by l assoc or r assoc respectively 7 2 1 Precedence A precedence is an integer and lesser precedences indicate stronger connectivity For ex ample op _ _ Int Int gt Int prec 33 op _ _ Int Int gt Int prec 31 states that _ _ connects stronger than _ _ and 1 2 3 parsesas 1 2 3 The default precedences depend on term constructs e Standard operators have precedence 0 Hence the term of the form f a connects strongest e When an operator is mixfix If the operator symbol does not start or end with _ that is no argument appears outside the term construct the precedence is zero An example is a singleton operator _ if it is a prefix unary operator the precedence is 15 The unary _ example Otherwise the precedence is 41 offers an Let us show examples CafeOBJ gt module PREC TEST Ts PI SS DS CCSS Ip PE SS SOS CIS Oy 5 2 8 5 defining module PREC TEST _ done CafeOBJ gt select PREC TEST PREC TEST gt parse X 5 Y S Z S CUNO 9Z 5S PREC TEST gt parse X 5 Y S X Y 8 PREC TEST gt 99 7 OPERATOR ATTRIBUTES According to the default rules _ has precedence 15 so connects stronger than _ _ Hence the r
182. s s s 0 s s 0 reduce in GCD gcd s s s s 0 s s 0 1 cond s s s s 0 lt s s 0 gt s s s 0 lt s 0 2 cond s s s 0 lt s 0 gt s s 0 lt 0 3 cond s s 0 lt 0 gt false 4 cond not s s s 0 lt s 0 gt not s s 0 lt 0 5 cond not s s 0 lt 0 gt not false 6 cond not false gt true 7 gcd s s s s 0 s s 0 gt gcd s s s s 0 s s 0 s s 0 8 gcd s s s s 0 s s 0 s s 0 gt gcd s s s 0 s 0 s s 0 9 gcd s s s 0 s 0 s s 0 gt gcd s s 0 0 s s 0 10 gcd s s 0 0 s s 0 gt ged s s 0 s s 0 11 cond s s 0 lt s s 0 gt s 0 lt s 0 12 cond s 0 lt s 0 Se DS O 13 cond O lt 0 gt false 14 cond not s 0 lt s 0 Z gt not 0 lt 0 15 cond not 0 lt 0 gt not false 16 cond not false gt true 17 gcd s s 0 s s 0 gt gcd s s 0 s s 0 s s 0 18 gcd s s 0 s s 0 s s 0 gt gcd s 0 s 0 s s 0 19 gcd s 0 s 0 s s 0 gt gcd 0 0 s s 0 20 gcd O 0 s s 0 gt gcd 0 s s 0 21 cond 0 lt s s 0 gt true 22 gcd 0 s s 0 gt gcd s s 0 0 23 cond s s 0 lt 0 gt false 24 gcd s s 0 0 gt s s 0 s s 0 NzNat 0 000 sec for parse 24 rewrites 0 070 sec 60 matches GCD gt 6 2 Do the Evaluation The apparent dif
183. soning is of the form to t SH oe bn and the theorem to prove is the equation ty tn Another way to prove theorems by evaluation is to state the theorems as terms of sort Bool and to evaluate them If the terms are reduced to true the theorems are proved For example to show eqat a 0 we may try to reduce the term a a to true This approach does not confer you with much extra power As explained in Section 4 4 1 in evaluating _ _ CafeOBJ simply reduces both arguments and check if they are equal Apart from the equality checking part which involves equational theory Section 7 1 what can be done with _ _ can be done without In terms of presentation however this approach produces something like GROUP gt start a a GROUP gt apply reduce at term result true Bool which is more appealing to intuition than GROUP gt start a a GROUP gt apply reduce at term result 0 G where you must mentally compare the actual result with the expected Especially when both sides of the equation need evaluation this approach provides you with a much more compact proof 164 10 2 Theorem Proving Techniques 10 2 1 Structural Induction In Section 9 1 1 we have presented a proof score to show that 0 is a right identity of _ _ under the definition of SIMPLE NAT The score relies on structural induction Strictly speaking proofs by structural induction only d
184. sort Date you can write year d and to set the slot to y write set year d y Strictly speaking since the definitions of access functions are by axioms axioms are to be explained in Chapter 4 a record declaration involve axioms as well as signatures You may investigate all the above effects by show command cf Section 5 1 4 3 4 2 Inheriting Records You can extend a record to create a new record The same access functions can be used as before The process of extending a record is called record inheritance la peculiar parlance of some community and is denoted by the following construct Syntax 39 record declaration with inheritance record record_name list_of upper_records 1 list_of_slot_declarations y A list of slot declarations is as in a plain record declaration A list of upper records is comma separated An upper record is of the form Syntax 40 upper record record_name slot_mapping where a slot mapping is Syntax 41 slot mapping slot_name gt slot_name slotname gt slot_name x where slot names before gt must be the ones belonging to the given record while names after gt are arbitrary so long as not conflicting Under a record declaration with inheritance the newly declared record inherits all the slots from the upper records Slot mappings which specify renaming are to be
185. sorts opera tors and records Chapter 3 while those in an axioms block are restricted to declarations of variables equations and transitions Chapter 4 imports signature and axioms blocks may appear more than once in a single module signature may be abbreviated to sig and axioms to axs These block constructs are for the sake of legibility and have no semantic connotation For example module SIMPLE NAT 4 signature Zero NzNat lt Nat op 0 gt Zero op s Nat gt NzNat op _ _ Nat Nat gt Nat axioms vars N N Nat eqO N N eq s N N s N N y is exactly the same module declaration as module SIMPLE NAT 4 Zero NzNat lt Nat op 0 gt Zero op s Nat gt NzNat op _ _ Nat Nat gt Nat vars N N Nat eqO N N eq N s N s N N or minutely blocked 15 2 MODULE DECLARATION module SIMPLE NAT signature Zero NzNat lt Nat signature op O ZE O op s Nat gt NzNat signature op _t_ Nat Nat gt Nat y axioms vars N N Nat axioms eqO0 N N eq N s N s N N y In inspecting modules by show command Section 1 3 3 you may notice that the system uses these block constructs even if you did not supply them cf Chapter 5 2 3 Tight Modules Loose Modules In CafeOBJ a module plays two different r les depending on where it appears or what it contains In one guise a module denotes a unique
186. t module TEST defining module TEST_ done CafeOBJ gt module TEST defining module TEST Warning redefining module TEST _ done Cafe0BJ gt protect TEST Cafe0BJ gt module TEST gt defining module TEST Error module TEST is protected CafeOBJ gt unprotect TEST Cafe0BJ gt module TEST gt defining module TEST Warning redefining module TEST _ done Cafe0BJ gt According to the syntax of module declarations empty modules are allowed as was the TEST here You are warned even if the unprotected TEST is overwritten Once under protection TEST cannot be redefined Stripped of protection it is subject to redefinition again 2 2 Blocks in a Module Module elements can be classified in three categories 1 references to other modules 2 signature definitions and 3 axioms It is possible to gather elements in each category into blocks References to other modules may be clustered by the following syntax Syntax 20 imports block imports module_element y where module elements are restricted to import declarations Section 2 5 Similarly sig nature definitions and axioms may be clustered by Syntax 21 signature block signature module_element x 14 2 2 Blocks in a Module Syntar 22 axioms block axioms module element x y where module elements in a signature block are restricted to declarations of
187. t equals the constant true We may say therefore that a boolean term is a condition As mentioned earlier Section 2 5 every module implicitly imports the module BOOL unless you have locked it out A major reason is that BOOL provides you with boolean terms BOOL contains all the usual boolean operators so that as conditions the following terms may be used if B B are boolean terms true false not B B and B B or B A complete listing may be obtained by show command see Section 5 4 2 3 Behavioural Equation Declaration To state behavioural equality explicitly the following constructs are available Syntaz 47 behavioural equation declaration beq label term term bceq label term term if boolean_term bceq may be abbreviated to bcq Labels etc are as in eq or ceq Also as in eq or ceq both terms must belong to the same connected component 41 4 AXIOMS According to the above definition you can write behavioural equations over visible sort There is no harm in that such equations are treated just like equations with eq or ceq But do avoid using beq if eq is what you mean Legality does not imply good manners Note that in many cases behavioural equality is defined indirectly with ordinary equations declared with eq or ceq not with behavioural ones cf Section 5 2 3 Behavioural equations are reserved for cases where explicit statements are des
188. t explain the above in detail and only say that these declarations are necessary for the flexible syntax you may use and for realising record inheritances Remember that a record may be written as Date year 1984 month 1 day 1 or Date month 1 day 1 year 1984 interchangeably you may also omit uninteresting slots as Date year 1984 56 5 2 Some Typical Modules where month and date disappear and set set year etc will be declared for every record that inherits Date Finally look at axioms DATE gt show axioms Equations eq day RID 5 RecordDate VAR SLOTDAY 4 Slotday VAL 7 Nat ATTRS 6 Attributes VAL 7 Nat eq set day RID 5 RecordDate VAR SLOTDAY 4 Slotday VAL 7 Nat ATTRS 6 Attributes NEW VAL 8 RID 5 RecordDate VAR SLOTDAY 4 Slotday NEW VAL 8 ATTRS 6 Attributes Again we omitted the rest of the long output The above two equations define day and set day Their simplified forms are eq day Date day D month M year Y D eq set day Date day D month M year Y D Date day D month M year Y which look exactly like the access functions to day 5 2 Some Typical Modules 5 2 1 Unique Models When you write a specification of natural numbers Section 5 1 1 your probable intention is to specify the natural numbers For example you do not want a singleton 0 to constitute a model of your specification the e
189. t given in the declaration The scope of a variable is within the module where it is declared or more precisely in the rest of the module after the declaration For example module M S Coa 8h gt S axioms using X a var X 8 S5 axioms using X b y would be an error if you put axioms in a involving X The correct place for such axioms is b It is illegal to declare a variable of the same name for different sorts And it is meaningless to re declare the variable for the same sort Sometimes it is convenient to use common variable names such as X for different sorts And sometimes it is economical to use an ephemeral variable valid only to the place where it appears For these reasons another construct for variable declaration is available Syntax 43 variable declaration on the fly variable_name sort_name Do not insert blanks on either side of the colon N Nat N Nat is unacceptable Only N Nat will do The following session illustrates the utility of declarations of this form Recall from Section 3 3 2 a module called SIMPLE INT 38 4 2 Equation Declaration Cafe0BJ gt parse in SIMPLE INT X Int s 0 X s 0 Int Cafe0BJ gt The variable X was declared on the fly If you only want to check syntactic ambiguity it is a bother to declare variables separately just for that purpose The system treats an ephemeral variable declaration as a term nothing mor
190. tate turning out to be either argument which itself may be indeterminate The above rules say that an indeterminate state may become more and more determinate but not conversely It is obvious that if these rules were equations all the states would be the same so that State would be an uninteresting singleton 42 4 4 Internalising Axioms A traditional way to describe the above choice operator is to define an explicit transition function The technique works at times but in this nondeterministic example it would lead to something like module CHOICE State ops ab gt State op _ l_ State State gt State op choose State gt State vars X Y State eq choose X Y eq choose X Y ou lt ps eq choose a a b eq choose b which alas is a specification of singletons 4 4 Internalising Axioms Axioms define certain kinds of relations when we construct models For example axioms introduced by eq or ceq define minimal congruence relations between reachable term generated elements of visible sorts These relations reside outside of CafeOBJ descriptions the mark is just a notation For various purposes it is convenient if these relations can be manipulated within the syntac tical framework of CafeOBJ In general it is impossible to give general decision procedures for these relations but under certain conditions or in some restricted sense it is possible to implement procedures
191. tead of id This attribute has the the same meaning as id 7 1 4 Idempotency That _and_ is idempotent is stated as follows op _and_ Bool Bool gt Bool assoc comm id true idem idem is equivalent to the equation eq X Bool and K X Idempotency affects evaluation For example true and true and true matches modulo idempotency idem makes sense only when the operator is binary and the arity sorts and the coarity sort are the same Formerly there was no explicit condition In the current implementation an equation like the above is actually added The system sometimes misbehaves the only certainty about idempotency is that matching modulo the combination of associativity commutativity and idempotency works correctly 7 1 5 Inheriting Equational Theory Attributes Equational theory attributes are inherited by operators if they have the same name and are declared on lower sorts For example when you declare Nat lt Int op _ _ Nat Nat gt Nat op _ _ Int Int gt Int assoc the operator _ _ on Nat is assumed associative Since a subsort is a subset such attribute inheritance is quite natural if associativity holds for all the integers it a forteriori holds for all the natural numbers As a special case an identity is inherited only when the identity term belongs to the lower sort 98 7 2 Parsing Attribute 7 2 Parsing Attribute Parsing attribute
192. the search space can be large gt is a dangerous weapon In such cases you may limit the search up to a realistic step with the set of predicates n gt where n is a natural number in the usual decimal notation and indicates how many transit steps to take For example CHOICE NAT gt reduce 0 s 0 s s 0 s s s 0 0 s s s s 0 1 gt s s s 0 reduce in CHOICE NAT O s 0 s s 0 s s s 0 0 s s s s 0 1 gt s s s 0 Warning N gt terminates reaching preset maximum count of transitions false Bool 0 010 sec for parse 13 rewrites 0 000 sec 16 matches CHOICE NAT gt which is a correct result since the first argument cannot transit to the second in one step Another way to limit the search is by a switch CafeOBJ gt set exec limit 40 limits the maximal transition step to 40 The default limit is quite large a As the above sessions show _ gt _ and _ gt _ take into account equations as well as transitions In most cases and with appropriate evaluation strategies _ gt _ does give correct answers on transition relations However it is in general impossible always to obtain correct answers on transition relations between equivalence classes of terms For example consider a module module M ow opsabcd gt S eqa b trans a gt c eqc Hd E 169 10 PROVING MODULE PROPERTIES and a theorem
193. ther modules For complete cleanup use CafeOBJ gt full reset which reinitialises the internal state of the system But before calling this command re member that you will lose all the module definitions you have supplied so far You are warned Bug Reports The system is under continual improvement If you detect any bugs malfunctions or just inconveniences do let us know The support team is reachable via cafe bugsOldl jaist ac jp 1 2 Files and Libraries 1 2 1 Reading Files Not every module is as trivial as TEST and you will soon need library systems for store recovering module definitions test cases and so on Cafe OBJ requires every imported module cf Section 2 5 to be defined beforehand so you need a recursive file reference mechanism As a minimum you need the following command Syntax 1 input command input pathname input or in for short requests the system to read the file specified by the pathname The file itself may contain input command and so on ad nauseum CafeOBJ reads the file up to eof or until it encounters a line that only contains the literal eof Syntar 2 eof command eof 1 2 Files and Libraries This little command is especially useful when the codes are under development You can supply the system with only those definitions that are up to scratch Pathnames follow the conventions of the Unix file system Both relative and absolute paths are possible
194. ts hsort invisibles op ordinary operators bop behaviourals and param parameters Sort and operator names should be familiar now Source names may be qualified target names may not they are supposed to be brand new names II Commas may be omitted Note that renaming creates a new different module even if it has isomorphic models A consequence is that a renamed module is not shared cf Section 8 1 2 Renaming is meant to describe a bijective signature morphism Section 8 2 2 The current implementation allows more flexible renaming however and you g may collapse two distinct sort operators into one If you do give such a renam ing care should be taken Renaming is quite often used in combination with instantiations Since instantiation is a module level operation that generates specific data types from generic ones it is natural for you to confer names that describe specialised sorts and operators more effectively For example in specialising generic indexed lists to those of natural numbers Section 8 3 1 you may write module NAT ILIST protecting ILIST IDX lt view to SIMPLE NAT sort Elt gt Nat DAT lt view to SIMPLE NAT sort Elt gt Nat sort IList gt IList of Nat In the parameterised ILIST a simple IList is okay to denote lists of something After instantiation a list is a list of natural numbers so why not call it as it is 8 4 3 Module Sum Combining several modules together
195. ty Bool For example pred _ lt _ Nat Nat has the same meaning as op _ lt _ Nat Nat gt Bool The system does not distinguish predicates as such You should think of them i a as mere shorthands Nothing more To complete the picture bpred is a shorthand of bop with coarity Bool Syntar 33 behavioural predicate declaration bpred standard_operator_symbol list_of_sort names bpred mizxfix_operator symbol list_of_sortznames 3 3 Terms 3 3 1 Well formed Terms As well as adopting arbitrary notational practices you may use the same notation to denote different operators such as 1 2 for addition and a a b for direct sum These flexibilities greatly enhance the legibility of CafeOBJ codes and we believe it worthwhile to support them One disadvantage of this liberty is the extra amount of processing time in parsing terms Another and more important problem is that a term may be parsed in more than one ways We make recourse to the following definition A term is well formed iff it has exactly one least parse tree Several parse trees are okay so long as all of them are of related sorts and one of them has a least sort The least sort is the smallest set to which the element belongs Dual membership is a seed of troubles just as dual marriage is A signature is regular iff all the terms have least sorts and a module is regular iff its signature is With the above observations in mind
196. ule_element yy 129 8 MODULE STRUCTURE principal sort may be abbreviated to p sort A sort name refers to a sort that is declared within the module or in an imported module Let us show some examples If you have module ONE Elt and module SIMPLE NAT principal sort Nat the same as SIMPLE NAT it is possible to declare a view view V from ONE to SIMPLE NAT which apparently is an empty mapping This is equivalent to view V from ONE to SIMPLE NAT sort Elt gt Nat Since great many views are from single sort modules principal sorts are very useful for making views compact If so declared a sort is principal in and only in that module and principality is not obtain able via importation The current version does not support all the mechanisms explained here Iden tifying sorts or operators by name is sometimes tedious you may have to i probe the depth of the module hierarchy Or controvertial Consider e g _ _ for natural number addition and for direct summation of sets It is also possible to shorten views by importation At the time of writing it is not possible We have not even worked out a i relevant syntax 8 3 Binding Parameters 8 3 1 Instantiation of Parameterised Modules An instance of a parameterised module is created by binding actual parameters to formals The process of binding is called instantiation The result of instantiati
197. us section In the proof score a constant a was declared by op a gt Nat to represent any element of sort Nat Such declarations appear quite often when you are using the evaluation mechanism to prove theorems To prove that 0 is a right identity a appeared to calculate the induction step reduce s a 0 To make proofs more concise you may use on the fly declarations of constants similar to variable declarations on the fly Section 4 1 Syntax 72 constant declaration on the fly constant_name sort_name where a constant name is a character string that starts with the backquote The effects of declarations are temporary like the case of variables Using this construct it is possible to invoke reduction commands without opening modules as Cafe0BJ gt select SIMPLE NAT SIMPLE NAT gt reduce O 0 reduce in SIMPLE NAT O 0 O Zero 0 000 sec for parse 1 rewrites 0 000 sec 1 matches SIMPLE NAT gt reduce s a Nat 0 reduce in SIMPLE NAT s a Nat 0 s a Nat 0 NzNat 0 000 sec for parse 1 rewrites 0 000 sec 6 matches SIMPLE NAT gt This time the hypothesis is implicit instead of stating and using it explicitly you take note of it in analysing the result of the second evaluation 144 9 2 Applying Rewrite Rules In fact you get quite similar effects by using variables on the fly instead of constants Although evaluation is a procedur
198. valuation It is controlled by a switch and Cafe0BJ gt set clean memo on tell the system to be forgetful The default is off It is also possible to initialise memo storages by the following command 104 7 6 Operator Attributes and Evaluations CafeOBJ gt clean memo The memo attributes may be ignored if you turn a switch off as CafeOBJ gt set memo off 7 5 1 Coherence As explained in Section 6 2 1 and 6 2 4 in evaluating a term application of behavioural axioms is prohibited unless the redex is enclosed in an observation and this restriction is to ensure the soundness of evaluation This implies that the system can ignore the restriction so long as the application does not lead to an incorrect reasoning An attribute called coherent may be used to tell the system to loosen the guard It asserts that the operator acts indistinguishably on behaviourally equivalent terms so that it is in effect a behavioural operator For example the declarations T SS Je ops a b gt S bop g S gt T op f S gt T coherent beq a sim b a b allow the system to apply a sim b to f a where a is not guarded by an observation as well as to g a where a is 7 6 Operator Attributes and Evaluations Let us see how various attributes affect evaluation In the case of an associative operator with identity module AZ OP CS ops a b c phi gt S op __ SS gt S associative id phi J you ma
199. ving mappings of sorts and operators under which axioms of T hold in M hence in M since M does not contain extra axioms To instantiate a parameterised module it is not enough to supply an actual parameter since there are in general several ways to replace sorts with sorts and operators with operators You need a view A view declaration consists of a parameter module an actual parameter module and a set of maps that constitute a specification morphism Syntax 63 view view view_name from module_name to module_name view_element SR view_element map variable_declaration A view name is a character string The module names after from and to are those of the parameter module and the actual parameter respectively Maps are as follows sort sort_name gt sort_name hsort sort_name gt sort_name op operator_reference gt operator_reference bop operator_reference gt operator_reference map A sort name may be qualified by a module name or a parameter name Section 8 1 3 and has to be visible for sort and hidden for hsort An operator reference is an operator name or a term that denotes a derived operator An operator reference may also be qualified And needless to say op is for non behavioural operators and bop is for behaviourals For a source operator only operator names or terms that denotes original operators is allowed Using the example of MULT with variab
200. were labelled as eq l id 0 X X the apply command might as well be GROUP gt apply 1 id at 1 152 9 2 Applying Rewrite Rules Do not put blanks anywhere in between the sign module name period number or label Memorise a rule spec hates vacuum Finally show command with rule not rules may be used to print a single rule This command is useful when the number of rewrite rules is large An example GROUP gt show rule 2 rule 2 of the last module 6 5 26 0 This rule rewrites up Do not forget the period before 2 Arguments to this command are rule specifications and 2 is of rule specification form according to the definition in Section 9 2 1 show rule and show rules may be invoked when no module is opened In such a case the rule s of the current module are printed 9 2 5 Appyling Conditionals When the action is a rewrite rule apply command tries to apply just one rule and imme diately returns the control to you What if the rule is conditional Recall GCD Section 6 2 8 153 9 THEOREM PROVING TOOLS Cafe0BJ gt open GCD opening module GCD done GCD gt start gcd s 0 s s 0 GCD gt show rules rewrite rules in module GCD 1 ceq gcd N M gcd M N if N lt M 2 eq gcd N 0 N 3 ceq gcd s N s M gcd s N s M s M if not N lt M GCD gt apply 1 at term shifting focus to condition condition 1 s 0 lt s s 0 Bool
201. y The operator must be in the current module which must be set be forehand If an operator name is omitted all the operators directly declared in the current module is checked Laziness is related to evaluation strategies The system checks a sufficient condition under which an operator may be evaluated lazily as explained Section 7 4 Here is an example Cafe0BJ gt module LAZY 4 S op ik S gt S op g S gt S eq f f X S g X eq g X S X defining module LAZY _ done Cafe0BJ gt select LAZY LAZY gt check laziness laziness of operator f O O strict on the arguments 1 rewrite strategy 1 0 axioms eq X S g X S laziness of operator g g s gt S5 may delay the evaluation on the arguments 1 rewrite strategy 0 1 0 axioms eq g X S X S LAZY gt I The system only checks an apparent sufficient condition and do not use a detailed strictness analysis as used in functional language compilers The word laziness was chosen humbly and carefully 163 10 PROVING MODULE PROPERTIES 10 2 Theorem Proving Techniques We have already shown a couple of proofs based on the TRS engine of CafeOBJ Sections 9 1 1 9 2 2 There a proof score was a sequence of commands including open reduce and apply The system reads the commands rewrites terms as commanded and prints the result Behind such rewrite sequences is equational reasoning schematically the rea
202. y added an equation eq hs1 Counter hs2 Counter read hs1 Counter read hs2 Counter once _ _ was shown to be a congruence Section 5 2 4 As an aside you may wonder why two axioms are given in these forms commutativity is stated with constants while associativity is with variables The reason is that a straight forward statement of commutativity eq M Nat N Nat N M engenders infinite rewrite sequences The trick here is to give an axiom that restricts the matching power of the system so that only in the special instances when you need for this special proof the axiom is usable as a rewrite rule 10 2 5 Behavioural Transition To illustrate proofs on behavioural transitions we define counters of wobbly numbers 172 10 2 Theorem Proving Techniques module W COUNTER protecting CHOICE NAT Counter bop read Counter gt Nat bop add Nat Counter gt Counter eq read add N Nat C Counter N read C The structure is the same as COUNTER and the difference is in the imported CHOICE NAT We would like to prove a behavioural transition relation btrans add M Nat N Nat C Counter gt add N C An element of hidden sort behaviourally transits to another iff every observation of the former transits to the same observation of the latter This definition leads to a proof by context induction as in the previous section The session goes as follows Cafe0BJ gt open W COUNTER
203. y compute as follows phi a phi b phi c gt a phi b phi c gt a b phi c gt abc 105 7 OPERATOR ATTRIBUTES where phi s are eliminated wherever they appear Indeed the system computes exactly like you CafeOBJ gt select AZ OP AZ OP gt set trace on AZ OP gt reduce phi a phi b phic reduce in AZ OP phi a phi b phi c 1 gt 1 rule eq ident12 phi X ID S X ID S X ID S gt a phi b phi c 1 lt 1 phi a phi b phi c gt a phi b phi c 1 gt 2 rule eq A2 phi X ID S A1 A2 X ID S A1 A1 gt phi c X ID S gt b A2 gt a 1 lt 2 a phi b phi c gt a b phi c 1 gt 3 rule eq A1 phi X ID S A1 X ID S Sm e Mil gt al 1 lt 3 a b phi c gt ab c abe S 0 000 sec for parse 3 rewrites 0 260 sec 13 matches AZ OP gt The equations in this trace were generated by the system to cope with identity The exact mechanism need not be your concern but beware that these extra equations may cause havoc Section 7 8 If you inspect the statistics it is apparent that the numbers of matching attempts greatly exceeded those of rewrites This is a general fact about evaluation modulo equational theory See what happens if the operator is also commutative as in 106 7 6 Operator Attributes and Evaluations AZ OP gt module ACZ OP S ops abc phi gt S5 op __ S S gt S associative commutative id phi defining module ACZ OP _ _ done AZ
204. you understand this is an important property CafeOBJ has a mechanism to regularise signatures To invoke this mechanism you may use 27 3 SIGNATURE Syntax 34 regularize command regularize module_name or set a switch for automatic invocation to on by Cafe0BJ gt set regularize signature on The default is off To regularise a signature additional sorts and operator declarations may be declared These addidions ensure the existence of lowest operators For a trivial example in module INTB NonPos Nat lt Int op 0 gt NonPos op 0 gt Nat Jr the constant 0 belongs both to NonPos and to Nat In general it is possible to overload constants there is a way to distinguish them see Section 3 3 2 and there is no harm in that But in this example since NonPos and Nat are both subsorts of Int the constant must in fact denote the same element As a consequence the term 0 does not have a least parse even qualified as in Section 3 3 2 A remedy is to add a common subsort of NonPos and Nat and declare O of that sort Using regularize command you do get a module modified along this line module INTB NonPos Nat lt NonPos Nat lt Int op 0 gt NonPos op 0 gt Nat op 0 gt NonPos Nat Two old declarations of O are redundant by now but system does not remove these Os in automatic More generally the system searches for operators that may create terms with no least pars

Download Pdf Manuals

Related Search

Related Contents

NTE INEN 2377  17579 - Truper  ILOG JViews 5.5 Graphics Framework User's Manual  concord ultimax.3  DVIDEC100 - Elpro Video Labs  Samsung AR12HSFNCWKX User Manual  Design House 533372 Installation Guide  g-ForceMR Sport  HP LC3260N Warranty and Support Guide    

Copyright © All rights reserved. Failed to retrieve file