Benutzer:DerSpezialist/Maude (Termersetzungssystem)
Das Termdefinitions- und -ersetzungssystem Maude ist eine Implementierung eines Termersetzungssystems, entwickelt von SRI International. Der grundsätzliche Ansatz ist ähnlich zu Joseph Goguens Implementierung OBJ3 der Gleichungslogik, basiert aber auch Termersetzung statt auf ordnungssortierter Gleichungslogik und mit einem starken Fokus auf Metaprogrammierung durch Reflection.
Maude ist Freie Software und es gibt Online-Tutorials.
Einfaches Beispiel
[Bearbeiten | Quelltext bearbeiten]Module in Maude, sogenannte Umschreibetheorien, bestehen aus einer Termsprache mit Mengen von Gleichungen und Umschreiberegeln. Terme in einer Umschreibetheorie werden mit Operatoren mit 0 oder mehr Argumenten gewisser sogenannter Sorten, die einen Term einer gewisser Sorte ergibt. Operatoren mit 0 Argumenten sind Konstanten.
Zeilenkommentare in Maude beginnen mit ---, mit drei Bindestrichen.
Beispiel 1
[Bearbeiten | Quelltext bearbeiten]fmod NAT is
sort Nat .
op 0 : -> Nat [ctor] .
op s : Nat -> Nat [ctor] .
endfmDiese Umschreibetheorie spezifiziert die natürlichen Zahlen. Die Anweisung sort gibt an, dass eine Sorte mit dem Namen Nat exisiteren soll. Dann folgt, wie die Terme der von Nat konstruiert werden. Der Operator s ist die Nachfolgerfunktion. Die Null wird durch eine eigene Konstante 0 dargestellt, Die natürliche Zahl Eins wird durch s 0 dargestellt.
Beispiel 2
[Bearbeiten | Quelltext bearbeiten]fmod NAT is
sort Nat .
op 0 : -> Nat [ctor] .
op s : Nat -> Nat [ctor] .
op _+_ : Nat Nat -> Nat .
vars N M : Nat .
eq 0 + N = N .
eq s N + M = s (N + M) .
endfmHier wird das Pluszeichen eingeführt, um die Addition von natürlichen Zahlen darzustellen. Seine Definition ist fast identisch mit der vorherigen, mit Eingabe und Ausgabe Sorten, aber es gibt einen Unterschied: der Operator hat Unterstriche auf jeder Seite. In Maude kann der Benutzer Infix-, Postfix- oder Präfixoperatoren definieren (wobei Präfix der Default ist), indem Unterstriche als Platzhalter für die Operanden-Terme verwendet werden. Da der Plus-Operator einen Tern auf jeder Seite annimmt, ist er ein Infix-Operator – im Gegensatz zu s, welches Terme vorangestellt werden muss (Präfixoperator).
Kommentare
[Bearbeiten | Quelltext bearbeiten]Drei Sterne sind in Maude normalerweise Zeilenkommentare; folgt jedoch eine öffnende Klammer, ist der Inhalt bis zur schließenden Klammer Kommentar:
*** rest of line is ignored by Maude
*** (
section
is
ignored by Maude
)The extended Nat module also holds two variables and two sets of equations.
vars N M : Nat .
eq 0 + N = N .
eq s(N) + M = s (N + M) .When Maude "executes", it rewrites terms according to our specifications. And this is done with the statement
reduce in <some module> : <some term> .
or the shorter form
red <some term> .
For this last statement to be used it is important that nothing is ambiguous. A small example from our rewrite theory representing the natural numbers:
reduce in NAT : s(0) + s(0) . rewrites: 2 in 0ms cpu (0ms real) (~ rewrites/second) result Nat: s(s(0))
Using the two equations in the rewrite theory NAT Maude was able to reduce our term into the desired term, the representation of the number two i.e. the second successor of 0. At that point no other application of the two equations were possible, so Maude halts. Maude rewrites terms according to the equations whenever there is a match between the closed terms that one tries to rewrite (or reduce) and the left hand side of an equation in our equation-set. A match in this context is a substitution of the variables in the left hand side of an equation which leaves it identical to the term that one tries to rewrite/reduce.
To illustrate it further one can look at the left hand side of the equations as Maude executes, reducing/rewriting the term.
eq s(N) + M = s (N + M) .
can be applied to the term:
s(0) + s(0)
since the substitution:
N => 0 M => s(0) s(N) + M [[N => 0, M => s(0)]] == s(0) + s(0)
makes them identical, and therefore it can be reduced/rewritten using this equation. After this equation has been applied to the term, one is left with the term:
s (0 + s(0))
If one takes a close look at that term, they will see that it has a fitting substitution with matches the first equation, at least parts of the term matches the first equation:
eq 0 + N = N .
substitution:
N => s(0) s (0 + N) [[N => s(0)]] == s (0 + s(0)) 0 + s(0) - matches first equation and is rewritten
The second substitution and rewrite step rewrites an inner-term (the whole term does not match any of the equations but the inner term does). Then one ends up with our resulting term s(s(0)), and it can seem like a lot of hassle to add 1 + 1, but hopefully you will soon see the strength of this approach.
Another thing worth mentioning is that reduction/rewriting up to this point has taken something very important for granted, which is:
- Reduction/Rewriting terminates
- Reduction/Rewriting is confluent (applying the equations in any order will eventually lead to the same resulting term)
This cannot be taken for granted, and for a rewrite theory to be sane, one has to ensure that equational application is confluent and terminating. To prove that term-rewriting terminates is not possible in every instance, which we know from studying the halting problem. To be able to prove that term-rewriting (with regards to the equations) terminates, one can usually create some mapping between terms and the natural numbers, and show that application of the equations reduces the associated value of the term. Induction then proves that it is a halting process since the event of finding smaller natural numbers is a halting process. Naturally equation sets that can cause a term-rewrite to contain cycles will not be terminating. To prove confluence is another important aspect since a rewrite theory lacking this ability will be rather flawed. To prove that the equation set is confluent one has to prove that any application of the equations to any belonging term will lead to the same resulting term (termination is a prerequisite). Details for how to prove termination or confluence will not be given here, it just had to be mentioned, since this is where equations and rewrite-rules differ, which is the next topic of this short overview.
Rewrite Rules
[Bearbeiten | Quelltext bearbeiten]Up to this point rewriting and reduction have been more or less the same thing, our first rewrite theory had no rewrite rules, still we rewrote terms, so it is time to illustrate what rewrite rules are, and how they differ from the equations we have seen so far (they do not differ much from equations naturally since we talk about the two concepts almost interchangeably).
The module presented so far NAT which represented the natural numbers and addition on its elements, is considered a functional module/rewrite theory, since it contains no rewrite rules. Such modules are often encapsuled with a fmod and endfm (instead of mod endm) to illustrate this fact. A functional module and its set of equations must be confluent and terminating since they build up the part of a rewrite theory that always should compute the same result, this will be clear once the rewrite rules come into play.
Example 3
[Bearbeiten | Quelltext bearbeiten]mod PERSON is including NAT . *** our previous module sort Person . sort State . op married : -> State [ctor] . op divorced : -> State [ctor] . op single : -> State [ctor] . op engaged : -> State [ctor] . op dead : -> State [ctor] . op person : State Nat -> Person [ctor] . var N : Nat . var S : State . rl [birthday] : person (S, N) => person (S, N + s(0)) . rl [get-engaged] : person (single, N) => person (engaged, N) . rl [get-married] : person (engaged, N) => person (married, N) . rl [get-divorced] : person (married, N) => person (divorced, N) . rl [las-vegas] : person (S, N) => person (married, N) . rl [die] : person (S, N) => person (dead, N) . endm
This module introduces two new sorts, and a set of rewrite rules. We also include our previous module, to illustrate how equations and rewrite rules differ. The rewrite rules is thought of as a set of legal state changes, so while equations hold the same meaning on both sides of the equality sign, rewrite rules do not (rewrite rules use a => token instead of an equality sign). You are still the same person after you're married (this is open for debate), but something has changed, your marital status at least. So this is illustrated by a rewrite rule, not an equation. Rewrite rules do not have to be confluent and terminating so it does matter a great deal what rules are chosen to rewrite the term. The rules are applied at "random" by the Maude system, meaning that you can not be sure that one rule is applied before another rule and so on. If an equation can be applied to the term, it will always be applied before any rewrite rule.
A small example is in order:
Example 4
[Bearbeiten | Quelltext bearbeiten]rewrite [3] in PERSON : person (single, 0) . rewrites: 4 in 0ms cpu (0ms real) (~ rewrites/second) result Person: person (married, s(0))
Here we tell the Maude system to rewrite our input term according to the rewrite theory, and we tell it to stop after 3 rewrite steps (remember that rewrite rules do not have to be terminating or confluent so an upper bound is not a bad idea), we just want see what sort of state we end up in after randomly choosing 3 matching rules. And as you can see the state this person ends up in might look a bit strange. (When you're married at the age of one you kind of stick out a bit in kindergarten I guess). It also says 4 rewrite steps, although we specifically stated an upper limit of 3 rewrite steps, this is because rewrite steps that are the result of applying equations does not count (they do not change the term, at least if the equations are sane). In this example one of the equations of the NAT module has been used to reduce the term 0 + s(0) to s(0), which accounts for the 4'th rewrite step. To make this rewrite theory a bit less morbid, we can alter some of our rewrite rules a bit, and make them conditional rewrite rules, which basically means they have to fulfill some criteria to be applied to the term (other than just matching the left hand side of the rewrite rule).
crl [las-vegas] : person (S, N) => person (married, N) if (S =/= married) /\ (S =/= dead) . crl [die] : person (S, N) => person (dead, N) if (S =/= dead) .
It seems reasonable that you cannot die once you're dead, and you cannot marry as long as you are married. The leaning toothpicks (/\) are supposed to resemble a logical AND which means that both criteria have to be fulfilled to be able to apply the rule (apart from term matching). Equations can also be made conditional in a similar manner.
Why Rewriting Logic? Why Maude?
[Bearbeiten | Quelltext bearbeiten]Maude sets out to solve a different set of problems than ordinary imperative languages like C, Java or Perl. It is a formal reasoning tool, which can help us verify that things are "as they should", and show us why they are not if this is the case. In other words, Maude lets us define formally what we mean by some concept in a very abstract manner (not concerning ourselves with how the structure is internally represented and so on), but we can describe what is thought to be the equal concerning our theory (equations) and what state changes it can go through (rewrite rules). This is extremely useful to validate security protocols and critical code. The Maude system has proved flaws in cryptography protocols by just specifying what the system can do (in a manner similar to the PERSON rewrite theory), and by looking for unwanted situations (states or terms that should not be possible to reach) the protocol can be shown to contain bugs, not programming bugs but situations happen that are hard to predict just by walking down the "happy path" as most developers do.
We can use Maude's built-in search to look for unwanted states, or it can be used to show that no such states can be reached.
A small example from our PERSON module once again.
search [1] in PERSON : person (single, 1) =>1 person (married, 2) . No solution.
Here the Natural numbers have a more familiar look (the basic Maude modules prelude.maude has been loaded, that can be done with the command "in prelude", or 1 can be replaced by s(0) and 2 by s(s(0)) if you don't want to load the default Maude-modules), naturally Maude has built-in support for ordinary structures like integers and floats and so on. The natural numbers are still members of the built-in sort Nat. We state that we want to search for a transition using one rewrite rule (=>1), which rewrites the first term into the other. The result of the investigation is not shocking but still, sometimes proving the obvious is all we can do. If we let Maude use more than one step we should see a different result:
search [1] in PERSON : person (single, 1) =>+ person (married, 2) .
Solution 1 (state 7) states: 8 rewrites: 14 in 0ms cpu (0ms real) (~ rewrites/second)
To see what led us in that direction we can use the built in command show path which lets us know what rule applications led us to the resulting term. The token (=>+) means one or more rule application.
show path 7 . state 0, Person: person (single, 1) ===[[rl person(S, N) => person(S, N + 1) [label 'birthday]] .] ===> state 1, Person: person (single, 2) ===[[crl person(S, N) => person(married, N) if S =/= married = true /\ S =/= dead = true [label las-vegas]] .] ===> state 7, Person: person (married, 2)
As we can see the rule application "birthday" followed by "las-vegas" got us where we wanted. Since all rewrite theories or modules with many possible rule applications will generate a huge tree of possible states to search for with the search command, this approach is not always the solution. We also have the ability to control what rule applications should be attempted at each step using meta-programming, due to the reflective property or rewriting logic.
References
[Bearbeiten | Quelltext bearbeiten]- Clavel, Durán, Eker, Lincoln, Martí-Oliet, Meseguer and Quesada, 1998. Maude as a Metalanguage, in Proc. 2nd International Workshop on Rewriting Logic and its Applications, Electronic Notes in Theoretical Computer Science 15, Elsevier.
- Martí-Oliet and José Meseguer, 2002. Rewriting Logic: Roadmap and Bibliography. Theoretical Computer Science 285(2):121-154.
- Martí-Oliet and José Meseguer, 1993-2000. Rewriting Logic as a Logical and Semantic Framework [1]. Electronic Notes in Theoretical Computer Science 4, Elsevier.
Further reading
[Bearbeiten | Quelltext bearbeiten]External links
[Bearbeiten | Quelltext bearbeiten]- Maude homepage at University of Illinois at Urbana-Champaign;
- The Real-Time Maude Tool homepage developed by Peter Csaba Ölveczky;
- An introduction to Maude by Neal Harman, Swansea University (errata)
- The Policy And GOal based Distributed Architecture written in Maude by SRI International.
- Maude for Windows, the Maude installer for Windows, and Maude Development Tools, the Maude Eclipse plugin developed by the MOMENT project at Technical University of Valencia (Spain).
[[Kategorie:Logische Programmiersprache]] [[Kategorie:Wikipedia:Seite mit ungeprüften Übersetzungen]]