Logic Notation in Prolog

There are (at least) two ways to represent e.g. logical formula in Prolog. One way is to define a bunch of operators in Prolog (and here we can take advantage of Unicode symbols if our Prolog supports it; I'm using SWI Prolog which works fine if you save your files as utf_8.)

    :- op( 500, fy, ¬).     % negation
    :- op(1000, xfy, ∧).    % conjunction
    :- op(1100, xfy, ∨).    % disjunction
    :- op(1110, xfy, →).    % implication

Then you can just write logical formulas with symbols and let the Prolog parser parse them (the following is valid Prolog source code with the above operator definitions in effect):

    p ∧ (p → q) → q

This says "P and (P implies Q) implies Q"

    ?- write(p ∧ (p → q) → q).
    p∧(p→q)→q
    true.

There's (at least) one wrinkle though, if you're not careful you can get weird problems. For example, if you remove the space before a negation symbol it causes a syntax error:

    ?- write(p ∧ (p →¬q) → q).
    ERROR: Syntax error: Operator expected
    ERROR: write(p ∧ (p
    ERROR: ** here **
    ERROR:  →¬q) → q) . 

Maybe this is due to an issue with priority or something?

The other way to represent notation in Prolog is to parse the formula as strings and then build regular Prolog datastructures to represent them.

Here's an example taken from two different places online that both describe simple type inference.

The first one presents code for type inference for the simply-typed lambda calculus while the second is to support a demonstration of Haskell's type inference for a certain expression (namely, "head . filter fst").

The simply-typed lambda calculus demo uses operators (with Unicode characters substituted for the original's ASCII) and includes an enviroment or context called "Γ" (Gamma) which maps values to their types (it's implemented as a list of ∷/2 pairs):

    :- op(150, xfx, ⊢).
    :- op(140, xfx, ∷).
    :- op(100, xfy, →).
    :- op(100, yfx, $).

    Γ ⊢    Term∷Type         :- atom(Term), member(Term∷Type, Γ).
    Γ ⊢ λ(A, B)∷Alpha → Beta :- [A∷Alpha|Γ] ⊢ B∷Beta.
    Γ ⊢   F $ A∷Beta         :- Γ ⊢ F∷Alpha → Beta, Γ ⊢ A∷Alpha.

While the Haskell demo spells out structure in standard Prolog terms:

    type(head,    arrow(list(A), A)).
    type(compose, arrow(arrow(B, C), arrow(arrow(A, B), arrow(A, C)))).
    type(filter,  arrow(arrow(A, bool), arrow(list(A), list(A)))).
    type(fst,     arrow(pair(A, _), A)).

    type([F, X], T):- type(F, arrow(A, T)), type(X, A).

One thing they both have in common is the pattern for application::

    Γ ⊢ F $ A∷Beta :- Γ ⊢ F∷Alpha → Beta, Γ ⊢ A∷Alpha.

    type([F, X], T) :- type(F, arrow(A, T)), type(X, A).

For clarity let's change the names in the first one to match the second, remove the "Gamma implies", and add some otherwise-unneccesary parentheses:

    (F $ X)∷T :- F∷(A → T), X∷A.

    type([F, X], T) :- type(F, arrow(A, T)), type(X, A).

Both of these statements say, "An application of function F to value X returns a value of type T if the type of F is 'function from type A to type T' and the type of X is A."

Here's a little translation table::

    (_$_) = [_,_]   (Application)
      ∷/2 = type/2
      →/2 = arrow/2

See? They're identical. (Except one uses operators and the other uses plain ol' Prolog.)

         (F $ X) ∷ T  :-      F ∷      (A → T) ,      X ∷ A .
    type([F , X] , T) :- type(F , arrow(A , T)), type(X , A).

If you translate the Haskell facts into operator form this is what they look like:

    head    ∷ [A] → A.
    compose ∷ (B → C) → (A → B) → (A → C).
    filter  ∷ (A → bool) → ([A] → [A]).
    first   ∷ p(A, _) → A.
    [F, X]  ∷ T :-
        F ∷ A → T,
        X ∷ A.

Neat, eh?

With the first one you can query:

    ?- type([[compose, head], [filter, fst]], T).
    T = arrow(list(pair(bool, _7900)), pair(bool, _7900)).

The operator form works too:

    ?- [[compose, head], [filter, first]] ∷ T.
    T = [p(bool, _10752)]→p(bool, _10752).