Alpha - Ein Werkzeug zur Alpha-Vermeidung
Das Tool bietet eine Implementierung eines Alpha-Vermeidungstools, basierend auf der Erkennung von Alpha-Pfaden. Alpha-Pfade bilden eine Adaption legaler Pfade (Asperti und Guerrini, 1999). Das Tool verwendet diese Pfade als Berechnungsgrundlage, um zu entscheiden, ob eine Alpha-Konvertierung in Lambda-Begriffen erforderlich ist, um eine korrekte Beta-Reduktion zu gewährleisten. Abhängig davon, ob solche Pfade gefunden werden können (bis zu einer variablen Tiefe), liefert das Tool eines der folgenden Ergebnisse:
- Alpha-frei: Es wurden keine Alpha-Pfade gefunden und daher ist keine Alpha-Konvertierung erforderlich.
- Alpha kann vermieden werden: Alpha-Pfade wurden gefunden, sind aber entfernbar; In diesem Fall geben die Tools einen Alpha-äquivalenten Term aus, für den die Berechnung alpha-frei ist.
- Alpha ist unvermeidbar: Es wurde ein nicht entfernbarer Alpha-Pfad gefunden. Um die korrekte Umsetzung der Beta-Reduktion zu gewährleisten, ist eine Erfassung unter Vermeidung von Substitution erforderlich.
- möglicherweise, wenn keine Alpha-Pfade gefunden wurden, die Berechnung jedoch nicht abgeschlossen wurde (die maximale Tiefe wurde erreicht). Beachten Sie, dass das Problem grundsätzlich unlösbar ist.
Alpha wird von Mitgliedern der Gruppe Theoretische Informatik entwickelt.
Änderungsprotokoll
2023-02-09: v1.0
Diese Version stellt die erste Version von Alpha vor, einem Tool zur Alpha-Vermeidung, das auf der Berechnung von Alpha-Pfaden basiert. Alpha-Pfade stellen eine Adaption des legalen Pfads dar, um die Variablenerfassung in Lambda-Begriffen zu erkennen; Sie bilden auch eine strenge Verallgemeinerung der für den Mu-Kalkül betrachteten Ketten, vgl. (Endrullis et al. 2011) Das Tool ist über die Befehlszeile oder seine Weboberfläche zugänglich.
Kontakt
Alpha wird derzeit entwickelt von: