Skip to content

Commit

Permalink
Merge branch 'develop' into feature/solve-streams-timeouts-alignment
Browse files Browse the repository at this point in the history
  • Loading branch information
gciatto committed Jun 12, 2020
2 parents 6249b0c + cdc872a commit 3a14c93
Show file tree
Hide file tree
Showing 103 changed files with 839 additions and 384 deletions.
Original file line number Diff line number Diff line change
@@ -1 +1,86 @@
TODO: write
Unification is the process of matching two terms by finding a suitable substitution to their variables, also known as the _most general unifier_ (MGU hereafter).

In 2P-Kt, unification utilities are encapsulated in the `Unificator` interface, which is partially implemented by the `AbstractUnificator` class.

Unification is provided by three functions:
- `mgu(Term, Term): Substitution` tries to unify two Terms, returning the MGU if it succeds, or the Fail object otherwise;
- `match(Term, Term): Boolean` tells whether two Terms match each other, that is there's a MGU for them;
- `unify(Term, Term): Term?` tries to unify two Terms, possibly returning the unified Term in case of success.

## Creating Unificators

Unificator's companion object provides three default implementations of the Unificator interface:

- `default` uses plain `equals` to determine Terms identity (like `strict`) and exploits a LRU cache with a fixed default capacity;
- `naive()` compares numbers by their value;
- `strict()` uses plain `equals` to determine Terms identity.

The `strict` and `naive` versions can also be called by giving them a starting unification _context_ to start with, which is simply a `Substitution` object containing pre-determined variable bindings that the user wishes to employ when unifying. Such behaviour can be obtained as follows:

```kotlin
val context: Substitution = ...
val strict = Unificator.strict()
val strictWithContext = Unificator.strict(context)
```

### Caching Unificators through decoration

Optionally, unificators can also be enabled to cache their results between several operations. This is easily accomplished by _decorating_ them through the companion object's `cached` method, which wraps them in a CachedUnificator instance, allowing them to store a limited amount of requests (default is 32) and repeating their response when necessary.

```kotlin
val unificator = Unificator.default

val cached = Unificator.cached(unificator) // default cache size
val smaller = Unificator.cached(unificator, capacity = 5) // stores up to 5 requests
```

By default, requests are cached following a LRU strategy (least recently used).

## Enabling/disabling occurs-check

The unification algorithm performs occurs-check by default. However, this check can be disabled by specifying the `occurCheckEnabled: Boolean` parameter when calling the aforementioned methods. For example:

```kotlin
val unificator = Unificator.default
val subtitution = unificator.mgu(term1, term2, occurCheckEnabled = false)
```

Note that this mechanism does not work when using the infix, operator-like variants of the unification functions.

## Infix variants

Unificator's companion object provides a handy alternative for calling unification functions in the form of **infix** methods.

These variants -- namely `mguWith`, `matches`, `unifyWith` -- allow developers to employ unification features in a more light and intuitive way, by exploting the syntactic tools provided by the Kotlin language.

This allows us to compute the MGU between two Terms simply by writing:

```kotlin
import it.unibo.tuprolog.unify.Unificator
...
val substitution = term1 mguWith term2
```

Keep in mind that these default variants **always perform occurs-check**, since they employ the implementations provided by `Unificator.default`.

## Implementing different unification strategies

Implementing custom Unificators comes down to defining the `checkTermsEquality` method from the `AbstractUnificator` class. This method is used by the unification algorithm to test whether two terms are matching.

Say we want to define a Unificator that compares numeric values by their absolute value. Then, we can write a new instance of `AbstractUnificator` that compares numbers like so:

```kotlin
val unificator = object : AbstractUnificator() {
override fun checkTermsEquality(first: Term, second: Term): Boolean = when {
first is Integer && second is Integer ->
first.value.absoluteValue.compareTo(second.value.absoluteValue) == 0
first is Numeric && second is Numeric ->
first.decimalValue.absoluteValue.compareTo(second.decimalValue.absoluteValue) == 0
else -> first == second
}
}
```

Notice how the default case still relies on checking term equality through the `==` operator, which aliases the `Term.equals` method.

This example shows how you can create custom unificator instances on-the-fly, but the same approach can be adopted if you want to extend the hierarchy by proper sub-classing.
Original file line number Diff line number Diff line change
Expand Up @@ -107,4 +107,72 @@ In particular, thanks to the instance of `Scope` created behind the scenes, vari
meaning that, if more variables exists within the to-be-copied `Term`, which have the same name,
then all fresh copies of such variables will have the same complete name.
Thus, for instance, a fresh copy of the `f(X, g(X))` would be something like `f(X_1, g(X_1))`
instead of `f(X_1, g(X_2))`.
instead of `f(X_1, g(X_2))`.

## Substitutions

