Logic Programming and Logic Meta Programming in TyRuBa

Language Reference (for release 5.10)

See also

Syntax in relation to Prolog

Tyruba's syntax is based on Prolog's syntax but has some differences.


Lexemes

Comments:

The conventions for comments are the same as those for Java. Some examples of comments:
   // This is a single line comment
/* This is a multi line
comment */

Literals

Lexemes for string literals and numbers are as in Java.

Note: although string literals can contain escape sequences like "\t" etc. These are recoginzed by the parser but not all escape sequences are currently handled by the language implementation. "\\" and "\"" work correctly. Do not assume any other escape sequences work.

Some examples:

   integers: 1234  -1234 0x4FA0
floating point: 0.9 1234.4E6 -9.9E-10
string: "This is a simple string"
"You can escape \" and \\ in a string"

Keywords

     These are "reserved" words in TyRuBa:

AS END MODES REALLY UNIQUE
BOUND EXISTS MULTI SEMIDET
DEFAULT FINDALL NONDET TEST
DET IS NOT TYPE

Variables and (Name) Constants

TyRuBa variables are distinguishable from name constants because variables start with a leading question mark.
CONSTANT ::= <LETTER> (<LETTER>|"_"|"."|<DIGIT>)*
Name constants match any legal Java identifier, including names qualified by a package name.

Examples:

   abc_def.ghiASSD
abx
AB
Snapshot
java.lang.Object

note: String literals and constants containing the same characters are equivalent. I.e. constants are just represented as string Literals. "abc" and abc are therefore equal to one another.

VARIABLE ::= "?" (<LETTER>|<DIGIT>)*
Examples
   ?X
?
?List1
?List2b
?number

