diff --git a/klogic-core/src/main/kotlin/org/klogic/core/Constraint.kt b/klogic-core/src/main/kotlin/org/klogic/core/Constraint.kt index 0f93e3f..dc97399 100644 --- a/klogic-core/src/main/kotlin/org/klogic/core/Constraint.kt +++ b/klogic-core/src/main/kotlin/org/klogic/core/Constraint.kt @@ -39,7 +39,7 @@ interface Constraint> { * The standard operation that applies this constraint is [Term.ineq]. */ data class InequalityConstraint internal constructor( - private val simplifiedConstraints: List> + internal val simplifiedConstraints: List> ) : Constraint { override fun verify(substitution: Substitution): ConstraintVerificationResult { if (simplifiedConstraints.isEmpty()) { @@ -55,7 +55,7 @@ data class InequalityConstraint internal constructor( } // Simplify this inequality constraint according to difference in substitutions - val simplifiedConstraints = delta.entries.map { + val simplifiedConstraints = delta.map { SingleInequalityConstraint(it.key, it.value.cast()) } val singleConstraint = InequalityConstraint(simplifiedConstraints) @@ -73,33 +73,23 @@ data class InequalityConstraint internal constructor( val firstSingleConstraint = remainingSimplifiedConstraints.first() - return unify(firstSingleConstraint.variable, firstSingleConstraint.term.cast()) + return unify(firstSingleConstraint.unboundedValue, firstSingleConstraint.term.cast()) ?.verify(remainingSimplifiedConstraints.subList(1, remainingSimplifiedConstraints.size)) } override fun toString(): String = simplifiedConstraints.joinToString(separator = ", ", prefix = "[", postfix = "]") companion object { - fun > of(variable: Var, term: Term): InequalityConstraint = - InequalityConstraint(listOf(SingleInequalityConstraint(variable, term))) - - // This method does not check that variable type equals to type of corresponding term, - // as it has to be in SingleInequalityConstraint, so it should be used very carefully - private fun unsafeOf(vararg pairs: Pair>, Term<*>>): InequalityConstraint { - val singleInequalityConstraints = pairs.map { - SingleInequalityConstraint(it.first, it.second.cast()) - } - - return InequalityConstraint(singleInequalityConstraints) - } + fun > of(unboundedValue: UnboundedValue, term: Term): InequalityConstraint = + InequalityConstraint(listOf(SingleInequalityConstraint(unboundedValue, term))) } /** - * Represents a simple inequality constraint - [variable] cannot be equal to [term] of the same type. + * Represents a simple inequality constraint - [unboundedValue] cannot be equal to [term] of the same type. */ - data class SingleInequalityConstraint>(val variable: Var, val term: Term) { - override fun toString(): String = "$variable !== $term" + data class SingleInequalityConstraint>(val unboundedValue: UnboundedValue, val term: Term) { + override fun toString(): String = "$unboundedValue !== $term" } } diff --git a/klogic-core/src/main/kotlin/org/klogic/core/Context.kt b/klogic-core/src/main/kotlin/org/klogic/core/Context.kt index d5c07db..8f7797f 100644 --- a/klogic-core/src/main/kotlin/org/klogic/core/Context.kt +++ b/klogic-core/src/main/kotlin/org/klogic/core/Context.kt @@ -21,7 +21,7 @@ open class RelationalContext : AutoCloseable { val nilStream: RecursiveStream = NilStream() /** - * The index of the last variable created in this context. + * The index of the last [Var] created in this context. */ private var lastCreatedVariableIndex: Int = 0 @@ -59,6 +59,12 @@ open class RelationalContext : AutoCloseable { */ fun > freshTypedVar(): Var = (lastCreatedVariableIndex++).createTypedVar() + /** + * Returns a new [Wildcard] according to the specified type. + */ + @Suppress("UNCHECKED_CAST") + fun > wildcard(): Term = Wildcard as T + /** * Returns a result of invoking [run] overloading with goals for the fresh variable created using the passed [state]. * NOTE: [goals] must not be empty. diff --git a/klogic-core/src/main/kotlin/org/klogic/core/State.kt b/klogic-core/src/main/kotlin/org/klogic/core/State.kt index 532ded3..e774a8d 100644 --- a/klogic-core/src/main/kotlin/org/klogic/core/State.kt +++ b/klogic-core/src/main/kotlin/org/klogic/core/State.kt @@ -16,7 +16,7 @@ data class State( val constraints: PersistentSet> = persistentHashSetOf(), ) { constructor( - map: Map, Term<*>>, + map: Map, Term<*>>, constraints: PersistentSet>, ) : this(Substitution(map), constraints) diff --git a/klogic-core/src/main/kotlin/org/klogic/core/Substitution.kt b/klogic-core/src/main/kotlin/org/klogic/core/Substitution.kt index 458e6f6..bd79596 100644 --- a/klogic-core/src/main/kotlin/org/klogic/core/Substitution.kt +++ b/klogic-core/src/main/kotlin/org/klogic/core/Substitution.kt @@ -10,8 +10,8 @@ import org.klogic.unify.toUnificationState * Represents an immutable association of [Var]s with arbitrary types and bounded [Term]s with corresponding types. */ @JvmInline -value class Substitution(private val innerSubstitution: PersistentMap, Term<*>> = persistentHashMapOf()) { - constructor(map: Map, Term<*>>) : this(map.toPersistentHashMap()) +value class Substitution(private val innerSubstitution: PersistentMap, Term<*>> = persistentHashMapOf()) { + constructor(map: Map, Term<*>>) : this(map.toPersistentHashMap()) /** * Checks whether [InequalityConstraint] for [left] and [right] of the same type can be satisfied. @@ -27,7 +27,8 @@ value class Substitution(private val innerSubstitution: PersistentMap, Te */ fun > ineq(left: Term, right: Term): ConstraintVerificationResult { return toUnificationState().unify(left, right)?.let { unificationState -> - val delta = unificationState.substitutionDifference + // Filter out wildcards as they add no information + val delta = unificationState.substitutionDifference.filterNot { it.key is Wildcard || it.value is Wildcard } // If the substitution from unification does not differ from the current substitution, // it means that this constraint is violated. if (delta.isEmpty()) { @@ -35,8 +36,8 @@ value class Substitution(private val innerSubstitution: PersistentMap, Te } // Otherwise, this constraint can be satisfied, and we can simplify it according to calculated substitution delta. - val simplifiedConstraints = delta.entries.map { - InequalityConstraint.SingleInequalityConstraint(it.key, it.value.cast()) + val simplifiedConstraints = delta.map { + InequalityConstraint.SingleInequalityConstraint(it.key as Var<*>, it.value.cast()) } val singleConstraint = InequalityConstraint(simplifiedConstraints) @@ -55,7 +56,7 @@ value class Substitution(private val innerSubstitution: PersistentMap, Te fun isEmpty(): Boolean = innerSubstitution.isEmpty() - operator fun plus(pair: Pair, Term<*>>): Substitution = + operator fun plus(pair: Pair, Term<*>>): Substitution = (innerSubstitution.put(pair.first, pair.second)).toSubstitution() operator fun minus(other: Substitution): Substitution = @@ -74,4 +75,4 @@ value class Substitution(private val innerSubstitution: PersistentMap, Te } } -fun Map, Term<*>>.toSubstitution(): Substitution = Substitution(this) +fun Map, Term<*>>.toSubstitution(): Substitution = Substitution(this) diff --git a/klogic-core/src/main/kotlin/org/klogic/core/Term.kt b/klogic-core/src/main/kotlin/org/klogic/core/Term.kt index 796ada4..decbe98 100644 --- a/klogic-core/src/main/kotlin/org/klogic/core/Term.kt +++ b/klogic-core/src/main/kotlin/org/klogic/core/Term.kt @@ -120,11 +120,17 @@ sealed interface Term> { } } +/** + * Represents a logic term of the specific type + * that does not have a particular value before unifications - either [Var] or [Wildcard]. + */ +sealed interface UnboundedValue> : Term + /** * Represents a symbolic term with the specified term that can be equal to any other [Term] of the same type. */ @JvmInline -value class Var>(val index: Int) : Term { +value class Var> internal constructor(val index: Int) : UnboundedValue { override fun > occurs(variable: Var): Boolean = this == variable override fun walk(substitution: Substitution): Term = substitution[this]?.let { @@ -136,11 +142,11 @@ value class Var>(val index: Int) : Term { return unificationState } - if (walkedOther !is Var && walkedOther.occurs(this)) { + if (walkedOther is CustomTerm && walkedOther.occurs(this)) { return null } - val newAssociation = this to walkedOther + val newAssociation = if (walkedOther is Wildcard) walkedOther to this else this to walkedOther unificationState.substitutionDifference[newAssociation.first] = newAssociation.second return unificationState.copy(substitution = unificationState.substitution + newAssociation) @@ -154,10 +160,39 @@ value class Var>(val index: Int) : Term { override fun toString(): String = "_.$index" companion object { + /** + * Manually creates a variable with [this] index. + * WARNING: use it very carefully as this method does not care about [RelationalContext.lastCreatedVariableIndex]. + */ fun > Int.createTypedVar(): Var = Var(this) } } +/** + * Represents all logic values of the specific type (in consideration of [InequalityConstraint]s). + * For more information [take a look at the paper](https://danyaberezun.github.io/publications/assets/mk-2022-wild.pdf). + */ +object Wildcard : UnboundedValue { + override fun > occurs(variable: Var): Boolean = false + + override fun walk(substitution: Substitution): Wildcard = this + + override fun unifyImpl(walkedOther: Term, unificationState: UnificationState): UnificationState? { + if (walkedOther is Wildcard) { + return unificationState + } + + return walkedOther.unifyImpl(this, unificationState) + } + + @Suppress("UNCHECKED_CAST") + override fun > cast(): Term = this as Term + + override fun asReified(): Nothing = error("Wildcard $this cannot be reified") + + override fun toString(): String = "__" +} + /** * Represents a custom (i.e., defined by user) term. */ @@ -188,6 +223,10 @@ interface CustomTerm> : Term { } override fun unifyImpl(walkedOther: Term, unificationState: UnificationState): UnificationState? { + if (walkedOther is Wildcard) { + return unificationState + } + if (walkedOther !is CustomTerm) { // This branch means that walkedOther is Var return walkedOther.unifyImpl(this, unificationState) diff --git a/klogic-core/src/main/kotlin/org/klogic/unify/Unify.kt b/klogic-core/src/main/kotlin/org/klogic/unify/Unify.kt index 0139260..fe47932 100644 --- a/klogic-core/src/main/kotlin/org/klogic/unify/Unify.kt +++ b/klogic-core/src/main/kotlin/org/klogic/unify/Unify.kt @@ -1,9 +1,6 @@ package org.klogic.unify -import org.klogic.core.State -import org.klogic.core.Substitution -import org.klogic.core.Term -import org.klogic.core.Var +import org.klogic.core.* /** * Represents a mutable state of unification process. @@ -13,7 +10,7 @@ import org.klogic.core.Var */ data class UnificationState( val substitution: Substitution = Substitution.empty, - val substitutionDifference: MutableMap, Term<*>> = mutableMapOf() + val substitutionDifference: MutableMap, Term<*>> = mutableMapOf() ) { /** * Tries to unify two terms of the same type [left] and [right] using [substitution]. diff --git a/klogic-core/src/test/kotlin/org/klogic/core/unify/InequalityTest.kt b/klogic-core/src/test/kotlin/org/klogic/core/unify/InequalityTest.kt index 75d5d6b..b21d14c 100644 --- a/klogic-core/src/test/kotlin/org/klogic/core/unify/InequalityTest.kt +++ b/klogic-core/src/test/kotlin/org/klogic/core/unify/InequalityTest.kt @@ -58,10 +58,11 @@ class InequalityTest { val goal = x `!==` `1` val run = run(2, x, goal) + val answer = run.single() val expectedConstraints = setOf(InequalityConstraint.of(x, `1`)) - assertEquals(x, run.singleReifiedTerm) - assertEquals(expectedConstraints, run.singleReifiedTermConstraints) + assertEquals(x, answer.term) + assertEquals(expectedConstraints, answer.constraints) } } @@ -163,9 +164,10 @@ class InequalityTest { val goals = arrayOf(`3` `!==` `4`) val run = run(2, q, goals) + val answer = run.single() - assertTrue(run.singleReifiedTermConstraints.isEmpty()) - assertEquals(q, run.singleReifiedTerm) + assertTrue(answer.constraints.isEmpty()) + assertEquals(q, answer.term) } } diff --git a/klogic-core/src/test/kotlin/org/klogic/core/wildcards/WildcardsTest.kt b/klogic-core/src/test/kotlin/org/klogic/core/wildcards/WildcardsTest.kt new file mode 100644 index 0000000..6076304 --- /dev/null +++ b/klogic-core/src/test/kotlin/org/klogic/core/wildcards/WildcardsTest.kt @@ -0,0 +1,169 @@ +package org.klogic.core.wildcards + +import org.junit.jupiter.api.Assertions.assertEquals +import org.junit.jupiter.api.Assertions.assertTrue +import org.junit.jupiter.api.Test +import org.klogic.core.Goal +import org.klogic.core.InequalityConstraint +import org.klogic.core.Term +import org.klogic.core.Var +import org.klogic.core.and +import org.klogic.core.conde +import org.klogic.core.delay +import org.klogic.core.freshTypedVars +import org.klogic.utils.terms.Cons +import org.klogic.utils.terms.LogicList +import org.klogic.utils.terms.LogicList.Companion.logicListOf +import org.klogic.utils.terms.LogicPair +import org.klogic.utils.terms.Nil.emptyLogicList +import org.klogic.utils.terms.PeanoLogicNumber +import org.klogic.utils.terms.Symbol +import org.klogic.utils.terms.Symbol.Companion.toSymbol +import org.klogic.utils.terms.ZeroNaturalNumber.Z +import org.klogic.utils.terms.logicTo +import org.klogic.utils.terms.toPeanoLogicNumber +import org.klogic.utils.terms.unaryPlus +import org.klogic.utils.withEmptyContext + +class WildcardsTest { + @Test + fun `x !== __ -- failure`() { + withEmptyContext { + val goal = { x: Term -> x `!==` wildcard() } + + val run = run(10, goal) + assertTrue(run.isEmpty()) + } + } + + @Test + fun `x !== (__, 1) && x === (1, y)`() { + withEmptyContext { + val one = "1".toSymbol() + + fun goal(x: Term>, y: Term): Goal = + (x `!==` (wildcard() logicTo one)) and (x `===` (one logicTo y)) + + val y = freshTypedVar() + val x = freshTypedVar>() + + val run = run(10, x, goal(x, y)) + val answer = run.single() + + val answerTerm = answer.term.asReified() + assertEquals(one, answerTerm.first) + + // x == (1, y), y != 1 + val inequalityConstraint = answer.constraints.single() as InequalityConstraint + val answerConstraint = inequalityConstraint.simplifiedConstraints.single() + assertEquals(answerTerm.second, answerConstraint.unboundedValue) + assertEquals(one, answerConstraint.term) + } + } + + @Test + fun `(1, __) != (__, 1) --- failure`() { + withEmptyContext { + val one = "1".toSymbol() + + val goal = { _: Term<*> -> (one logicTo wildcard()) `!==` (wildcard() logicTo one) } + + val run = run(10, goal) + assertTrue(run.isEmpty()) + } + } + + @Test + fun `(x, 2, __) != (1, __, 2) --- x != 1`() { + withEmptyContext { + val one = "1".toSymbol() + val two = "2".toSymbol() + + val goal = { x: Term -> + logicListOf(x, two, wildcard()) `!==` logicListOf(one, wildcard(), two) + } + + val run = run(10, goal) + val answer = run.single() + + val variable = answer.term + assertTrue(variable is Var) + + val inequalityConstraint = answer.constraints.single() as InequalityConstraint + val answerConstraint = inequalityConstraint.simplifiedConstraints.single() + + assertEquals(variable, answerConstraint.unboundedValue) + assertEquals(one, answerConstraint.term) + } + } + + @Test + fun `(x, y) != (1, __) --- x != 1`() { + withEmptyContext { + val one = "1".toSymbol() + + val x = freshTypedVar() + val y = freshTypedVar() + val goal = { symbol: Term -> + logicListOf(symbol, y) `!==` logicListOf(one, wildcard()) + } + + val run = run(10, x, goal(x)) + val answer = run.single() + + val variable = answer.term + assertTrue(variable is Var) + + val inequalityConstraint = answer.constraints.single() as InequalityConstraint + val answerConstraint = inequalityConstraint.simplifiedConstraints.single() + + assertEquals(variable, answerConstraint.unboundedValue) + assertEquals(one, answerConstraint.term) + } + } + + @Test + fun `x lt 4`() { + withEmptyContext { + fun allPeanoNumbers(x: Term): Goal = conde( + x `===` Z, + freshTypedVars { prev -> + (x `===` +prev) and delay { allPeanoNumbers(prev) } + } + ) + + fun lessThan4(x: Term) = x `!==` +(+(+(+(wildcard())))) + + val goal = { x: Term -> lessThan4(x) and allPeanoNumbers(x) } + + val run = run(10, goal) + assertEquals(4, run.size) + assertEquals(Z, run[0].term) + assertEquals(1.toPeanoLogicNumber(), run[1].term) + assertEquals(2.toPeanoLogicNumber(), run[2].term) + assertEquals(3.toPeanoLogicNumber(), run[3].term) + } + } + + @Test + fun `x != Cons --- x == ()`() { + withEmptyContext { + val value = "42".toSymbol() + + fun allLists(x: Term>): Goal = conde( + x `===` emptyLogicList(), + freshTypedVars> { prev -> + (x `===` Cons(value, prev)) and delay { allLists(prev) } + } + ) + + fun isNotCons(x: Term>) = x `!==` Cons(wildcard(), wildcard()) + + val goal = { x: Term> -> isNotCons(x) and allLists(x) } + + val run = run(10, goal) + val answer = run.single() + assertEquals(emptyLogicList(), answer.term) + } + } +} diff --git a/klogic-utils/src/main/kotlin/org/klogic/utils/terms/PeanoLogicNumber.kt b/klogic-utils/src/main/kotlin/org/klogic/utils/terms/PeanoLogicNumber.kt index 1514da8..2f597bc 100644 --- a/klogic-utils/src/main/kotlin/org/klogic/utils/terms/PeanoLogicNumber.kt +++ b/klogic-utils/src/main/kotlin/org/klogic/utils/terms/PeanoLogicNumber.kt @@ -22,6 +22,7 @@ sealed class PeanoLogicNumber : CustomTerm { } private typealias PeanoTerm = Term +operator fun PeanoTerm.unaryPlus(): NextNaturalNumber = NextNaturalNumber(this) object ZeroNaturalNumber : PeanoLogicNumber() { val Z: ZeroNaturalNumber = ZeroNaturalNumber diff --git a/klogic-utils/src/test/kotlin/org/klogic/utils/terms/OlegLogicNumberTest.kt b/klogic-utils/src/test/kotlin/org/klogic/utils/terms/OlegLogicNumberTest.kt index a9aa179..e4a6791 100644 --- a/klogic-utils/src/test/kotlin/org/klogic/utils/terms/OlegLogicNumberTest.kt +++ b/klogic-utils/src/test/kotlin/org/klogic/utils/terms/OlegLogicNumberTest.kt @@ -26,7 +26,7 @@ class OlegLogicNumberTest { val firstTenPositiveNumbers = run(10, x, goal) - assertEquals(x, firstTenPositiveNumbers.singleReifiedTerm) + assertEquals(x, firstTenPositiveNumbers.single().term) } } @@ -56,7 +56,7 @@ class OlegLogicNumberTest { val firstTenPositiveNumbers = run(10, x, goal) - assertEquals(x, firstTenPositiveNumbers.singleReifiedTerm) + assertEquals(x, firstTenPositiveNumbers.single().term) } } @@ -129,7 +129,7 @@ class OlegLogicNumberTest { val run = run(10, result, mulᴼ(first, second, result)) val expectedResult = i * j - assertEquals(expectedResult, run.singleReifiedTerm.asReified().toUInt()) + assertEquals(expectedResult, run.singleReifiedTerm.toUInt()) } } } @@ -147,7 +147,7 @@ class OlegLogicNumberTest { val run = run(10, first, mulᴼ(first, second, result)) - assertEquals(i, run.singleReifiedTerm.asReified().toUInt()) + assertEquals(i, run.singleReifiedTerm.toUInt()) } } } @@ -205,7 +205,7 @@ class OlegLogicNumberTest { val run = run(10, second, mulᴼ(first, second, result)) - assertEquals(j, run.singleReifiedTerm.asReified().toUInt()) + assertEquals(j, run.singleReifiedTerm.toUInt()) } } } @@ -253,7 +253,7 @@ class OlegLogicNumberTest { val b = 2u.toOlegLogicNumber() val q = 3u.toOlegLogicNumber() - val r = run(10, { r: Term -> logᴼ(n, b, q, r) }).singleReifiedTerm.asReified().toUInt() + val r = run(10, { r: Term -> logᴼ(n, b, q, r) }).singleReifiedTerm.toUInt() assertEquals(6u, r) } } @@ -271,7 +271,7 @@ class OlegLogicNumberTest { val run = run(10, result, expᴼ(base, power, result)) val expectedResult = i.toDouble().pow(j.toInt()).toUInt() - assertEquals(expectedResult, run.singleReifiedTerm.asReified().toUInt()) + assertEquals(expectedResult, run.singleReifiedTerm.toUInt()) } } } @@ -289,7 +289,7 @@ class OlegLogicNumberTest { val run = run(10, base, expᴼ(base, power, result)) - assertEquals(i, run.singleReifiedTerm.asReified().toUInt()) + assertEquals(i, run.singleReifiedTerm.toUInt()) } } } @@ -307,7 +307,7 @@ class OlegLogicNumberTest { val run = run(10, power, expᴼ(base, power, result)) - assertEquals(j, run.singleReifiedTerm.asReified().toUInt()) + assertEquals(j, run.singleReifiedTerm.toUInt()) } } } diff --git a/klogic-utils/src/testFixtures/kotlin/org/klogic/utils/TestUtils.kt b/klogic-utils/src/testFixtures/kotlin/org/klogic/utils/TestUtils.kt index d55e766..8132e96 100644 --- a/klogic-utils/src/testFixtures/kotlin/org/klogic/utils/TestUtils.kt +++ b/klogic-utils/src/testFixtures/kotlin/org/klogic/utils/TestUtils.kt @@ -44,8 +44,8 @@ val listB: Var> = listSymbolVariables[5] val listC: Var> = listSymbolVariables[6] val listD: Var> = listSymbolVariables[7] -val > List>.singleReifiedTerm: Term - get() = single().term +val > List>.singleReifiedTerm: T + get() = single().term.asReified() val List>.singleReifiedTermConstraints: Set> get() = single().constraints