Eine entscheidbare Klasse n-stelliger

Horn-Prädikate

Jochen Burghardt GMD, Rudower Chaussee 5, D-12489 Berlin Tel *49-30-6392-1867, Fax -1805, E-Mail jochen@first.gmd. de 

Einleitung

Das Rechnen mit unendlichen Mengen von Grundtermen hat zahlreiche Anwendungen, speziell auf den Gebieten der Programmanalyse und des automatischen Beweisens: z.B. Typ-Inferenz in PROLOG, basierend auf einer oberen Abschätzung der Extension von Prädikaten [9]; Berechnung einfacher Invarianten imperativer Programme [START_REF] Jones | Flow analysis and optimization of LISP-like structures[END_REF]; Beschreibung von Bildmengen von Abstraktionsfunktionen in Implementierungsbeweisen [START_REF]Eine feinkörnige Sortendisziplin und ihre Anwendung in der Programmkonstruktion[END_REF]; Beschreibung der Äquivalenzklassen von Grundtermen für E-Anti-Unifikation [6]; usw.

Allen Anwendungen ist als Mindestanforderung gemeinsam, daß der Durchschnitt zweier darstellbarer Termmengen wieder darstellbar sein muß und daß entscheidbar sein muß, ob eine dargestellte Menge leer ist. In diesem speziellen Sinne wird hier von Entscheidbarkeit gesprochen. Die Leistungsfähigkeit eines Formalismus zur Beschreibung solcher Termmengen hängt entscheidend ab von der Komplexität der Mengen, die er darzustellen in der Lage ist. Der bekannteste Beschreibungsformalismus, reguläre Baumautomaten [START_REF]Equational formulas in order-sorted algebras[END_REF], ist äquivalent zu Hornklauseln mit einstelligen Prädikaten und ausschließlich Variablen als Argumenten im Rumpf, bzw. in der Terminologie von [START_REF]Computational aspects of an order-sorted logic with term declarations[END_REF] zu linearen Termdeklarationen.

In [START_REF] Uribe | Sorted Unification Using Set Constraints[END_REF] werden semi-lineare Termdeklarationen zugelassen, d.h. mehrfache Vorkommen einer Variablen werden erlaubt, sofern die Listen der Funktionssymbole auf den Pfaden von der Wurzel zu den Vorkommen jeweils gleich sind; äquivalent dazu sind reguläre Baumautomaten mit Gleichheitstests für direkte Unterterme [1], für nichtdirekte Unterterme wird die Disjunktheit der Sprachen bereits unentscheidbar [START_REF]Automates avec tests d'égalités entre cousins germains[END_REF].

In [START_REF]Eine feinkörnige Sortendisziplin und ihre Anwendung in der Programmkonstruktion[END_REF] werden reguläre Substitutionsmengen zugelassen, äquivalent dazu sind n-stellige Horn-Prädikate mit linearen Kopftermen f 1 ( x 1 ), . . . , f m ( x m ) und linearen Variablenvektoren x 1 , . . . , x n als Rumpfargumenten, sofern die x i die Zeilen-und die x j die Spaltenvektoren einer verallgemeinerten Matrix bilden. Damit sind auch einfache Relationen wie z.B. x ≤ y für x, y ∈ IN ausdrückbar. Ω-Terme [START_REF]On unification of terms with integer exponents[END_REF] entsprechen speziellen Hornklauselmengen, in denen für jedes Prädikat genau zwei Klauseln existieren, quasi eine für den Basis-und eine für den Rekursionsfall. Durch die starke Einschränkung der möglichen Rekursion auf die Struktur von IN wird es möglich, daß eine beschränkte Anzahl von Variablen beliebig oft und an beliebigen Stellen in beschreibenden Ω-Termen vorkommen darf.

Im folgenden wird ein Ansatz vorgestellt, der auf einer mit der Unifikation kommutierenden Termordnung basiert und teilweise ausdrucksstärker ist als semi-lineare Term-Deklarationen.

Überblick

