You will find here the description of my simple term replacement system. It's documentation is mostly in german.

NAME

termreplace - Ein Termersetzungssystem

VERSION

Version 0.1

SYNOPSIS

   $ cat > test.term
   a 2
   b 0

   a(x,b) = x

   ? a(b,b)
   <CTRL-D>

   $ ./termreplace ./test.term

   $ cat test.term | ./termreplace

DESCRIPTION

Dieses Programm liest eine Beschreibung eines Termersetzungssystem ein, bestehend aus einer Signatur, einer Liste von Termersetzungsregeln und Termen die transformiert werden sollen.

Das Eingabeformat ist wie folgt (EBNF):

   Zahl           = ("1" | ... | "9") { ("0" | ... | "9") }
   Zeichen        = "a" | ... | "z" | "A" | ... | "Z" | "0" | ... "9" ;
   Identifier     = Zeichen { Zeichen } ;
   Argumente      = Identifier { "," Identifier } ;
   Term           = Identifier [ "(" Argumente ")" ] ;
   Signatur       = Identifier " " Zahl ;
   Regel          = Term " " "=" " " Term ; 
   Transformation = Term ;

Die Eingabe setzt sich dann mit Zeilenumbrüchen getrennten Regeln, Transformationen und Signaturen zusammen.


Wenn das eingegebene Termersetzungssystem nicht noethersch ist, dann kann es
dazu kommen, dass das Programm in einer Endlosschleife gerät.

EXAMPLE

Hier ein Beispiel um die Ausgabe zu erklären:

   f 1
   b 0
   c 0

   f(b) = c
   f(x) = b

   ? f(f(x))

Wir haben also eine Funktion (f(x)) und zwei Konstanten (b, c). Und 2 Regeln, sowie ein Term der transformiert werden soll.

   $ ./termreplace example.term
   Signature:
      c(0)
      b(0)
      f(1)
   Rules:
      f(b) == c
      f(x) == b
   Terms:
      f(f(c))

   ############################################
   # f(f(c))
   ############################################

   f(f(c))
      * f(x) => b
     -> f(b)
     -> b

   f(b)
      * f(b) => c
     -> c
      * f(x) => b
     -> b

   b
   ============================================
   Transformations:
   > c
   > b

Hier nun eine Detailierte Erklärung der Ausgabe:

Am Anfang sieht man die Eingabe noch einmal Wiederholt, zum kontrollieren:

   Signature:
      c(0)
      b(0)
      f(1)
   Rules:
      f(b) == c
      f(x) == b
   Terms:
      f(f(c))

Danach wird für jeden Term der transformiert werden soll Ein Kopf ausgegeben:

   ############################################
   # f(f(c))
   ############################################

Gefolgt von der Transformation, bei der ein Schritt ca. so aussieht:

   f(b)
      * f(b) => c
     -> c
      * f(x) => b
     -> b

Der Term der am Zeilenanfang steht ist der Term der als naechstes transformiert wird. Danach werden die angewendeten Regeln aufgelistet und das was sie Erzeugen. Dabei ist eine Regelanwendung mit einem * gekennzeichnet und das Resultat der Anwendung mit einem ->.

Nach allen Schritten wird dann das Endresultat ausgegeben, welches aus allen irreduziblen Resultaten besteht:

    ============================================
    Transformations:
    > c
    > b

Im Beispiel war das Termersetzungssystem offenbar nicht konfluent bzw. kanonisch, da man aus f(f(x)) 2 irreduziblen Terme erreichen kann: c und b.

COPYRIGHT & LICENSE

This program is free software; you can redistribute it and/or modify it under the same terms as Perl itself.