The variable "?" has a special purpose. It is like the prolog variable _. Normally two occurrences of variables with identical names in a query or rule will be treated as "equal". However, for "?" each occurrence will be treated as a "fresh" variable. (i.e. imagine that they are implicitly followed by distinct number ?1, ?2, etc...

Quoted Code/Text Sequences

This is a mechanism built into TyRuBa to facilitate the assembly of text, such as for example Java code, error messages, etc...

Quoted code blocks start with a "{" and end at the first matching "}". I.e. the number of "{" and "}" must be balanced. Example:

   { This is a simple quoted text block
It may span multiple lines and contain
matched numbers of { and } as this
example shows.
}

Quoted code blocks may also contain logic variables like this:

   { This block contains a ?Variable and ?anotherVariable }

Question marks can be included by doubling them like this:

   { Do you want to include a question mark ?? 
Then just repeat it twice to avoid it being
treated as a ?variable
}

Quoted code blocks are useful to assemble pieces of code (or other text). Variables represent holes in the text where other text may be fitted in by binding the variable. Every kind of binding has some textual representation inside a quoted code block (which may differ from the normal way it is printed).

Type of element Syntax Example Printed inside { } as

Constant

java.lang.Object
"Zork!!!"
java.lang.Object
Zork!!!
Lists and Pairs [1,2,abc,def]
[]
[abcdef]
[[a,b,c],[1,2,3]]
12abcdef
prints nothing
abcdef
abc123
Compound terms person<Kris,DeVolder>
examples.Stack<int>
person<Kris,DeVolder>
examples.Stack<int>

Note: Lists occuring inside quoted text are printed without any separators or delimiters between elements. This is convenient in some situations (e.g. inserting snippets of text found by FINDALL) but not so convenient in others (e.g. when you use it to generate an error message text, and actually want the list to appear as printed with separators... this is a bit of a dilemma.)


Grammar

CompilationUnit ::= 
( IncludeDirective
| PredicateDeclaration
| UserDefinedTypeDeclaration
| Rule
| Query
) *
<EOF>

Directives

IncludeDirective  ::= "#include" <STRING_LITERAL>
Any file loaded by TyRuBa may contain #include directives. They look like
#include "a filename"
The filename is interpreted relative to the file (or URL) in which the include directive is encountered. Include directives in -i mode are not supported.

PredicateDeclaration ::= <STRING_LITERAL> "::" TypeList
[ "MODES" ( ModeDeclaration )* "END" ]
Each SimplePredicate must be declared before use (both in Rules and in Query). PredicateDeclaration contains the predicate's argument types and its available mode of execution.
For a more detailed explanation of predicate declaration, take a look at the TyRuBa tutorial.

UserDefinedTypeDeclaration ::= UserDefinedAtomicTypeDeclaration
| UserDefinedCompositeTypeDeclaration

UserDefinedAtomicTypeDeclaration ::= "TYPE" AtomicType "=" AtomicType ( "|" AtomicType )*
| "TYPE" AtomicType "AS" AtomicType
AtomicType can be declared as a union of AtomicTypes.
TYPE Vechicle = Car | Bicycle is a declaration for AtomicType "Vehicle" which is the union of AtomicTypes "Car" and "Bicycle". One thing to note is that "Car" and "Bicycle" must be declared before declaring "Vehicle".
All AtomicTypes corresponding to any class in the java.lang package are already declared. The way to declare an AtomicType that does not have any subtypes is to indicate what declared AtomicType is used to represent it.
For example: TYPE Car AS String declares AtomicType "Car" which is represented with String. The type system of TyRuBa only knows a constant is of type "Car" if there is a typecast on the constant. (More on typecasting in description of Term)

UserDefinedCompositeTypeDeclaration ::= "TYPE" CompositeType "=" CompositeType ( "|" CompositeType )*
| "TYPE" CompositeType "AS" (TupleType | ListType)
Similar to defining atomic type declaration, composite type declaration describes hierarchy between composite types. Please see TyRuBa tutorial for examples.

Rule ::= SimplePredicate [ ":-"  Expression ] "."

SimplePredicate ::= <IDENTIFIER> "(" TermList ")"
Rules are simply parsed and inserted into the rule base. Rules which do not have a condition (condition = the part after ":-") are called facts. Facts are basically just rules with a condition that is always true.

Query ::= ":-" Expression "."
Immediately after a query has been parsed it is launched in the current rule base. Its results are then printed on the standard error device.


Expressions

Expression    ::= Disjunction | ModeSwitchExpression
Disjunction ::= Conjunction ( ";" Conjunction )*
Conjunction ::= Predicate ( "," Predicate )*
The meaning of conjunctions (logical "and") and disjunctions (logical "or") are similar to Prolog; however, TyRuBa's mode system may decide to change the order of execution.

ModeSwitchExpression ::= ModeCase ( "|" ModeCase )* [ "|" DefaultModeCase ]
ModeCase ::= "BOUND" VariableList ":" Expression
DefaultModeCase ::= "DEFAULT" ":" Expression
purpose: A ModeSwitchExpression allows the developer to gain explicit control over the precise implementation and execution order of expressions for a predicate, depending on the binding modes of the variables. This is useful in cases where an expert developer decides he can implement some predicate more efficiently by providing varying implementations for different modes. It is technically possible to provide mode clauses which are not semantically equivalent, however this not a recommended use since it likely will caus confusion about the meaning of a predicate when it is being used (i.e. the meaning of an expression may change depending on the execution order in the context of its use, this execution order is, to some degree arbitrary!)

execution semantics: When a ModeSwitchExpression is evaluated, TyRuBa looks at each ModeCase in order. If the variables in the current ModeCase's VariableList is not all bound, then TyRuBa moves on to the next ModeCase. The DefaultModeCase is just a ModeCase that does not require any variable to be bound (i.e. this ModeCase can always be satisfied). If all the ModeCases fail and there is no DefaultModeCase, then TyRuBa is unable to evaluate this ModeSwitchExpression and a Mode Error is thrown. Otherwise, the Expression corresponding to the first ModeCase that can be satisifed is evaluated in the exact order in which it was typed.

note: The execution semantics as described above does not actually occur litterally because mode cases are resolved statically during type and mode checking, by the mode checker.
Predicate  ::= ExistsQuantifier
| FindAll
| ConvertToTypeExpression
| PredicateExpression
| NotFilter
| TestFilter
| UniqueQuantifier
| "(" Expression ")"

ExistsQuantifier ::= "EXISTS" VariableList ":" Expression
This expression succeeds when the enclosed expression returns a solution. This is used mainly inside NotFilter to ensure the Variables in VariableList are all bound.

FindAll ::= "FINDALL" "(" Predicate "," t1=Term "," t2=Term ")"
Very much like Prolog's findall. The predicate is evaluated. Then, t1 is instantiated with the returned bindings. This is done for each individual solution of the predicate and a list is constructed with all the resulting instantiations of t1. This list is then unified with t2.

ConvertToTypeExpression ::= "convertToType" "(" from=Term "," to=Term")"
This expression succeeds if from is of type Type and the type of to has an intersection with Type. This is used mainly to convert from a non strict type to a strict type. (More on strict type later. See also the example in the library specification.

NotFilter ::= "NOT" "(" Expression ")"
Only succeeds when Expression fails. Note all FREE variables in the NOT must become bound before the NOT is evaluated. The mode system may rearrange to make it so. Below are some examples:
:- NOT(foo(?x)) // illegal - ?x is not bound inside NOT
:- NOT(foo(?)) // legal
:- NOT(EXISTS ?x : foo(?x), bar(?x)) // legal

PredicateExpression ::= <IDENTIFIER> "(" TermList ")"
A PredicateExpression is an "atomic" predicate/goal to be matched with the rule base.

TestFilter ::= "TEST" "(" Expression ")"
Only succeeds when Expression succeeds. This is the same as evaluating Expression, except that bindings made while evaluating Expression will not be retained after the TEST expression. This expression effectively is equivalent to NOT(NOT(...))

UniqueQuantifier ::= "UNIQUE" VariableList Expression
This expression succeeds when the enclosed expression returns exactly one solution for the variables in VariableList, and fails otherwise. Note that TyRuBa automatically removes duplicates from any query's solutions. This means that replicated solutions will only be counted once.

Terms

Term ::= CompoundTerm
| List
| QuotedCode
| SimpleTerm
| Tuple

CompoundTerm ::= name = <IDENTIFIER> "<" TermList ">"
| name = <IDENTIFIER> List

TermList ::= Term [ "," TermList ]
Every compound term has a corresponding composite type according to the TyRuBa type system. Each composite type must be declared before any reference to it. For an example of using compound terms, please see TyRuBa tutorial.

List ::= "[" RealTermList "]"

RealTermList ::= Term [ "," RealTermList
| "|" Term ]
TyRuBa lists are similar to prolog lists, including the notation using "|" for matching rest lists.

QuotedCode ::= "{" <any_text_with_balanced_braces> "}"

SimpleTerm ::= Constant
| TypeCastedConstant
| Variable

Constant ::= <IDENTIFIER> 
| <INTEGER_LITERAL>
| <FLOATING_POINT_LITERAL>
| <STRING_LITERAL>
| "#" <IDENTIFIER> ("[]") // Java Class
| "/" (~["/"]|"\\/")* "/" // Regexp matcher

<IDENTIFIER> ::= <LETTER> (<LETTER>|"."|"*"|"+"|<DIGIT>)*
Integers, strings and floating point constants use the same syntax as Java's. Name constants are equivalent to strings, but it is convenient in the notation to be able to omit the quotes around them.
Names preceded by a hash "#" sign are Java class constants. These are resolved by the Java class loader at the time the TyRuBa program is loaded.
A sequence of characters in between two single "/" will be turned into an org.apache.regexp.RE object. The string in between the "/" may include "/" escaped by a "\". It must be in the syntax specified by the org.apache.RE API documentation. The predicates to match regular expressions to strings are re_match and regexp. The descriptions for them are in TyRuBa Library.

TypeCastedConstant ::= Constant "::" AtomicType
Constant can be typecasted to any user defined type as long as that type is a "leaf type" and it is represented by the native type of the constant. A type is a "leaf type" if it does not have any subtypes. Example:
TYPE StreetName AS String
TYPE StreetNumber AS Integer
TYPE StreetInfo = StreetName | StreetNumber
Granville::StreetName // legal
"10"::StreetName // legal
10::StreetNumber // legal

Granville::StreetNumber // illegal - StreetNumber is represented by Integer, not String
10::StreetName // illegal - StreetName is represented by String, not Integer
Granville::StreetInfo // illegal - StreetInfo is not a "leaf type" (must typecast it to StreetName in this case)

Variable ::= "?" (<LETTER>|<DIGIT>)*;

VariableList ::= "(" Variable [ "," Variable ] ")"
TyRuBa variables are identifiers preceded by a "?".

Tuple ::= "<" TermList ">"


Types

Type ::= AtomicType
| CompositeType
| ListType
| TupleType

TypeList ::= "(" Type [ "," TypeList ] ")"

AtomicType ::= <IDENTIFIER>

CompositeType ::= <IDENTIFIER> "<" TypeList ">"

ListType ::= "[" Type "]"

TupleType ::= "<" TypeList ">

TypeVariable ::= "?" (<LETTER>|<DIGIT>)*
Kind of Term Term Type of Term
Constant abc
100
123.123
abc::Foo
String
Integer
Float
Foo
Compound terms person<Kris, DeVolder>
info<abc, 123>
person<String, String>
info<String, Integer>
Lists and Pairs []
[1, 2]
[1, 2, abc, def]
[[], [1], [a]]
[foo<abc>]
[any Type]
[Integer]
[Object]
[[Object]]
[foo<String>]
Tuples <Kris, Devolder>
<abc, 123>
<String, String>
<String, Integer>
Unbound Variable ?xyz ?xyz

Note: ?xyz on the left and ?Xyz on the right are different. The one on the left is a logic variables whereas the one on the right is a type variable.



Modes

Mode ::= "SEMIDET"
| "DET"
| "NONDETMODE"
| "MULTI"
Mode Expected # of Result(s)
SEMIDET 0 - 1
DET 1
NONDET 0 - n
MULTI 1 - n


Mode Declaration

ModeDeclaration ::= BindingList [ "REALLY" ] "IS" Mode

Binding ::= "B"["OUND"]
| "F"["REE"]
Predicate declaration example:
  1. pred1 :: String
    MODES (B) IS SEMIDET END
    • declares pred1 to take one argument with type String
    • pred1 can only be executed with all its arguments bound

  2. pred1 :: String
    • is equivalent to (1)
    • TyRuBa automatically adds the mode SEMIDET to predicates with arguments all bound

  3. pred2 :: =Integer and pred3 :: Integer

  4. append :: [?a], [?a], [?a]
    MODES
    (B,B,F) IS DET
    (F,F,B) IS MULTI
    END
    • declares append to take three arguments with types of List with any element type; however, the three list element types must be compatible (have a common supertype)
      • append([1,2],[3,4],?x) // legal
      • append([1,2],[a,b],?x) // legal - String and Integer have common supertype (Object)
      • append([foo<abc>],[1],?x) // illegal - foo<String> and Integer are incompatible types
    • when the first and second arguments are bound, the third argument will be bound to exactly one value
    • when only the third argument is bound, the first and second arguments will be bound to at least one value

  5. list_ref :: =Integer, [?x], ?x
    MODES
    (B,B,F) REALLY IS SEMIDET
    END
    • the REALLY in the mode declaration tells TyRuBa that the declared mode is correct even if the system infers that it should return more result; the following illustrate why this would occur:
      • insert fact list_ref(0,[?x|?],?x).
      • then insert rule list_ref(?i,[?x|?r],?el) :- greater(?i,0), sum(?ii,1,?i), list_ref(?ii,?r,?el).
      • logically, we know that the fact and the rule cannot be satisfied together, since the fact requires the first argument to be 0 and the rule requires the first argument to be greater than 0; however, the type system only remembers that the first argument is of type =Integer in both the fact and the rule, and it will infer that there can be more than one result returned from using list_ref with the first two arguments bound to integers.
    • warning: TyRuBa will use mode information to optimize execution, but if mode is incorrectly declared and the actual number of results is greater than the declared mode, than TyRuBa will throw away the "extra" results and queries with the predicate would return incorrect result

Note: it is illegal to use predicate with bindings that are not declared unless these bindings are "more bound" than the ones that are declared. For example:
:- append(?x,?y,?z) // illegal
:- append([1,2],?x,[1,2,3]) // legal



Experimental Features

Infinite Loop Detection

TyRuBa has a caching mechanism that remembers query results of previously run queries. This speeds up things considerably. One of the more interesting aspects of this mechanisms is that it actually "remembers" a lazily computed result. This means that it "remembers" the query even before it has been computed. This allows queries which run into their own tails so to speak to be resolved in a more meaningful way than just looping infinitely. TyRuBa is relatively smart in trying other alternatives to find solutions and then later try a previously "blocked" path again. This mechanism is quite similar to "tabling" as in XSB. Here is a concrete example of what it can do that prolog cannot:

   married :: String, String
MODES
(F,F) IS NONDET
END

married(John,Mary).
married(?x,?y) :- married(?y,?x).
:- married(?a,?b).
Produces the following result: ##QUERY : married<?a,?b>
.H########
| ?b=Mary ?a=John |
| ?b=John ?a=Mary |################
##END QUERY
In Prolog such a thing would go into an infinite loop trying the
married(?x,?y) rule: married(?x,?y) :- married(?y,?x) :- married(?x,?y) :- ...

In TyRuBa this kind of situation is handled better due to a combination of the detection of queries "biting their own tail" and not keeping to accumulate duplicate results (this makes the search terminate when all swappings of marriage partners have been generated).

I have found this a useful feature (as have many other logic language implementers before me with tabling and other similar techniques), but in practice I tend to avoid the situation of really needing it and relying on it because:

  1. It clearly slows down the logic program. A rewrite somehow avoiding the situation is usually much better. (This is not necesarily a problem with the technique, but with the implementation in TyRuBa).
  2. It is not always intuitive to know when it will and will not have the desired effect. Infinite loops may unexpectedly appear "out of the blue" anyway (depending on which variables are bound etc.) note: this problem has been significanlty reduced by the mode system whose purpose it is exactly to avoid the situation where queries logically producing infinite number of results are avoided. Thus, the mode/type system makes the tabling feature a lot more useful and dependable!) 

The "#" character in the output is an indication of the loop detection mechanism backtracking over a "tail-biting" query.

TyNI: TyRuBa Native Interface

This option is no longer available; however there is another way to declare predicates that interact with Java code. It is still quite experimental but if you would like more information on it, email me at kdvolder@cs.ubc.ca


Kris De Volder <kdvolder@cs.ubc.ca>