From d702b9b08140a78cbbe6ead928712b9301113c7a Mon Sep 17 00:00:00 2001 From: Tibo De Peuter Date: Sun, 6 Apr 2025 14:42:57 +0200 Subject: [PATCH] Checkpoint --- src/prolog/builtins/control.kt | 30 ++++++++++------ src/prolog/builtins/other.kt | 3 +- src/prolog/components/Program.kt | 13 ++++--- src/prolog/components/Provable.kt | 10 +++++- src/prolog/components/Resolvent.kt | 9 ++++- src/prolog/components/expressions/Clause.kt | 31 +++++++++-------- src/prolog/components/expressions/Operator.kt | 5 +-- .../components/expressions/Predicate.kt | 9 +++-- src/prolog/components/terms/Atom.kt | 4 ++- src/prolog/components/terms/Goal.kt | 3 +- src/prolog/components/terms/Structure.kt | 7 ++-- src/prolog/unify.kt | 19 +++++++---- tests/prolog/EvaluationTest.kt | 34 ++++++++++--------- 13 files changed, 114 insertions(+), 63 deletions(-) diff --git a/src/prolog/builtins/control.kt b/src/prolog/builtins/control.kt index f90106c..e8dc1f6 100644 --- a/src/prolog/builtins/control.kt +++ b/src/prolog/builtins/control.kt @@ -1,15 +1,18 @@ package prolog.builtins +import prolog.Substitution import prolog.components.expressions.Operand import prolog.components.expressions.Operator import prolog.components.terms.Atom import prolog.components.terms.Body +import prolog.components.terms.Term +import prolog.components.terms.Variable /** * Always fail. */ class Fail: Atom("fail"), Body { - override fun prove(): Boolean = false + override fun prove(): Sequence = emptySequence() } /** @@ -21,7 +24,7 @@ typealias False = Fail * Always succeed. */ class True: Atom("true"), Body { - override fun prove(): Boolean = true + override fun prove(): Sequence = sequenceOf(emptyMap()) } // TODO Repeat/0 @@ -32,10 +35,16 @@ class True: Atom("true"), Body { * Conjunction (and). True if both Goal1 and Goal2 are true. */ class Conjunction(leftOperand: Operand, rightOperand: Operand) : Operator(Atom(","), leftOperand, rightOperand) { - override fun prove(): Boolean { - val left = leftOperand?.prove() ?: true - val right = rightOperand.prove() - return left && right + override fun prove(): Sequence = sequence { + if (leftOperand != null) { + leftOperand.prove().forEach { left -> + rightOperand.prove().forEach { right -> + yield(left + right) + } + } + } else { + yieldAll(rightOperand.prove()) + } } } @@ -43,9 +52,10 @@ class Conjunction(leftOperand: Operand, rightOperand: Operand) : Operator(Atom(" * Disjunction (or). True if either Goal1 or Goal2 succeeds. */ class Disjunction(leftOperand: Operand, rightOperand: Operand) : Operator(Atom(";"), leftOperand, rightOperand) { - override fun prove(): Boolean { - val left = leftOperand?.prove() ?: false - val right = rightOperand.prove() - return left || right + override fun prove(): Sequence = sequence { + if (leftOperand != null) { + yieldAll(leftOperand.prove()) + } + yieldAll(rightOperand.prove()) } } diff --git a/src/prolog/builtins/other.kt b/src/prolog/builtins/other.kt index 5cae935..815dfdb 100644 --- a/src/prolog/builtins/other.kt +++ b/src/prolog/builtins/other.kt @@ -1,9 +1,10 @@ package prolog.builtins +import prolog.Substitution import prolog.components.expressions.Operand import prolog.components.expressions.Operator import prolog.components.terms.Atom class Query(rightOperand: Operand) : Operator(Atom("?-"), null, rightOperand) { - override fun prove(): Boolean = rightOperand.prove() + override fun prove(): Sequence = rightOperand.prove() } diff --git a/src/prolog/components/Program.kt b/src/prolog/components/Program.kt index 4d8fff4..33fe47e 100644 --- a/src/prolog/components/Program.kt +++ b/src/prolog/components/Program.kt @@ -1,5 +1,6 @@ package prolog.components +import prolog.Substitution import prolog.builtins.True import prolog.components.expressions.Clause import prolog.components.expressions.Fact @@ -24,16 +25,20 @@ object Program: Resolvent { )) } - fun query(goal: Goal): Boolean { + /** + * Queries the program with a goal. + * @return true if the goal can be proven, false otherwise. + */ + fun query(goal: Goal): Boolean = solve(goal).any() + + override fun solve(goal: Goal): Sequence { val functor = goal.functor // If the predicate does not exist, return false - val predicate = predicates[functor] ?: return false + val predicate = predicates[functor] ?: return emptySequence() // If the predicate exists, evaluate the goal against it return predicate.solve(goal) } - override fun solve(goal: Goal): Boolean = query(goal) - /** * Loads a list of clauses into the program. */ diff --git a/src/prolog/components/Provable.kt b/src/prolog/components/Provable.kt index 9480b53..fd0ed7b 100644 --- a/src/prolog/components/Provable.kt +++ b/src/prolog/components/Provable.kt @@ -1,5 +1,13 @@ package prolog.components +import prolog.Substitution + interface Provable { - fun prove(): Boolean + /** + * Proves the current [Provable] instance. + * + * @return a sequence of [Substitution] instances representing the results of the proof. + * If the proof fails, an empty sequence is returned. + */ + fun prove(): Sequence } diff --git a/src/prolog/components/Resolvent.kt b/src/prolog/components/Resolvent.kt index 582c5ea..bb87b3a 100644 --- a/src/prolog/components/Resolvent.kt +++ b/src/prolog/components/Resolvent.kt @@ -1,10 +1,17 @@ package prolog.components +import prolog.Substitution import prolog.components.terms.Goal /** * Can be instructed to solve a goal. */ interface Resolvent { - fun solve(goal: Goal): Boolean + /** + * Attempts to solve the given goal. + * + * @return A sequence of substitutions that can be applied to the goal to unify it with this resolvent. + * If the goal cannot be unified with this resolvent, an empty sequence is returned. + */ + fun solve(goal: Goal): Sequence } diff --git a/src/prolog/components/expressions/Clause.kt b/src/prolog/components/expressions/Clause.kt index b2e58b3..4113e3e 100644 --- a/src/prolog/components/expressions/Clause.kt +++ b/src/prolog/components/expressions/Clause.kt @@ -1,8 +1,9 @@ package prolog.components.expressions +import prolog.Substitution import prolog.components.Resolvent import prolog.components.terms.* -import prolog.unify +import prolog.unifyLazy /** * ‘Sentence’ of a Prolog program. @@ -15,20 +16,22 @@ import prolog.unify abstract class Clause(private val head: Head, private val body: Body? = null) : Resolvent { val functor: Functor = head.functor - override fun solve(goal: Goal): Boolean { - val unification = unify(goal, head) - - if (unification.isEmpty) { - return false + override fun solve(goal: Goal): Sequence = sequence { + if (body == null) { + // If the clause is a fact, unify the goal with the head, and return the substitutions. + // Do this in a lazy way. + yieldAll(unifyLazy(goal, head)) + } else { + // If the clause is a rule, unify the goal with the head and then try to prove the body. + // Only if the body can be proven, the substitutions should be returned. + // Do this in a lazy way. + unifyLazy(goal, head).forEach { subs -> + // If the body can be proven, yield the (combined) substitutions + body.prove().forEach { bodySubs -> + yield(subs + bodySubs) + } + } } - - val substitutions = unification.get() - - val proven = body == null || body.prove() - - substitutions.forEach { (variable, _) -> variable.unbind() } - - return proven } override fun toString(): String { diff --git a/src/prolog/components/expressions/Operator.kt b/src/prolog/components/expressions/Operator.kt index 272d781..e991dee 100644 --- a/src/prolog/components/expressions/Operator.kt +++ b/src/prolog/components/expressions/Operator.kt @@ -1,5 +1,6 @@ package prolog.components.expressions +import prolog.Substitution import prolog.components.Provable import prolog.components.terms.Atom import prolog.components.terms.CompoundTerm @@ -8,11 +9,11 @@ import prolog.components.terms.Goal typealias Operand = Goal abstract class Operator( - val symbol: Atom, + private val symbol: Atom, val leftOperand: Operand? = null, val rightOperand: Operand ) : CompoundTerm(symbol, listOfNotNull(leftOperand, rightOperand)), Provable { - abstract override fun prove(): Boolean + abstract override fun prove(): Sequence override fun toString(): String { return when (leftOperand) { diff --git a/src/prolog/components/expressions/Predicate.kt b/src/prolog/components/expressions/Predicate.kt index b7b1bd0..eebd224 100644 --- a/src/prolog/components/expressions/Predicate.kt +++ b/src/prolog/components/expressions/Predicate.kt @@ -1,5 +1,6 @@ package prolog.components.expressions +import prolog.Substitution import prolog.components.Resolvent import prolog.components.terms.Functor import prolog.components.terms.Goal @@ -48,8 +49,12 @@ class Predicate : Resolvent { this.clauses.addAll(clauses) } - override fun solve(goal: Goal): Boolean { + override fun solve(goal: Goal): Sequence = sequence { require(goal.functor == functor) { "Goal functor does not match predicate functor" } - return clauses.any { it.solve(goal) } + for (clause in clauses) { + // Try to unify the goal with the clause + // If the unification is successful, yield the substitutions + yieldAll(clause.solve(goal)) + } } } diff --git a/src/prolog/components/terms/Atom.kt b/src/prolog/components/terms/Atom.kt index 4b8df24..faf1e9e 100644 --- a/src/prolog/components/terms/Atom.kt +++ b/src/prolog/components/terms/Atom.kt @@ -1,12 +1,14 @@ package prolog.components.terms +import prolog.Substitution import prolog.components.Resolvent import prolog.unify +import prolog.unifyLazy open class Atom(val name: String) : Goal(), Head, Body, Resolvent { override val functor: Functor = "$name/_" - override fun solve(goal: Goal): Boolean = unify(goal, this).isEmpty + override fun solve(goal: Goal): Sequence = unifyLazy(goal, this) override fun toString(): String { return name diff --git a/src/prolog/components/terms/Goal.kt b/src/prolog/components/terms/Goal.kt index 352d4c0..4120241 100644 --- a/src/prolog/components/terms/Goal.kt +++ b/src/prolog/components/terms/Goal.kt @@ -1,5 +1,6 @@ package prolog.components.terms +import prolog.Substitution import prolog.components.Program import prolog.components.Provable @@ -13,5 +14,5 @@ import prolog.components.Provable abstract class Goal : Term, Provable { abstract val functor: Functor - override fun prove(): Boolean = Program.query(this) + override fun prove(): Sequence = Program.solve(this) } diff --git a/src/prolog/components/terms/Structure.kt b/src/prolog/components/terms/Structure.kt index 706dcd4..8965313 100644 --- a/src/prolog/components/terms/Structure.kt +++ b/src/prolog/components/terms/Structure.kt @@ -1,15 +1,16 @@ package prolog.components.terms +import prolog.Substitution import prolog.components.Resolvent -import prolog.unify +import prolog.unifyLazy typealias Argument = Term open class Structure(val name: Atom, val arguments: List): Goal(), Head, Body, Resolvent { override val functor: Functor = "${name.name}/${arguments.size}" - override fun solve(goal: Goal): Boolean { - return unify(goal, this).isEmpty + override fun solve(goal: Goal): Sequence { + return unifyLazy(goal, this) } override fun toString(): String { diff --git a/src/prolog/unify.kt b/src/prolog/unify.kt index a49b2a3..f97b063 100644 --- a/src/prolog/unify.kt +++ b/src/prolog/unify.kt @@ -11,7 +11,7 @@ import java.util.* typealias Substitution = Map // Apply substitutions to a term -fun applySubstitution(term: Term, substitution: Substitution): Term = when { +private fun applySubstitution(term: Term, substitution: Substitution): Term = when { variable(term) -> (term as Variable).alias().map { applySubstitution(it, substitution) }.orElse(term) atomic(term) -> term compound(term) -> { @@ -22,7 +22,7 @@ fun applySubstitution(term: Term, substitution: Substitution): Term = when { } // Check if a variable occurs in a term -fun occurs(variable: Variable, term: Term): Boolean = when { +private fun occurs(variable: Variable, term: Term): Boolean = when { variable(term) -> term == variable atomic(term) -> false compound(term) -> { @@ -33,7 +33,7 @@ fun occurs(variable: Variable, term: Term): Boolean = when { } // Generate possible substitutions -fun generateSubstitutions(term1: Term, term2: Term, substitution: Substitution): Sequence = sequence { +private fun generateSubstitutions(term1: Term, term2: Term, substitution: Substitution): Sequence = sequence { val t1 = applySubstitution(term1, substitution) val t2 = applySubstitution(term2, substitution) @@ -42,15 +42,17 @@ fun generateSubstitutions(term1: Term, term2: Term, substitution: Substitution): variable(t1) -> { val variable = t1 as Variable if (!occurs(variable, t2)) { - variable.bind(t2) +// variable.bind(t2) yield(substitution + (variable to t2)) +// variable.unbind() } } variable(t2) -> { val variable = t2 as Variable if (!occurs(variable, t1)) { - variable.bind(t1) +// variable.bind(t1) yield(substitution + (variable to t1)) +// variable.unbind() } } compound(t1) && compound(t2) -> { @@ -68,8 +70,11 @@ fun generateSubstitutions(term1: Term, term2: Term, substitution: Substitution): } // Unify two terms with backtracking and lazy evaluation -fun unifyLazy(term1: Term, term2: Term, substitution: Substitution = emptyMap()): Sequence { - return generateSubstitutions(term1, term2, substitution) +fun unifyLazy(term1: Term, term2: Term, substitution: Substitution = emptyMap()): Sequence = sequence { + generateSubstitutions(term1, term2, substitution).forEach { newSubstitution -> + // Return the new substitution + yield(newSubstitution) + } } fun unify(term1: Term, term2: Term): Optional { diff --git a/tests/prolog/EvaluationTest.kt b/tests/prolog/EvaluationTest.kt index fd1e522..d9e8ee7 100644 --- a/tests/prolog/EvaluationTest.kt +++ b/tests/prolog/EvaluationTest.kt @@ -1,7 +1,6 @@ package prolog -import org.junit.jupiter.api.Assertions.assertFalse -import org.junit.jupiter.api.Assertions.assertTrue +import org.junit.jupiter.api.Assertions.* import org.junit.jupiter.api.BeforeEach import org.junit.jupiter.api.Test import prolog.builtins.Conjunction @@ -11,6 +10,7 @@ import prolog.components.expressions.Fact import prolog.components.expressions.Rule import prolog.components.terms.Atom import prolog.components.terms.Structure +import prolog.components.terms.Variable class EvaluationTest { @BeforeEach @@ -23,7 +23,9 @@ class EvaluationTest { val fact = Fact(Atom("a")) Program.load(listOf(fact)) - assertTrue(Program.query(Atom("a"))) + val result = Program.query(Atom("a")) + + assertTrue(result) } @Test @@ -75,14 +77,14 @@ class EvaluationTest { val mother = Fact(Structure(Atom("mother"), listOf(Atom("jane"), Atom("jimmy")))) val parent1 = Rule( - Structure(Atom("parent"), listOf(Atom("X"), Atom("Y"))), + Structure(Atom("parent"), listOf(Variable("X"), Variable("Y"))), /* :- */ - Structure(Atom("father"), listOf(Atom("X"), Atom("Y"))) + Structure(Atom("father"), listOf(Variable("X"), Variable("Y"))) ) val parent2 = Rule( - Structure(Atom("parent"), listOf(Atom("X"), Atom("Y"))), + Structure(Atom("parent"), listOf(Variable("X"), Variable("Y"))), /* :- */ - Structure(Atom("mother"), listOf(Atom("X"), Atom("Y"))) + Structure(Atom("mother"), listOf(Variable("X"), Variable("Y"))) ) Program.load(listOf(father, mother, parent1, parent2)) @@ -100,11 +102,11 @@ class EvaluationTest { val mother = Fact(Structure(Atom("mother"), listOf(Atom("jane"), Atom("jimmy")))) val parent = Rule( - Structure(Atom("parent"), listOf(Atom("X"), Atom("Y"))), + Structure(Atom("parent"), listOf(Variable("X"), Variable("Y"))), /* :- */ Disjunction( - Structure(Atom("father"), listOf(Atom("X"), Atom("Y"))), + Structure(Atom("father"), listOf(Variable("X"), Variable("Y"))), /* ; */ - Structure(Atom("mother"), listOf(Atom("X"), Atom("Y"))) + Structure(Atom("mother"), listOf(Variable("X"), Variable("Y"))) )) Program.load(listOf(father, mother, parent)) @@ -129,17 +131,17 @@ class EvaluationTest { val parent2 = Fact(Structure(Atom("parent"), listOf(Atom("jane"), Atom("jimmy")))) val isFather = Rule( - Structure(Atom("isFather"), listOf(Atom("X"), Atom("Y"))), + Structure(Atom("isFather"), listOf(Variable("X"), Variable("Y"))), Conjunction( - Structure(Atom("parent"), listOf(Atom("X"), Atom("Y"))), - Structure(Atom("male"), listOf(Atom("X"))) + Structure(Atom("parent"), listOf(Variable("X"), Variable("Y"))), + Structure(Atom("male"), listOf(Variable("X"))) ) ) val isMother = Rule( - Structure(Atom("isMother"), listOf(Atom("X"), Atom("Y"))), + Structure(Atom("isMother"), listOf(Variable("X"), Variable("Y"))), Conjunction( - Structure(Atom("parent"), listOf(Atom("X"), Atom("Y"))), - Structure(Atom("female"), listOf(Atom("X"))) + Structure(Atom("parent"), listOf(Variable("X"), Variable("Y"))), + Structure(Atom("female"), listOf(Variable("X"))) ) )