tuprolog / 2p-kt Goto Github PK

The actual implementation of the unification algorithm was made following the first definition in this paper.

But after Section 3 in this paper, more efficient versions of the algorithm are proposed; in some future, will be a good thing to implement the more efficient version proposed.

Actual implementation of Clauses sintactically allows any Term as its body, but the Standard Prolog states that:

A well-formed body cannot contain a number.

So it would be nice to add a property isWellFormed to Clause that will detect if it's well formed or not.

There are three jvm tests in TestReal class that are failing; their names are: creationAsNumbers2, comparisons, value.

This failure shold be investigated and solved.

Sadly, I modeled sets in a wrong way.

Currently, sets are modeled as follows:

• N-Sized Set -> '{}'(Arg1, ..., ArgN), i.e., a struct whose functor is {} and whose arguments are the set items
  • for all N = 0, 1, 2, ...
• the Empty Set is actually an Atom

But actually, their are modeled differently in Prolog:

• Empty set -> Atom '{}'
• 1-sized set with argument X -> Struct '{}'(X)
• N-sized set with arguments X1, ..., Xn -> Struct '{}'(X) where X = (X1, ..., Xn) is a conjunction

So, for instance, unifying { 1, 2, 3 } with { 1, X }, is solved by X = (2, 3)

I wanted to use the library programmatically from Java. Sadly I couldn't find any specific information regarding this in the readme.md or in the projects documentation (the respective page is empty).

So my questions are:

1. Where is the programmatic entry point for adding a knowledge base and then querying the Prolog engine against this knowledge base. I have the knowledge base and the respective queries as a string representation.
2. Which part of the library do I need for that (core, parser, theory, ...?)

I think that Signature is missing that in kotlin vararg parameters can be in all positions of a method signature, not only in last position like in java.

So if vararg support is for invoking even kotlin vararg methods, this class should be enhanched with a position of the vararg.

Using A scope with method listOf is misleading to Kotlin user that really wanted to create a kotlin List.

Methods such as listOf() and setOf() that clash with library method names should be changed to logicListOf() and logicSetOf().

Currently if you want to construct a tuple with tupleOf(Iterable<Term>) you can't write tupleOf(listOf(atomOf("a"), atomOf("b"))) inside Scope scope, because the outermost argument is considered as a logic list, so it is one Term an so Tuple constructor complains throwing exception... But the user didn't want to create a logical list.

Now method stricltyEquals checks if passed class is of one type or a subclass of it.

As it should be a strict check, we maybe should add a check to limit correct classes to the specific instance class.

From the Prolog Standard:

In a database all the clauses are well-formed (Section 2.2.3) and transformed, i.e. all variables X in the position of a predication in the body of the clauses have been replaced by call(X) and all the facts also have the form of a rule whose body is true. Thus all the clauses in a database have the form of a rule.

For example, the Clause product (A) : - A, A is stored in the database, after preparation for execution, as the term: product(A) :- call(A) , call(A)

Those transformation should be made during Clause addition and/or Database creation.

A check on Clause insertion should be added, to ensure that all contained clauses are well-formed

Anonymous variables during the unification process should be considered different even using the non-strict identity matcher.

They should always be considered different from each other unless they are the same instance.

Hashmaps are not currently used in it.unibo.tuprolog.theory.Rete but they should in order to reach better performances in accessing clauses

Recently added TermVisitor was not tested... tests for it should be added to ensure its correct functionality.

This issue lists Renovate updates and detected dependencies. Read the Dependency Dashboard docs to learn more.

Open

These updates have all been created already. Click a checkbox below to force a retry/rebase of any.

• ci(deps): update actions/checkout action to v4.1.6
• fix(deps): update kotlinx.coroutines to v1.8.1 (minor) (org.jetbrains.kotlinx:kotlinx-coroutines-test, org.jetbrains.kotlinx:kotlinx-coroutines-core)
• fix(deps): update dependency com.github.ajalt.clikt:clikt to v4
• Click on this checkbox to rebase all open PRs at once

Detected dependencies

