Einordnung: die Literatur und Parität mit miniKanren

Smolka und Treinens CFT ("Records for Logic Programming", JLP 1994) ist eine Logik der Records: Bäume, deren Kanten mit Features (Keys) beschriftet sind. Sie hat Feature-Constraints ("y ist das Kind von x bei f"), Aritäts-Constraints ("x hat genau diese Features") und Gleichungen. Erfüllbarkeit ist polynomiell. Es ist das Record-System unter Oz.

Eine offene Map mit festen Keys ist CFT ohne Arität. Eine geschlossene Clojure-Map ist CFT mit Arität. Unser Lacks-Constraint ist CFTs negiertes Feature-Atom. Der Teil des Forks mit festen Keys liegt also in einem polynomiellen Fragment: Die Unifikation zweier offener Maps mit bekannten Keys sollte nie verzweigen. Die Tests des Forks prüfen das jetzt:

(run* [q] (fresh [m1 m2 r1 r2]
            (lmapo m1 {:a 1} r1) (lmapo m2 {:b 2} r2)
            (== m1 m2) (== q m1)))
;;=> ((lmap {:b 2, :a 1} | _0))     ;; one answer, nothing left pending

Unbekannte Keys sind eine andere Geschichte. Treinens "Feature Constraints with First-Class Features" (MFCS 1993) lässt Features Variablen sein. Mit Aritäts-Constraints wird Erfüllbarkeit NP-vollständig. Ohne sie ist sie mit einem einfacheren Algorithmus entscheidbar. Und das ∀∃-Fragment der Theorie erster Stufe ist unentscheidbar.

Das sind genau unsere einfachen Maps mit unbekannten Keys: geschlossen (Arität) plus variable Keys. Das Verzweigen über Paarungen in Teil 2 ist also keine Schwäche der Implementierung. Es ist inhärent, außer P = NP. Die Theorie sagt auch, wann es inhärent ist: erst wenn eine geschlossene Map oder ein Lacks-Constraint die genaue Key-Menge festlegt. Vorher teilt der Fork höchstens in "dieser Key" oder "ein anderer Key" auf und lässt den Rest warten; Paarungen zählt er erst auf, wenn die Key-Menge feststeht.

Aït-Kacis ψ-Terme und OSF-Unifikation (LIFE; Aït-Kaci und Podelski, JLP 1993) ergänzen solche Records um Sorten aus einem Verband und unifizieren, indem sie das Infimum der Sorten nehmen. Das ist die Vorarbeit für die geplanten Records als Typen: Ein Record-Typ sollte eine Sorte sein, kein Key.

