Autolog coding information

1- Builtin Autolog operators

The following builtin symbolic operators can be used by the programmar. The operators are listed in order of precedence: An operator listed before another binds more tightly in contexts without parens. Otherwise use parens. There is no fixed prior meaning assumed for the operators. The programmer's inference rules or rewite modulators determine intended semantics. 
   name (functor)
      ⊤           editor (22A4)  
      ⊥           editor (22A5)
      ∀           editor (2200)
      ∃           editor (2203)
      λ           editor (3BB)
      ∅           editor (2205)
      Π           editor (3A0)
      Σ           editor (3A3)
   unary prefix operator
      @ 
      - 
      ¬  option l editor (AC)
      ~ 
      # 
      ◇            editor (25C7)
      □            editor (25A1)
   binary infix operator
      =
      ≠   option =
      ≈   option x
      ≤   option <
      ≥   option >
      ∧            editor (2227)
      ∨            editor (2228)
      ->
      →            editor (2192) 
      \       
      <-     
      ←           editor (2190) 
      /  
      ↔            editor (2194)
      +
      *
      &
      ^
      ∘            editor (2218)
      ∙            editor (2219)
      ∩            editor (2229)
      ∪            editor (222A)
      ∈            editor (2208)
Symbols marked "editor (unicode)" are available to paste from the Autolog editor toolbar. The names can be used as functors with arity determined by source context. The rest of the symbols are keyboard symbols. The right arrows are right associative. The keyboard - is intended for use as a prefix "minus". For subtraction the programmer might use – (option -) as an infix subtraction operator, as in 3–5=-2. (See DUOPs below.)

2- Parametric functor terms and predicates

A Parametric functor term appears as a function application which itself is applied to an argument. Examples could be like the 
  p(a)(b)
  (f*g)(X)=f(X)*g(X)
  F(G∘H)=F(G)∘F(H)
  F(G∘H)(X)=F(G)(X)∘F(H)(X)
  (F(G)∘F(H))(X)=F(G)(X)∘F(H)(X)
The third expression is not functorial but the fourth and fifth expressions are. The last three expressions are impredicative (variable ops). Parametric functors must be expressed using applied function expressions such as the examples (no prefix or infix versions can be parsed).

3- Dynamic user specified operators (DUOPs)

The Autolog programmer can designate functional(...), prefix unary, infix binary operators using unicode symbols pasted into source code. The unicode symbols are copied from a convenient table source. For example, we could use op symbol α in various ways, 
     α(X,Y) => goal.   // functional predicate
     αX=X.             // prefix op in rewrite
     XαY => YαX.       // infix predicate in rule
     XαY=YαX,          // infix op in rewrite
It is of course not recommended to use operators in more than one intended arity/position context. The examples merely emphasize that the dynamic occurrence of the op in source code designates its intended position and arity usage. The built-in ops of the first section above have more precedence (bind tighter) than DUOPs (but all ops bind tighter using parens).

One finds lists of math/logic unicode symbols at various online locations, for example https://en.wikipedia.org/wiki/Mathematical_operators_and_symbols_in_Unicode
Test such a found symbol by copying it from the reference and then paste it in the source code. To test whether the symbol renders in a reasonable manner, compile the source and view the display of the operator in the AutoLog Viewer. The Autolog editor displays a handy list of symbols (Code menu, ⇑⌘I).

Operator words are possible, as in

mary' likes 'henry
which then displays in compiled form in the same mannner (with the single quotes).

3- Term builders

Currently, Autolog employs two term builders
{term|term} collection builder
(term,term) pair builder
See the Autolog Design Notebook for examples.

4- compile

Use the Compile menuitem under the Code menu, or use the Compile button on the toolbar. The current code in the Autolog editor is translated and displayed in the Autolog Viewer. Any errors are displayed in the AutoLog Viewer console.

If the input document contains autolog code lines surrounded by parens ≪ ... ≫ (keyboard option | and shift-option |, respectively), then the compile command will first extract the embedded autolog code befor compiling it. All text outside of these parens is treated as commentary, and the text ≪inside the parens≫ is presumed to be autolog code.

5- Skolem machine programing conventions

A goal rule has form A1, ... ,An => goal.
A false rule has form A1, ... ,An => false.
All false rules precede all goal rules in a program.
No rule has false or goal literals in the antecedent.
No conjunctive rule consequent contains a false or goal literal.
No disjunctive rule contains a false or goal literal.
The AutoLogAnalyzer does not currently detect exceptions to these conventions nor modify user input source codes. For example, see the README text that accompanies colog14I. Production versions of autolog will have a program code checker for these and other code form requirements or preferences.
2/15/2023