• Check this box to trigger a request for Renovate to run again on this repository

This popup shows up when trying to save a file.

Steps to reproduce:

• create a new file
• click File > Save As
• save the file with .pl o .pro extension
• click File > Save

Versions:

• 2P-Kt v0.20.4-dev61+cbec54e9
• JVM v17.0.3
• JavaFX v19-ea+6
• Kubuntu 21.10

Should be added a test code coverage tool to detect, in an automatic fashion, which parts of code are still not adequately tested.

I think that all Terms manipulated inside a Scope should absorb current variable bindings.

Actual situation:

    val scope = Scope.of("X")

    val scopeExternalStructWithXVariable = Struct.of("f", Var.of("X"))

    println("Two different variables with same name should only be equals.")
    println(scope["X"] === scopeExternalStructWithXVariable[0]) // false, correct
    println(scope["X"] == scopeExternalStructWithXVariable[0]) // true, correct
    println(scope["X"]?.strictlyEquals(scopeExternalStructWithXVariable[0])) // false, correct

    val myFactCreatedTroughXScope = with(scope){
        factOf(scopeExternalStructWithXVariable)
    }

    val structWithXVariableThatWalkedTroughXScope = myFactCreatedTroughXScope.head

    println("\nExternal terms manipulated inside a scope, doesn't absorb variable bindings; is that misleading for final users?")
    println(scope["X"] === structWithXVariableThatWalkedTroughXScope[0]) // false, maybe *expected* true by an API user??
    println(scope["X"] == structWithXVariableThatWalkedTroughXScope[0]) // true, correct
    println(scope["X"]?.strictlyEquals(structWithXVariableThatWalkedTroughXScope[0])) // false, maybe *expected* true by an API user??

Expected:

In my opinion all three last println should print true!

A logging framework should be adopted to help debugging, of critical software parts. It should work in common code to be compiled in all destinaton platform languages.

Hello,

First of all, thanks for a great portable Prolog implementation.

I'm experimenting with reasoning in GDL. It's a subset of Prolog that is used to specify games for an AI to play.

The issue is that it requires the ability to assert some statements about a game using true/1 predicate, but it seems like even a simple example can't be handled by tuProlog.

If I create a file example.pdb with the following contents:

true(_).

I'm getting the output:

# 2P-Kt version 0.18.1
# Error while parsing theory file: example.pdb
#     Message: mismatched input '(' expecting {SIGN, ',', '|', FULL_STOP, OPERATOR}
#     Line   : 1
#     Column : 5
#     Clause : 0

# Successfully loaded library `prolog.io`
# Successfully loaded library `prolog.lang`

?- 

I'm using 2p-repl-0.18.1-redist.jar.

Can this issue be somehow solved?

In core subproject there are two exceptions TuprologException and TuprologRuntimeException that extend the same base class Exception.

Why they're not exteding one from each other? And why there are two exceptions?

In Kotlin all exceptions are unchecked an so in my opinion there's no need for a TuprologException (checked exceptions only raise management problems, when used in Java, with no true benefit)

The method freshCopy() for now doesn't take into account that if a Variable occurs multiple times in a Term, then the same copied instance should be placed multiple times in the copy, to avoid creating diverging variables.

It is of paramount importance that RETE indexes (i.e. it.unibo.tuprolog.theory.ReteTree) are finely tested in order to ensure each method work as intended.
Thus we should not merely test RETE indexes indirectly by testing ClauseDatabases.

Let me here remark the intended meaning of the ReteTree API:

• ReteTree.Companion.of should create a new tree out of the provided Clauses

  • The partial order among the provided clauses sharing the same functor & arity is of paramount importance
    • Such order affect the behaviour of ReteTree.get, ReteTree.clauses, ReteTree.remove

• ReteTree.clauses: Sequence<Clause> should return a sequence lazily iterating over all the clauses indexed by the current tree, there including directives.

  • An essential feature is that the partial ordering of clauses sharing the same functor & arity (w.r.t. insertion order) must be respected in the sequence.