Substitutions represent variable bindings, and are obtained through unification operations (see [Unification](substitutions-and-unification)). Indeed, Substitution is actually a subclass of Map<Var, Term>, and its methods are implemented by delegating to a Map instance.

Substitution has two types: Unifier and Fail. The former is a type representing a substitution as described in the Prolog standard, while the latter is a singleton instance used where a unifier cannot be found.

### Substitution creation

Substitution instances can be created using the `Substitution.of` factory method. Although these instances are usually obtained as a result of unification operations, it still may be useful to be aware of this simple implementation detail.

For example, Substitution instances can be created by specifying a series of variable-term pairs:

```kotlin
Scope.empty {
val substitution = Substitution.of(
varOf("X") to atomOf("abraham"),
varOf("Y") to atomOf("isaac"),
)
}
```

Keep in mind that `Substitution.of` will check for contradictions, and may possibly return Fail objects.

### Substitution application

Substitutions can be applied to terms through the `applyTo(term: Term)` method. Calling this method will return a new Term equivalent to the starting one, but all variables will be replaced according to the provided bindings.

For example, by applying the substitution `{X = abraham}` on term `father(X, isaac)`:

```kotlin
Scope.empty {
val term = structOf("father", varOf("X"), atomOf("isaac"))
val substitution = Substitution.of(varOf("X") to atomOf("abraham"))

val result = substitution.applyTo(term)
}
```

we will get the `father(abraham, isaac)` ground term as a result.

### Substitution composition

Substitutions can be composed through the `plus()` method, which is also available as the infix operator `+`.

For example, say we want to compose a substitution `{X = abraham}` with `{Y = isaac}` within the same scope. In order to do so, we would write:

```kotlin
Scope.empty {
val sub1 = Substitution.of(varOf("X"), atomOf("abraham"))
val sub2 = Substitution.of(varOf("Y"), atomOf("isaac"))

val substitution = sub1 + sub2
}
```

In 2P-Kt, unlike in the Prolog standard, composing two contradicting substitution will lead to a failure, yielding the Fail singleton object. For example, if we tried to bind a variable `X` with two different atoms:

```kotlin
Scope.empty {
val sub1 = Substitution.of(varOf("X"), atomOf("abraham"))
val sub2 = Substitution.of(varOf("X"), atomOf("nahor"))

val substitution = sub1 + sub2 // contradiction!
}
```

we would cause a contradiction, and the composition would fail.
1 change: 1 addition & 0 deletions gradle.properties
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
org.gradle.console=plain
kotlin.code.style=official

javaVersion=8
Expand Down
1 change: 0 additions & 1 deletion repl/gradle.properties

This file was deleted.

Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@ package it.unibo.tuprolog.ui.repl