Typsysteme für erweiterbare Records haben dasselbe Unifikationsproblem gelöst: Wand (LICS 1987), Rémy (1993), Gaster und Jones (1996), Leijen ("Extensible Records with Scoped Labels", TFP 2005). Row-Unifikation mit festen Labels hat einen einzigen allgemeinsten Unifikator: {l: a | r1} mit {l': b | r2} unifiziert man, indem man ein frisches r3 erfindet. Das lacks-Prädikat von Gaster und Jones ist unser lacks-keyo, mit derselben Propagationsregel.

Die klassische Falle sind zwei Rows mit gemeinsamem Rest: {:a 1 | r} gegen {:b 2 | r} hat keine Lösung, und ein naiver Unifikator erweitert r endlos. Der Fork scheitert sofort daran, und hat jetzt einen Test dafür.

Eine Map ist eine Menge von Paaren, in der keine zwei Paare einen Key teilen. Mengen-Unifikation ist NP-vollständig (Kapur und Narendran, CADE 1986). {log} stellt Mengen mit Rest dar, {x | s}, dieselbe Form wie unsere offenen Maps (Dovier, Omodeo, Pontelli und Rossi, JLP 1996; Dovier, Piazza, Pontelli und Rossi, TOPLAS 2000; und der Überblick von Dovier, Pontelli und Rossi, TPLP 2006). Cristiá, Rossi und Frydman haben partielle Funktionen ergänzt (TPLP 2015), das kommt Maps mit unbekannten Keys am nächsten.

Verschiedene Keys helfen: Der Abgleich zweier geschlossener Maps ist eine Bijektion, also gibt es keine doppelten Antworten der Art, die allgemeine Mengen-Unifikation produziert. Die Tests prüfen jetzt, dass jede Paarung genau einmal herauskommt. Für Sets später lässt sich das Design von {log} direkt übernehmen: Reste, ein ∉-Constraint, und verbleibende Constraints statt Aufzählung.

Die nächste Vorarbeit innerhalb von miniKanren ist ganz neu: {Kanren} (gelesen "set-Kanren") von Sanna, Byrd und Amin ("Beyond Cons: Purely Relational Data Structures", miniKanren Workshop 2025). Es hat Mengen als eigene Werte und Constraints für Assoziationslisten mit Verschattung und Lookup mit Gültigkeitsbereich. Ihr chrKanren (ICLP 2026) baut Constraint Handling Rules in miniKanren ein, mit semantischer Unifikation benutzerdefinierter Daten als Anwendung. Das ist eine Alternative zu den handgeschriebenen Constraints in diesem Fork. Beide stehen auf meiner Leseliste, bevor Vektoren und Sets mehr davon hinzufügen.

Vektoren mit unbekannten Stücken sind Wortgleichungen. Makanin (1977) hat gezeigt, dass sie entscheidbar sind, Plandowski (JACM 2004) hat sie in PSPACE gelegt, und Jeż' Recompression (JACM 2016) hat den Algorithmus einfach gemacht. Nichts davon ist praktikabel innerhalb einer Suche wie der von miniKanren. Kommen Längen-Constraints hinzu, ist die Entscheidbarkeit ein offenes Problem (Ganesh et al., HVC 2012).

Für das Vektor-Design heißt das:

• Eine unbekannte Mitte pro Vektor, und Unifikation, die bekannte Elemente an beiden Enden abschält, ist billig. Zwei verschiedene Mitten, die sich überlappen, sind eine endliche Fallunterscheidung.
• Dieselbe Mitte auf beiden Seiten ist eine echte Wortgleichung: x ++ [1] = [2] ++ x hat keine Lösung, aber das Aufzählen von Längen findet das nie heraus. Die Längen stimmen überein (|x| + 1 auf beiden Seiten), also zeigen nur die Elemente den Konflikt. Eine Relation wie concato kann jede Antwort aufzählen. Sie kann nicht immer in endlicher Zeit scheitern.
• Längenrechnung sollte zuerst laufen: x ++ [1] = [1] ++ x ++ [2] sollte an |x| + 1 ≠ |x| + 2 scheitern, ohne irgendetwas aufzuzählen. Die Forschung empfiehlt, Längen zu FD-Constraints zu machen, statt sie nur aufzuzählen.
• cvc5s Theorie der Sequenzen (Sheng et al., IJCAR 2022) behandelt nth, Update, Länge und Konkatenation zusammen und ist die beste Vorlage für die Vektor-Relationen.

Verglichen mit faster-miniKanren und The Reasoned Schemer (2. Aufl.) ist core.logic voraus bei Tabling, nominaler Logik (αKanren), CLP(FD) und der Faktendatenbank. Es ist gleichauf bei ==, fresh, conde-Interleaving, conda/condu, project, Pattern Matching, Ungleichheit und dem standardmäßigen Occurs Check. Es lag zurück bei diesen Punkten, das Wichtigste zuerst. Der Fork hat alle bis auf den dritten geschlossen:

1. symbolo, numbero, stringo sind keine echten Typ-Constraints. Jetzt sind sie es. Eine eingeschränkte Variable trägt ihren Typ, also scheitert (symbolo x) mit (numbero x), solange x noch ungebunden ist, ebenso die Unifikation einer Symbol-typisierten Variable mit einer Zahl-typisierten.
2. Kein natives absento. (absento t x) wartet jetzt auf jeden ungebundenen Teil von x, und Keys von Maps zählen als Teile.
3. ClojureScript hat überhaupt keine Constraints: kein !=, FD, nominal, Tabling oder Maps. Der cljs-Kern ist eine alte separate Kopie, kein geteilter Code.
4. Kein defrel. defrel definiert eine Relation, deren Rumpf aufgeschoben wird, bis sie durchsucht wird, wie in The Reasoned Schemer.
5. Keine Portierung von faster-miniKanrens Interpreter und Quine-Benchmarks. Der einfache relationale Interpreter läuft jetzt als Test. Er findet die klassische Quine ((lambda (x) (list x (list 'quote x))) '(lambda (x) (list x (list 'quote x)))) in etwa 30 ms und eine Twine in etwa 0,3 s auf der JVM.
6. FD-Domänen werden nicht reifiziert. Mit (fd/residual) in einem run behalten Antworten ihre FD-Variablen ungelabelt und zeigen die Domänen und FD-Constraints, die auf ihnen übrig bleiben, wie Prologs CLP(FD). Eine Antwort kommt nur, wenn Labeling eine Lösung finden würde, denn das Einengen von Domänen allein kann das nicht feststellen.
7. != auf Maps mit unbekannten Keys funktioniert und ist jetzt getestet. Sein verbleibender Constraint hält die beiden Maps als ein Paar zusammen, (!= ({_0 1} {:a 1})), in derselben (!= (lhs rhs))-Form, die core.logic für jede Ungleichheit verwendet.

Was bleibt, ist ClojureScript, beschrieben unter zukünftige Arbeit.

Seitdem läuft faster-miniKanrens eigene Testsuite auf core.logic: 352 von 355 Tests stimmen überein, nachdem sieben Bugs in != und absento behoben wurden, die sie gefunden hat. Siehe Teil 8.

Titel, Autoren, Veröffentlichungsort und Jahr sind geprüft, außer wo (unchecked) steht.

• G. Smolka, R. Treinen, "Records for Logic Programming", J. Logic Programming 18(3), 1994.
• R. Treinen, "Feature Constraints with First-Class Features", MFCS 1993, LNCS 711.
• R. Backofen, G. Smolka, "A complete and recursive feature theory", TCS 146, 1995.
• H. Aït-Kaci, A. Podelski, "Towards a Meaning of LIFE", J. Logic Programming 16(3), 1993.
• M. Wand, "Complete Type Inference for Simple Objects", LICS 1987.
• D. Rémy, "Type Inference for Records in a Natural Extension of ML", in Theoretical Aspects of Object-Oriented Programming, MIT Press, 1993.
• B. R. Gaster, M. P. Jones, "A Polymorphic Type System for Extensible Records and Variants", Tech. rep. NOTTCS-TR-96-3, Nottingham, 1996.
• D. Leijen, "Extensible Records with Scoped Labels", TFP 2005.
• D. Kapur, P. Narendran, "NP-completeness of the set unification and matching problems", CADE-8, 1986.
• A. Dovier, E. G. Omodeo, E. Pontelli, G. Rossi, "{log}: A language for programming in logic with finite sets", J. Logic Programming 28(1), 1996.
• A. Dovier, C. Piazza, E. Pontelli, G. Rossi, "Sets and Constraint Logic Programming", ACM TOPLAS 22(5), 2000.
• A. Dovier, E. Pontelli, G. Rossi, "Set Unification", TPLP 6, 2006.
• M. Cristiá, G. Rossi, C. Frydman, "Adding Partial Functions to Constraint Logic Programming with Sets", TPLP 15, 2015.
• G. S. Makanin, "The problem of solvability of equations in a free semigroup", Math. USSR-Sbornik 32(2), 1977.
• W. Plandowski, "Satisfiability of word equations with constants is in PSPACE", JACM 51(3), 2004.
• A. Jeż, "Recompression: a simple and powerful technique for word equations", JACM, 2016.
• V. Ganesh, M. Minnes, A. Solar-Lezama, M. Rinard, "Word Equations with Length Constraints: What's Decidable?", HVC 2012.
• K. Schulz, "On Existential Theories of List Concatenation", CSL 1994.
• Y. Sheng et al., "Reasoning About Vectors Using an SMT Theory of Sequences", IJCAR 2022.
• C. Alvis et al., "cKanren: miniKanren with Constraints", Scheme Workshop 2011.
• W. E. Byrd, E. Holk, D. P. Friedman, "miniKanren, Live and Untagged: Quine Generation via Relational Interpreters", Scheme Workshop 2012.
• W. E. Byrd, M. Ballantyne, G. Rosenblatt, M. Might, "A Unified Approach to Solving Seven Programming Problems", ICFP 2017.
• D. P. Friedman, W. E. Byrd, O. Kiselyov, J. Hemann, The Reasoned Schemer, 2nd ed., MIT Press, 2018.
• L. Zhang et al., "Neural Guided Constraint Logic Programming for Program Synthesis", NeurIPS 2018.
• D. Rozplokhas, A. Vyatkin, D. Boulytchev, "Certified Semantics for Relational Programming", APLAS 2020.
• A. Sanna, W. E. Byrd, N. Amin, "Beyond Cons: Purely Relational Data Structures", miniKanren Workshop 2025.
• A. Sanna, W. E. Byrd, N. Amin, "chrKanren: Constraint Handling Rules in a Relational Language", ICLP 2026.
• D. Nolen, "Constraints & modes" and "CLP(Set)", core.logic wiki, 2013, https://github.com/clojure/core.logic/wiki.
• Difference lists: L. Sterling, E. Shapiro, The Art of Prolog (unchecked).

Generiert von Claude im Auftrag von Benjamin Schwerdtner.