Sei eine endliche Menge CR von Funktionssymbolen (genauer: Konstruktorsymbolen) mit ihren festen Stelligkeiten und eine unendliche Menge V von Variablen gegeben; sei T die Menge aller Terme über V ∪ CR. Terme werden mit t, t , t i , . . . bezeichnet, Variablen mit x, y, z, . . ., Funktionssymbole mit f, g, . . ., Prädikate mit p, q, . . ., Substitutionen mit β, γ, . . ., t 1 , . . . , t n bezeichnet ein n-Tupel von Termen, vars(t) bezeichnet die Menge aller in t vorkommenden Variablen, dom(β) := {x ∈ V | βx = x} bezeichnet den Definitionsbereich einer Substitution. Substitutionen werden oBdA. stets als idempotent und mit genügend großem Definitionsbereich angenommen, so daß für alle vorkommenden Anwendungen βt stets vars(t) ⊂ dom(β) ist. Bezeichnet β = mgu(t 1 , t 2 ) die unifizierende Substitution für t 1 und t 2 , falls sie existiert, so ist lci(t 1 , t 2 ) = βt 1 = βt 2 die allgemeinste gemeinsame Instanz. Zu einer gegebenen irreflexiven Ordnungsrelation < bezeichnen wir mit ≤ deren reflexive Hülle.

Eine Termmenge wird dargestellt als die Extension eines Prädikats p, das durch ein Horn-Programm der Form 1: Man beachte, daß * nicht gegen beliebige Substitutionen abgeschlossen sein muß. Die Prädikate werden der Einfachheit halber als einstellig geschrieben, Mehrstelligkeit läßt sich leicht durch n-Tupel codieren; in Beispielen verwenden wir dazu ":" als zweistelliges Funktionssymbol niedrigster Priorität. Verlangt man, daß die t ij sämtlich Variablen sein müssen und die t i linear bzw. semi-linear, so erhält man reguläre Baumsprachen bzw. semi-lineare Termdeklarationen.

p 1 (t 1 ) ← p 11 (t 11 ) ∧ . . . ∧ p 1n 1 (t 1n 1 ) . . . p m (t m ) ← p m1 (t m1 ) ∧ . . . ∧ p mnm (t mnm ) 2. t ij * t i für 1 ≤ i ≤ m und 1 ≤ j ≤ n i , 3. dabei
Im folgenden werden die beiden Algorithmen inh zur Entscheidung der Erfüllbarkeit eines Prädikats und inf zur Berechnung der Konjunktion zweier Prädikate vorgestellt. Beide verlangen z.Zt. noch die -starke -Einschränkung n i ≤ 1 für i = 1, . . . , m.

Algorithmus 3 (Erfüllbarkeit: inh)

Sei ein Horn-Programm wie in 1 gegeben, wobei als zusätzliche Einschränkung n i ≤ 1 für i = 1, . . . , m sei. inh ∨ (p t , {}) liefert true genau dann, wenn das Prädikat p durch eine Instanz des Terms t erfüllbar ist. Algorithmus 4 (Konjunktion: inf ) Sei ein Horn-Programm wie in 1 gegeben, mit den zusätzlichen Einschränkungen Induktion über die Indirektionsstufe des aktuellen Aufrufs: Für den ersten Aufruf von inh ist nichts zu zeigen. Fallunterscheidung, durch welche Regel des Algorithmus 3 der aktuelle Aufruf entstanden ist:

1. inh ∨ (p t , Occ) ⇔ inh ∧ (p β 1 t 1 1 , Occ) ∨ . . . ∨ inh ∧ (p β k t k k , Occ) ( * 1) 2. inh ∧ (p t , Occ) ⇔ f alse für p t ∈ Occ, ( * 2) 3. inh ∧ (p β i t i i , Occ) ⇔ inh ∨ (p β i t i1 i1 , Occ ∪ {p β i t i i }) für n i = 1, 4. inh ∧ (p β i t i i , Occ) ⇔ true für n i = 0 ( * 
• n i ≤ 1 für i = 1, . . . , m und • t i1 , t i 1 * t i , t i für alle i, i ∈ {1, . . . ,
1.

β i t i = lci(t , t i ) nach ( * 1) zu 3.1 ∈ lci • lci • less({t 1 , . . . , t m , t }) nach Induktionsvoraussetzung = lci • less({t 1 , . . . , t m , t })
da lci idempotent 2.,4. Es entsteht kein neuer Aufruf.

3.

β i t i1 ∈ less • lci • less({t 1 , . . . , t m , t }) nach I.V., da β i t i1 * β i t i ⊂ lci • less • less({t 1 , . . . , t m , t }) nach 2.4, s.o. = lci • less({t 1 , . . . , t m , t })
da less idempotent Also treten nur endlich viele verschiedene "Exponenten" auf; wegen der Regel 3.2 wird inh nie zweimal mit demselben Argument (mod. Umbenennung) aufgerufen, so daß der Algorithmus terminiert. Die Terminierung von inf ist trivial.

Beispiel 6 0 und s seien null-bzw. einstellige Konstruktoren. Gegebene Klauseln: 1. p(ssx : sy) ← p(sx : y) 2. p(x : 0) 3. q(sx : sx) ← q(x : x) 4. q(0 : x)

Berechnung der Konjunktion von p und q nach Algorithmus 4: 5. pq(ssx : ssx) ← pq(sx : sx) aus 1. und 3. 6. pq(0 : 0) aus 2. und 4.

Es gilt pq(x : y) ⇔ p(x : y) ∧ q(x : y); die Erfüllbarkeit von pq ist wegen 6. trivial.

Feststellung der Unerfüllbarkeit von pq(ssx : ssx) nach Algorithmus 3: inh ∨ (pq ssx:ssx , {}) ⇔ inh ∧ (pq ssx:ssx , {}) Regel 3.1 ⇔ inh ∨ (pq sx:sx , {pq ssx:ssx }) Regel 3.3 ⇔ inh ∧ (pq ssx:ssx , {pq ssx:ssx }) Regel 3 

Terme als Pfadmengen mit Kongruenzrelationen

Sei "." eine assoziative Operation mit "ε" als neutralem Element. Die Menge P aller markierten Baumpfade ist definiert als kleinste Menge mit folgenden Eigenschaften: ε ∈ P f ∈ P falls f ∈ CR nullstellig f.i.p ∈ P falls f ∈ CR n-stellig, i ∈ {1, . . . , n}, p ∈ P Die Menge paths(t) aller (Teil-)Pfade eines Terms t ist definiert durch:

paths(x) = {ε} für x ∈ V paths(f ) = {f, ε} für f ∈ CR nullstellig paths(f (t 1 , . . . , t n )) = {f.i.p | p ∈ paths(t i ), 1 ≤ i ≤ n} ∪ {ε} für f ∈ CR n-stellig
Pfade werden mit p, p , p i , q, . . . bezeichnet, aus dem Zusammenhang wird stets klar, ob etwa p einen Pfad oder ein Prädikat meint. Für p 1 , p 2 ∈ P definiere p.f.i sibl p.f.j für alle p, f n-stellig, 

t/ ε = t f (t 1 , . . . , t n )/ f.i.p = t i / p für 1 ≤ i ≤ n
Zu gegebenem Term t definiere (≡ t ) als die kleinste Kongruenzrelation auf P mit ∀p 1 , p 2 ∈ P p 1 ≡ t p 2 ⇔ t/ p 1 = t/ p 2 , wobei rechts syntaktische Gleichheit steht (nicht mod. Umbenennung). (≡ t ) muß mit "." verträglich sein in folgendem Sinne: p 1 ≡ t p 2 ⇒ p 1 .p ≡ t p 2 .p. Für eine beliebige Relation (R) ⊂ P × P sei c rf (R) der reflexive, c sm (R) der symmetrische und c tr (R) der transitive Abschluß von (R); für eine Kongruenzrelation (≡) definiere darüber hinaus die folgenden Abschlußoperationen, wobei P ⊂ P sei:

c mx (≡) := (≡) ∪ { p 1 , p 2 | p 1 .f.i ≡ p 2 .f.i für alle i = 1, . . . , n, f n-stellig, } c ∞ mx (≡) := i∈IN c i mx (≡) c (≡) (P ) := {p 1 | p 1 ≡ p 2 ∈ P }
Eine Substitution β heißt linear, wenn β x 1 , . . . , x n linearer Term ist, wobei dom(β) = {x 1 , . . . , x n } sei. Eine Substitution β heißt flach, wenn βx ∈ V für alle x ∈ dom(β). Eine lineare und flache Substitution heißt Umbenennungssubstitution. Jede Substitution β läßt sich in eine flache und eine lineare Substitution zerlegen:

β = β 1 • β 2 mit β 1 flach und β 2 linear.

Satz 7

Zu P ⊂ P und (≡) Kongruenzrelation auf P gibt es einen Term t mit paths(t) = P und (≡ t ) = (≡) genau dann, wenn

Streichungen in Pfaden

Mit der Termdarstellung aus Abschnitt 3 kann nun eine Ordnung auf Termen definiert werden, die die Anforderungen aus Definition 2 erfüllt.

Eine Streichung ist ein Paar von Pfaden, geschrieben q ← q.q . Definiere die Ausführung der Streichung durch: 1. del(q ← q.q , p)

= {p} falls q pr/ ef p 2. del(q ← q.q , q.p) = {} falls q.q pr/ ef q.p 3. del(q ← q.q , q.q .p) = {q.p} sonst 1.

3.

q q 1. 2. 3. c c & & & a & & & a
del(q ← q.q , p) liefert eine maximal einelementige Pfadmenge. Für eine Pfadmenge P definiere del(q ← q.q , P ) := p∈P del(q ← q.q , p); für eine Folge von Streichungen S = q 1 ← q 1 .q 1 , . . . , q n ← q n .q n definiere del(S, P ) := del(q n ← q n .q n , . . . del(q 1 ← q 1 .q 1 , P ) . . .). Es gilt stets del(S, p 1 ) = del(S, p 2 ) = {} ⇒ p 1 = p 2 .

Eine Streichungsfolge S auf P ⊂ P heißt verträglich mit einer Kongruenzrelation (≡) genau dann, wenn del(S, p 1 ) = {} ⇔ del(S, p 2 ) = {} für alle p 1 ≡ p 2 ist. In diesem Fall definiere

p 1 ≡ S p 2 :⇔ p 1 ≡ p 2 für del(S, p 1 ) = {p 1 } und del(S, p 2 ) = {p 2 }, sowie del(S, (≡)) := c ∞ mx (≡ S ).
Ist S verträglich mit (≡ t ), so gibt es genau ein t mit

• paths(t ) = del(S, paths(t)),

• (≡ t ) = del(S, (≡ t )) und

• t / p = t/ p für alle p ∈ paths(t) mit t/ p ∈ V und del(S, p) = {p }.

Definiere del(S, t) := t sowie t t :⇔ ∃S t = del(S, t).

Die Wohlfundiertheit von ≺ folgt daraus, daß ≺ eine Unterrelation der Einbettungsordnung nach [START_REF] Computation And Deduction | International Summer School on Logic of Programming and Calculi of Discrete Design[END_REF] ist. Auf der Menge der linearen Terme sind beide Ordnungen identisch. Abbildung 1 zeigt in der linken, mittleren und rechten Spalte jeweils eine Anwendung von del(f.3 ← f.3.g 3 .1, . . .).

Satz 12

Zu t t = lci(t 1 , . . . , t n ) existieren t 1 t 1 , . . . , t n t n mit t = lci(t 1 , . . . , t n ). Siehe Beispiel in Abbildung 1.

Für t = del(S, t) ist nicht immer βt = del(S, βt), sondern nur dann, wenn S nicht nur mit (≡ t ), sondern darüber hinaus auch mit (≡ βt ) verträglich ist. Zur Sicherstellung der Forderung 2.5 verlangen wir daher die Existenz einer globalen Kongruenzrelation ( * ≡) mit folgenden Eigenschaften: In Beispiel 6 wird ( * ≡) induziert von (: .1) * ≡ (: .2), und die einzige vorkommende Streichungsfolge ist (: .1) ← (: .1.s.1), (: .2) ← (: .2.s.1) . An einer hinreichenden Bedingung für 13.2, die die konstruktive Berechnung von ( * ≡) aus den in einem gegebenen Horn-Programm vorkommenden (≡ t i ) und (≡ t ij ) erlaubt, wird z.Zt. gearbeitet.

f g 1 x 2 x 2 x 1 d d •••••••• f g 1 g 2 g 2 x 1 g 1 g 1 x 1 x 1 d d • • • • • • • • • • • • •••••••• • • • • • • • • • • • • •••••••• •••••••• f x 3 g 2 x 4 x 3 d d • • • • • • • • • • • • f g 1 x 2 g 3 x 1 x 2 d d • • • • • • • • • • • • f g 1 g 2 g 3 x 1 g 1 g 2 x 1 g 1 x 1 d d • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • f x 3 g 2 x 4 x 3 d d • • • • • • • • • • • • c less c less c less E lci ' lci E lci ' lci Abbildung 

Ausblick

Darüber hinaus scheint es interessant, die sich aus Definition 2 ergebenden Forderungen an * zunächst abstrakt zu formulieren und weitere konkrete "Implementierungen" von * zu untersuchen. In diesem Zusammenhang werden Abbildungen ϕ : T → T untersucht, für die gilt ϕ(lci(t 1 , t 2 )) = lci(ϕ(t 1 ), ϕ(t 2 )) und ϕ(t) ≤ t bzgl. einer beliebigen Wohlordnung < Eine solche Abbildung ist durch ihr Verhalten auf T 1 ∪ T 2 schon eindeutig bestimmt, wobei 

••••••••••••••••••••• • • • • • • • •

  1): Dabei seien oBdA. p 1 = . . . = p k = p sämtliche Klauselköpfe für p, für die β i := mgu(t , t i ) existiert. ( * 2): Der Test muß mod. gebundener Umbenennung durchgeführt werden.

  .1 ⇔ f alse Regel 3.2 Im folgenden wird eine konkrete Ordnung * ≺ konstruiert, die die Bedingungen aus Definition 2 erfüllt. Dazu wird in Abschnitt 3 zunächst eine Termdarstellung eingeführt, die invariant gegen gebundene Umbenennung ist und jeden Term durch seine Baumpfade und die Kongruenzrelation gleicher Unterterme (insbesondere Variablen) repräsentiert.

T 1 :

 1 = {t ∈ T | ∃p ∈ P paths(t) = c sibl • pref ({p})} und T 2 := {t ∈ T | ∃p 1 = p 2 ∈ P paths(t) = c sibl • pref ({p 1 , p 2 }), (≡ t ) = c sm • c rf ({ p 1 , p 2 })} .Auf Seite 10 sind zwei Elemente von T 1 bzw.

  Seien zwei Prädikate p i 1 , p i 2 gegeben. Der Algorithmus führt einen neuen Prädikatnamen ein, der hier mit p i 1 p i 2 bezeichnet wird, und definiert neue Klauseln dafür, so daß p i 1 p i 2 (x) ⇔ p i 1 (x) ∧ p i 2 (x) wird: Für alle Klauseln 2 von p i 1 und p i 2 , für die t i 1 und t i 2 etwa durch β unifizierbar sind, definiere eine neue Klausel p i 1 p i 2 (βt i 1 ) ← p i 1 1 p i 2 1 (βt i 1 1 ). Verfahre in der gleichen Weise mit p i 1 1 p i 2 1 , usw.Die partielle Korrektheit der beiden Algorithmen ist jeweils relativ leicht zu zeigen, indem die in[START_REF]Eine feinkörnige Sortendisziplin und ihre Anwendung in der Programmkonstruktion[END_REF] für reguläre Baumsprachen angewandte Methodik entsprechend verallgemeinert wird; statt der Termstruktur dient jetzt die Wohlordnung * ≺ als Grundlage für die Induktionsbeweise, Einzelheiten werden in[START_REF]A decidable class of n-ary Horn predicates[END_REF] ausgeführt. Ohne die Einschränkung n i ≤ 1 müßte Regel 3.3 lauten inh ∧ (p β i t i

m} (als Verschärfung von 2.2). i , Occ) ⇔ inh ∨ (p β i t i1 i1 , Occ ) ∧ . . . ∧ inh ∨ (p

β i t in i in i , Occ ) für n i > 0

