Hornlogik-Programme mit definierten Funktionen 1. Ordnung und
typisierenden Termen 1. Klasse

Harold Boley



Funktionssymbole sind in hornlogischen Programmiersprachen 'frei'
(Funktoren, Konstruktoren); fuer viele Problemstellungen bieten sich
aber zusaetzlich definierte Funktionen wie in gleichungsbasierten
bzw. funktionalen Programmiersprachen an. Obwohl zur Argumentauswertung
Call-by-Need ('Lazy Evaluation') gewisse theoretische Vorteile hat,
benutzen die in der Praxis meistverbreiteten funktionsbasierten
Programmiersprachen (ANSI COMMON LISP, Standard ML) Call-by-Value
('Eager Evaluation'). Fuer die Integration von 'Eager'-Funktionen
1. Ordnung in Hornlogik-Programme gibt es eine nauerliche Semantik:
Verallgemeinerte Herbrandmodelle, die neben ungerichteten Elementen fuer
Relationen auch gerichtete fuer Funktionen enthalten. Nicht-Lambda-
Funktionen in der Notation hoeherer Ordnung koennen auf solche
Funktionen 1. Ordnung reduziert werden.

Die Typisierung logischer Variablen kann als ihre Initialisierung mit
typisierenden Termen aufgefasst werden.  Da logische Variablen-
zuweisungen fruehere Werte nicht beliebig aendern sondern nur
spezialisieren koennen, lassen sich durch vorhandene 'Typwerte' spaetere
'Datenwerte' pruefen. Beispiele fuer typisierende Terme sind endliche
Domaenen, endliche Exklusionen und Sorten. Die Unifikation einer
Konstanten mit einer endlichen Domaene (Exklusion) prueft, ob die
Konstante Element (nicht Element) der Domaene (Exklusion) ist.  Sorten
werden als ausgezeichnete unaere Praedikate aufgefasst, die bei der
Typpruefung auf Konstanten angewandt werden. Die Unifikation zweier
Domaenen (Exklusionen, Sorten) liefert deren Schnitt-Domaene
(Vereinigungs-Exklusion, glb-Sorte). Solche Typen sind Terme 1. Klasse
('1st-class citizens'), die anonym, als Variablenwerte und als
Rueckgabewerte definierter Funktionen auftreten koennen.