• ReteTree.get(Clause): Sequence<Clause> should return a sequence lazily iterating over all the clauses indexed by the current tree which unify with Clause according to the default unifier.

  • An essential feature is that the partial ordering of clauses sharing the same functor & arity (w.r.t. insertion order) must be respected in the sequence.

• ReteTree.remove(Clause, Int): Sequence<Clause> should return a sequence lazily iterating over all the clauses indexed by the current tree which unify with Clause according to the default unifier. In case the second argument, namely limit, is negative, then all possible Clauses are returned within the sequence. Otherwise, if limit is non-negative the amount of Clauses actually returned by this method must be lower or equals to limit. In any case, all Clauses returned within the output sequence are removed from the current ReteTree and its internal nodes.

  • An essential feature is that the partial ordering of clauses sharing the same functor & arity (w.r.t. insertion order) must be respected.

• ReteTree.clone(): ReteTree<*> produces a brand new deep copy of the current index---except for the indexed Clauses, for which only references are cloned. Each edit to returned index does not affect the original index.

Common code of each sub-project, should run tests on each target platform.

Running tests on JavaScript platform is not out-of-the-box like JVM testing.

A custom way to run tests over a JavaScript test framework should be found and integrated into the project.

More tests should be added for already present classes, to stress single methods and cover as much as possible all relevant lines of code.

I am looking for an example of how to

• Load a Prolog script,
• Add few more facts to the load program programmatically
• Find a solution to a resulting predicate

In details, let say I have a script main.pl:

increment(A, B) :-
    diff(C),
    B is A + C.   

Then I'd like to enhance it on Java side

Struct.of("diff", Integer.of(15));

and then run

Struct.of("increment", Atom.of(15), Integer.of("X"));

... something that the returns the value of X as an int

I think that more meaningful names should be given to methods that work with Substitutions

For example:

1. In Substitution interface the method ground(term: Term) could be named substituteIn(term: Term) or applyIn(term: Term)
2. In Term interface the methods groundTo(substitution: Substitution) could be named simply apply(substitution: Substitution)

Code before:

val substitutedTerm = myStruct.groundTo(mySubstitution)
val substitutedTerm = mySubstitution.ground(myStruct)

Code after:

val substitutedTerm = myStruct.apply(mySubstitution)
val substitutedTerm = mySubstitution.applyIn(myStruct) // mySubstitution.substituteIn(myStruct)

Var default equals should check complete name to help management of variables in Sets and Maps.

Should solve #180.

I've found a BUG in the implementation of AbstractUnificationStrategy, in particular the implementation of applySubstitutionToEquations(...)

The bug prevents simple unification like (f(a,b(X)) :- b) = (f(A,B) :- C) from being "solved", making the Unification strategy go into infinite loop.

The problem is due the use of === (aka referential equality) that is used to check if changes are made during Substitution application; in fact applying a Substitution always results in creation of new Struct for example (because of the support to immutability); so even if actually no change is made, the function returns true signaling changes and making the algorithm continue indefinitely.

The solution could be simply the change of referential equality with simple equality check, in that function.

Furthermore, a new test for this unification should be added to prevent future regression.

All of the build.gradle.kts files now share an identical part that should be moved in a common place, to make changes consistent within all subprojects.

For example there is already an inconsistency between the multiplatform plugin version in core subproject (1.3.31) and other subprojects (1.3.21); to avoid this, the common part could be placed in project root gradle file.

For some reason Gitlab CI is still using Gradle 5.4 version despite its updated to Gradle 5.5.1 in project gradle-wrapper.properties

In the 2p-kt IDE, the content of the solution box (and most likely of other similar boxes) cannot be copied for later pasting elsewhere. This is a pity, copying solutions (but also output, etc.) is often needed for documentation, debug, reports, etc.
Should be fixed in one of the following ways:

• preferred approach: simply enable text selection and copying, in a standard way; OR
• support mouse right-click with contextual menu providing a "copy" item; OR
• just add a "copy" button (less general, somehow weird, but perhaps quicker to impement..?)

Now VarImpl uses Int as type for it's internal identifier field.