import com.github.ajalt.clikt.core.ProgramResult
import com.github.ajalt.clikt.output.TermUi
import com.github.ajalt.clikt.output.defaultCliktConsole
import it.unibo.tuprolog.core.TermFormatter
import it.unibo.tuprolog.core.format
import it.unibo.tuprolog.core.parsing.ParseException
Expand Down Expand Up @@ -102,7 +103,7 @@ object TuPrologUtils {
var first = true
while (solutions.hasNext()) {
if (!first) {
val cmd = TermUi.prompt("", promptSuffix = "")?.trim()
val cmd = defaultCliktConsole().promptForLine("", false)?.trim()
if (cmd != ";") break
} else {
first = false
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -5,15 +5,19 @@ import it.unibo.tuprolog.solve.Solution

internal data class StateBacktracking(override val context: ClassicExecutionContext) : AbstractState(context) {
override fun computeNext(): State {
return with(context) {
if (choicePoints === null || !choicePoints.hasOpenAlternatives) {
StateEnd(
solution = Solution.No(query),
context = copy(step = nextStep())
)
val choicePoints = context.choicePoints
return if (choicePoints.let { it === null || !it.hasOpenAlternatives }) {
StateEnd(
solution = Solution.No(context.query),
context = context.copy(step = nextStep())
)
} else {
val choicePointContext = choicePoints!!.pathToRoot.first { it.alternatives.hasNext }
val nextContext = choicePointContext.backtrack(nextStep(), context.startTime)
if (nextContext.primitives.hasNext) {
StatePrimitiveExecution(nextContext)
} else {
val choicePointContext = choicePoints.pathToRoot.first { it.alternatives.hasNext }
StateRuleExecution(choicePointContext.backtrack(nextStep(), context.startTime))
StateRuleExecution(nextContext)
}
}
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -7,16 +7,9 @@ import it.unibo.tuprolog.solve.Solve
import it.unibo.tuprolog.solve.exception.PrologError
import it.unibo.tuprolog.solve.exception.TuPrologRuntimeException
import it.unibo.tuprolog.solve.exception.error.MessageError
import it.unibo.tuprolog.solve.primitive.UnaryPredicate

object Throw : UnaryPredicate<ExecutionContext>("throw") {
override fun uncheckedImplementation(request: Solve.Request<ExecutionContext>): Sequence<Solve.Response> =
sequenceOf(
request.ensuringAllArgumentsAreInstantiated()
.replyException(
handleError(request.context, request.arguments[0])
)
)

private fun handleError(context: ExecutionContext, error: Term): TuPrologRuntimeException =
when {
error is Struct && error.functor == "error" && error.arity in 1..2 -> {
Expand All @@ -28,4 +21,13 @@ object Throw : UnaryPredicate<ExecutionContext>("throw") {
}
else -> MessageError.of(error, context)
}

override fun Solve.Request<ExecutionContext>.computeAll(first: Term): Sequence<Solve.Response> {
return sequenceOf(
ensuringAllArgumentsAreInstantiated()
.replyException(
handleError(context, arguments[0])
)
)
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -278,4 +278,19 @@ class ClassicSolverSystemTesting : SolverFactory, SolverTest {
override fun testBasicBacktracking4() {
prototype.testBasicBacktracking4()
}

@Test
override fun testAssertRules() {
prototype.testAssertRules()
}

@Test
override fun testRetract() {
prototype.testRetract()
}

@Test
override fun testNatural() {
prototype.testNatural()
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -281,4 +281,19 @@ class StreamsSolverSystemTesting : SolverFactory, SolverTest {
override fun testBasicBacktracking4() {
prototype.testBasicBacktracking4()
}

@Test
override fun testAssertRules() {
prototype.testAssertRules()
}

@Test
override fun testRetract() {
prototype.testRetract()
}

@Test
override fun testNatural() {
prototype.testNatural()
}
}
29 changes: 29 additions & 0 deletions solve/src/commonMain/kotlin/it/unibo/tuprolog/solve/Solve.kt
Original file line number Diff line number Diff line change
Expand Up @@ -48,6 +48,35 @@ sealed class Solve {

/** Creates a new [Response] to this Request */
@JsName("replyWith")
fun replyWith(
substitution: Substitution,
libraries: Libraries? = null,
flags: PrologFlags? = null,
staticKb: Theory? = null,
dynamicKb: Theory? = null,
sideEffectManager: SideEffectManager? = null,
inputChannels: PrologInputChannels<*>? = null,
outputChannels: PrologOutputChannels<*>? = null
) = when (substitution) {
is Substitution.Unifier -> {
replySuccess(
substitution,
libraries,
flags,
staticKb,
dynamicKb,
sideEffectManager,
inputChannels,
outputChannels
)
}
else -> {
replyFail(libraries, flags, staticKb, dynamicKb, sideEffectManager, inputChannels, outputChannels)
}
}

/** Creates a new [Response] to this Request */
@JsName("replyWithSolution")
fun replyWith(
solution: Solution,
libraries: Libraries? = null,
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,7 @@ class InstantiationError(

fun forArgument(context: ExecutionContext, procedure: Signature, index: Int? = null, variable: Var? = null) =
InstantiationError(
message = "Argument ${index ?: ""} `${variable ?: ""}` of $procedure is unexpectedly not instantiated",
message = "Argument ${index ?: ""} `${variable ?: ""}` of ${procedure.toIndicator()} is unexpectedly not instantiated",
context = context,
extraData = variable
)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,7 @@ class TypeError(
index: Int? = null
) : this(
message = "Argument ${index
?: ""} of `$procedure` should be a `$expectedType`, but `$actualValue` has been provided instead",
?: ""} of `${procedure.toIndicator()}` should be a `$expectedType`, but `$actualValue` has been provided instead",
context = context,
expectedType = expectedType,
actualValue = actualValue,
Expand All @@ -64,13 +64,13 @@ class TypeError(
actualValue: Term,
index: Int? = null
) = TypeError(
message = "Argument ${index
?: ""} of `$procedure` should be a `$expectedType`, but `$actualValue` has been provided instead",
context = context,
expectedType = expectedType,
actualValue = actualValue,
extraData = actualValue
)
message = "Argument ${index
?: ""} of `${procedure.toIndicator()}` should be a `$expectedType`, but `$actualValue` has been provided instead",
context = context,
expectedType = expectedType,
actualValue = actualValue,
extraData = actualValue
)

fun forGoal(
context: ExecutionContext,
Expand Down
Original file line number Diff line number Diff line change
@@ -1,10 +1,9 @@
package it.unibo.tuprolog.solve.stdlib.function
package it.unibo.tuprolog.solve.function

import it.unibo.tuprolog.core.Integer
import it.unibo.tuprolog.core.Numeric
import it.unibo.tuprolog.core.Real
import it.unibo.tuprolog.solve.ExecutionContext
import it.unibo.tuprolog.solve.function.Compute

/**
* Base class to implement unary math functions
Expand Down
Loading

0 comments on commit 3a14c93

Please sign in to comment.