und es müßte sichergestellt werden, daß β i t i1 , . . . , β i t in i paarweise disjunkte Variablen haben. Z.Zt. wird untersucht, unter welchen Voraussetzungen die Bedingung n i ≤ 1 fallengelassen werden kann. Damit könnte der vorgestellte Ansatz u.U. eine echte Obermenge der semi-linearen Termdeklarationen abdecken.

Für die Terminierungsbeweise definieren wir für T ⊂ T :

1. lci(T ) := {lci(t 1 , . . . , t n ) | t 1 , . . . , t n ∈ T, lci(t 1 , . . . , t n ) existiert},

2. less(T

) := {t | t * t ∈ T },

Für T endlich ist lci(T ) und wegen 2.3 auch less(T ) endlich, also auch lci • less(T ). Aus 2.4 folgt sofort, daß less • lci(T ) ⊂ lci • less(T ). Damit gilt: Lemma 5 Wird inh ∨ (p t , Occ) oder inh ∧ (p t , Occ) direkt oder indirekt von inh ∨ (q t , {}) aufgerufen, so gilt t ∈ lci • less({t 1 , . . . , t m , t }).

  1 ≤ i, j ≤ n p pref p.p für alle p, p (Gleichheit mod. Assoziativität und Neutralität) Z.B. für + zweistellig und s einstellig ist s.1 pref s.1. + .1, aber nicht s pref s.1. + .1 Definiere den Unterterm t/ p eines Terms t am Ende eines Pfads p ∈ paths(t) durch:

  1: Beispiel zu Satz 12 für alle 1 ≤ i, i ≤ m. Man beachte, daß ( * ≡) i.allg. nicht als (≡ t ) für irgend einen Term t darstellen läßt. nach Induktionsvoraussetzung, damit ist nach 13.2 auch (≡ β i t i1 ) ⊂ (

	Definition 13		
	1. ( ≡) ist maximal im Sinne von 7.6, d.h. abgeschlossen gegen c mx , *
	2. ( ≡) ist abgeschlossen gegen konsistente Streichungen, *
	d.h. für (≡ Definition 14 Wir definieren t mit ( * ≡) verträgliche Streichungsfolge S gibt, so daß t = del(S, t). * t genau dann, wenn (≡ t ) ⊂ ( ≡) ist und es eine *
	Als Unterrelation von ≺ ist	* ≺ ebenfalls Wohlordnung, und Satz 12 folgt leicht auch
	für	*	. Damit erfüllt	*	alle Forderungen aus Definition 2, wobei 2.5 präzisiert wird zu
	2.5':			t	

t ) ⊂ ( * ≡) und S verträglich mit ( * ≡) ist auch (≡ del(S,t) ) ⊂ ( * ≡).

Von einem wie in 1 gegebenen Horn-Programm verlangen wir, daß (≡

t i , t i ) ⊂ ( * ≡) und (≡ t i ) ⊂ ( * ≡) * t ∧ (≡ βt ) ⊂ ( * ≡) ⇒ βt * βt.

Die dadurch in den

Terminierungsbeweisen zusätzlich notwendigen Voraussetzungen kann man mit Hilfe von Satz 11 leicht zeigen; etwa in der zweiten Zeile von Fall 3. im Beweis von Lemma 5 ist (≡ β i t i ) ⊂ ( * ≡), da (≡ t i ) ⊂ ( * ≡) und (≡ t ) ⊂ ( * ≡) * ≡).

  T 2 skizziert. lci(T 1 ) ist gerade die Menge aller linearen Terme; und lci(T 1 ∪T 2 ) = T . Für lci(t 1 , t 2 ) = t ∈ T 1 ∪T 2 muß schon t = t 1 oder t = t 2 bis auf Umbenennung sein. Es gibt eine notwendige und hinreichende Bedingung dafür, daß sich eine vorgegebene Zuordnung t 1 → t 11 , . . . , t m → t m1 zu einer Abbildung ϕ mit den obigen Eigenschaften fortsetzen läßt. Damit läßt sich * allgemeiner als in Def. 14 definieren durch t * t :⇔ ∃ϕ t = ϕ(t); und es können auch noch Horn-Programme wie das für reverse behandelt werden, in denen beim Übergang vom Kopf zum Rumpf Konstruktorsymbole von einem Argument in ein anderes (lexikographisch nachrangiges) geschoben werden.

Diese Einschränkung wird später formal präzisiert, vgl. Definition 14 ff.

OBdA. werden hier nur die Klauseln i 1 und i 2 selbst betrachtet.