Eine Abbildung von Variablen auf Terme, die, auf einen Term oder eine Formel angewandt, jede Variable ihres Definitionsbereichs einheitlich durch den zugehörigen Term ersetzt und sich homomorph auf zusammengesetzte Terme ausdehnt.

Prinzip

Eine Substitution σ = { x1 -> t1, ..., xn -> tn } wird auf Terme durch Ersetzen der Variablen und rekursive Anwendung auf Funktionsargumente erweitert; Komposition und Einschränkung von Substitutionen folgen algebraischen Gesetzen und interagieren kritisch mit Bindung und Variablen-Capture.

Demonstration

Mit σ = { x -> f(a), y -> b } ergibt σ(g(x,y,z)) = g(f(a), b, z). Beim Unifikationsproblem sucht man eine Substitution, die zwei Terme identisch macht, etwa unifiziere f(x,a) und f(b,y) ergibt { x->b, y->a }.

Fehlanwendung

Eine Substitution in Gegenwart von Bindern (z. B. Lambda-Abstraktionen) anzuwenden, ohne gebundene Variablen umzubenennen, führt zu Variable-Capture; anzunehmen, Substitutionskomposition sei kommutativ oder Substitutionen invertierbar ohne Voraussetzungen ist ebenfalls fehlerhaft.

Konsequenz

Substitutionen instantiieren schematische Terme zu konkreten Termen, ermöglichen Unifikation und Matching, treiben Regelanwendung in Rewriting an und sind grundlegend für Inferenzschritte in Logik und automatischem Schließen.

Umkehrung

Betrachte Anti-Substitution oder Musterabstraktion, die eine Substitution extrahiert, durch die ein konkreter Term aus einem Muster entsteht; Anti-Substitution ist oft partiell oder nicht eindeutig, die Umkehrung ist schwieriger als die Vorwärtsanwendung.

Abgrenzung

Definiert für freie Variablen in Termen und Formeln ersten Grades; die Semantik der Substitution muss angepasst oder eingeschränkt werden bei Bindern, höherordentlichen Variablen oder Meta-Variablen, und es ist Vorsicht geboten, um Capture zu vermeiden.

Semantische Spannung

Spannung zwischen syntaktischer Substitution (textuelles Ersetzen in Termen) und semantischer Zuweisung (Mapping von Variablen auf Werte in einem Modell): syntaktische Substitution verändert Termstruktur, semantische Zuweisung betrifft Bewertung und Wahrheit.

Synthese

Eine Substitution ist eine algebraische Abbildung von Variablen auf Terme, homomorph auf zusammengesetzte Ausdrücke erweitert; sie ist der Mechanismus zur Instantiierung von Variablen, bildet die Grundlage von Unifikation und Rewriting und erfordert Capture-vermeidende Disziplin bei Bindern.