In intensive usage cases, the Int value can overflow... BigInteger would solve those problems once for all.

According to section 2.1.2 (page 6) of the Prolog standard, terms are totally ordered in a non-trivial way:

In Standard Prolog the terms are totally ordered according to the following rules which define the binary relation term_precedes.

More precisely:

• All variables precede all floating-point numbers, which precede all integers, which precede all atoms, which precede all compound terms.
• All variables are totally ordered but the order is implementation dependent and may vary during computations.
• All numbers (of the same type) are ordered according to the usual arithmetic.
• All atoms are ordered according to the characters forming their name and the character codes of the characters (an integer associated with each character). The null atom precedes all non-null atoms (hence z precedes z_a). An atom a1 precedes an atom a2 if the character code of the first character of a1 is less than the character code of the first character of a2. If these
  values are equal, the tail character sequences are compared. Notice that the order induced by the character codes is implementation
  defined, except that the alphabetical order must be respected and the digits must be sequential. More details are provided in Section 9.1.3.
• Compound terms are ordered according to their arity; if they have same arity, by the name of their functor. If they have same arity and same functor name, they are ordered by considering successively the order of their arguments starting from the first.
  • Example: g(X) precedes f(X, V), f(Z,b) precedes f(a,A), according to the ASCII table given in Annex 11.3, but is after f(Z, a). f(Z, Z) precedes f(X, X, X) but its comparison with f(X, X) depends on the processor (implementation dependent).

There is yet another notable sort of structures that may deserve their own interface in core: indicators.
A well formed indicator is a struct in the form '/'(F, N) where F is an atom and N is a non negative integer.
Of course, variables may be accepted too in some cases.

Substitution should be an interface, with maybe two implementations (to be studied how can be done):

• an implementation SuccessSubstitution backed by a Map<Var, Term> with actual substitutions
• a singleton implementation FailedSubstitution that will be "empty"

There are two types of lists:

• those terminated with an empty list terminator, also writeable as [E1, E2, E3]
• those terminated with pipe operator [H1, H2 | T]

For creating lists now we have two factory methods in List companion object:

• List.of: creates always an empty terminated list with given arguments (e.g the first type described above)
• List.from: that can create both list types passing, or not, a terminal Term to the method

The second method should always create a "piped list" with last item, and leave the creation of empty terminated lists to List.of only, to better separate their responsibilities (Single Responsibility Principle)

Scope.varOf("_") should be treated as Scope.anonymous() in my opinion.

Am I right?

KotlinTest is a powerful testing suite that could be adopted to make project tests more readable and expressive.

Among other feature it supports Property Based testing and Data Driven testing, two important features to be more declarative in testing.

Adopting this suite will mean migrating to JUnit 5 and therefore also rewriting part of the existing test structure to adapt to it.

In code there's no documtation, it would be better to document at least non-trivial/domain-specific "things" (methods, properties and classes) to shortly explain what they stand for.

https://www.quora.com/What-is-the-difference-between-the-integer-and-integral

We need another name, e.g. Int or Integer.
Avoiding clashes with standard libraries is also desired, but not strictly required

Some changes were made to core without testing them, and therefore:

• Test the addition of method Substition.of(Iterable<Pair<Var, Term>>)
• Test the addition of Constant interface
• Test the addition of Term.isConstant property

Tests should be aligned.

A Constant interface should be added, as shown in this UML, to be a superinterface of Atom and Numeric interfaces.

I've found a problem that makes actual mgu implementation to go into infinite loop.

Steps to reproduce:

1. Execute this code somewhere:

fun main() {
    val myBuggyUnifier = Unifier.naive(Substitution.of("X", Atom.of("a")))

    myBuggyUnifier.mgu(Atom.of("b"), Var.of("X"))
    
    println("You'll never see this printed, until issue solved")
}

Expected behaviour: mgu should return null and the println should be executed!

Since in this paper is stated

A solution of an equation, called a unifier, is any substitution ϑ, if it exists, which makes the two terms identical

So a Success Substitution should be called Unifier