logic is a vocab for an embedded language that runs on Factor with the capabilities of a subset of Prolog.

It is an extended port from tiny_prolog and its descendants, ruby-prolog.



In the DSL, words that represent relationships are called logic predicates. Use LOGIC-PRED: or LOGIC-PREDS: to declare the predicates you want to use. Logic variables are used to represent relationships. use LOGIC-VAR: or LOGIC-VARS: to declare the logic variables you want to use.

In the above code, logic predicates end with the character 'o', which is a convention borrowed from miniKanren and so on, and means relation. This is not necessary, but it is useful for reducing conflicts with the words of, the parent language, Factor. We really want to write them as: cat°, mouse° and creature°, but we use 'o' because it's easy to type.

Goals are questions that logic tries to meet to be true. To represent a goal, write an array with a logic predicate followed by zero or more arguments. logic converts such definitions to internal representations.




We will write logic programs using these goals.



The above code means that Tom is a cat and Jerry and Nibbles are mice. Use fact to describe the facts.



The above code asks, "Is Tom a cat?". We said,"Tom is a cat.", so the answer is t. The general form of a query is:



The parentheses are omitted because there was only one goal to be satisfied earlier, but here is an example of two goals:



Tom is a cat, but Jerry is not declared a cat, so f is returned in response to this query.

If you query with logic variable(s), you will get the answer for the logic variable(s). For such queries, an array of hashtables with logic variables as keys is returned.



The following code shows that if something is a cat, it's a creature. Use rule to write rules.



According to the rules above, "Tom is a creature." is answered to the following questions:



The general form of rule is:



This means Gh when all goals of Gb1, Gb2, ..., Gbn are met. This Gb1 Gb2 ... Gbn is a conjunction.



This Gh is called head and the { Gb 1Gb 2... Gbn } is called body.

Facts are rules where its body is an empty array. So, the form of fact is:



Let's describe that mice are also creatures.



To tell the truth, we were able to describe at once that cats and mice were creatures by doing the following.



;; is used to represent disjunction. The following two forms are equivalent:





logic actually converts the disjunction in that way. You may need to be careful about that when deleting definitions that you registered using rule, etc.

You can use nquery to limit the number of answers to a query. Specify a number greater than or equal to 1.



Use \+ to express negation. \+ acts on the goal immediately following it.



Other creatures might also like cheese...

You can also use sequences, lists, and tuples as goal definition arguments.

The syntax of list descriptions allows you to describe "head" and "tail" of a list.




You can also write a quotation that returns an argument as a goal definition argument.



When written as an argument to a goal definition, the following lines have the same meaning as above:





Such quotations are called only once when converting the goal definitions to internal representations.

membero is a built-in logic predicate for the relationship an element is in a list.



Recently, they moved into a small house. The house has a living room, a dining room and a kitchen. Well, humans feel that way. Each of them seems to be in their favorite room.



Don't worry about not mentioning the bathroom.

Let's ask who is in the kitchen.



These two consecutive underbars are called anonymous logic variables. Use in place of a regular logic variable when you do not need its name and value.

It seems to be meal time. What do they eat?



Here, facts and rules are used. They can be used for successive facts or rules.

Let's ask what Jerry consumes.



Well, what about Tom?



This is a problematical answer. We have to redefine consumeso.



We wrote about Tom before about common cats. What two consecutive exclamation marks represent is called a cut operator. Use the cut operator to suppress backtracking.

The next letter f is an abbreviation for goal { failo } using the built-in logic predicate failo. { failo } is a goal that is always f. Similarly, there is a goal { trueo } that is always t, and its abbreviation is t.

By these actions, "Tom consumes mice." becomes false and suppresses the examination of general eating habits of cats.



It's OK. Let's check a cat that is not Tom.



Jerry, watch out for the other cats.

So far, we've seen how to define a logic predicate with fact, rule, facts, and rules. Each time you use those words for a logic predicate, information is added to it.

You can clear these definitions with clear-pred for a logic predicate.



fact and rule add a new definition to the end of a logic predicate, while fact* and rule* add them first. The order of the information can affect the results of a query.



While clear-pred clears all the definition information for a given logic predicate, retract and retract-all provide selective clearing.

retract removes the first definition that matches the given head information.



On the other hand, retract-all removes all definitions that match a given head goal definition. Logic variables, including anonymous logic variables, can be used as goal definition arguments in retract and retract-all. A logic variable match any argument.



let's have them come back.



Logic predicates that take different numbers of arguments are treated separately. The previously used cato took one argument. Let's define cato that takes two arguments.



If you need to identify a logic predicate that has a different arity, that is numbers of arguments, express it with a slash and an arity number. For example, cato with arity 1 is cato/1, cato with arity 2 is cato/2. But, note that logic does not recognize these names.

clear-pred will clear all definitions of any arity. If you only want to remove the definition of a certain arity, you should use retract-all with logic variables.



You can trace logic's execution. The word to do this is trace.

The word to stop tracing is notrace.

Here is a Prolog definition for the factorial predicate factorial.

factorial(0, 1).

factorial(N, F) :- N > 0, N2 is N - 1, factorial(N2, F2), F is F2 * N.

Let's think about how to do the same thing. It is mostly the following code, but is surrounded by backquotes where it has not been explained.



Within these backquotes are comparisons, calculations, and assignments (to be precise, unifications). logic has a mechanism to call Factor code to do these things. Here are some example.






Use callback to set the quotation to be called. Such quotations take an environment which holds the binding of logic variables, and returns t or f as a result of execution. To retrieve the values of logic variables in the environment, use of or at.

The word unify unifies the two following the environment in that environment.

Now we can rewrite the definition of factorialo to use them.



Let's try factorialo.





logic has features that make it easier to meet the typical requirements shown here.

There are the built-in logic predicates (<), (>), (>=), and (=<) to compare numbers. There are also (==) and (\==) to test for equality and inequality of two arguments.

The word is takes a quotation and a logic variable to be unified. The quotation takes an environment and returns a value. And is returns the internal representation of the goal. is is intended to be used in a quotation. If there is a quotation in the definition of rule, logic uses the internal definition of the goal obtained by calling it.

If you use these features to rewrite the definition of factorialo:



Use the built-in logic predicate (=) for unification that does not require processing with a quotation. (\=) will be true when such a unification fails. Note that (\=) does not actually do the unification.

varo takes a argument and is true if it is a logic variable with no value. On the other hand, nonvaro is true if its argument is not a logic variable or is a concrete logic variable.

Now almost everything about logic is explained.