Syntax

The syntax of yarn is not completely defined yet so much of this is tentative. I will attempt to keep the syntax in the yarn wiki self consistent.

The syntax of yarn is composed of predicates, connectives, and modal operators. Predicates are defined by a special relation that maps predicate names to their definitions.

• & is conjunction. Read this as "and"
• + is disjunction. Read this as "or"
• ¬ is negation. Read this as "not"
• : is binding. Read this as "bind"
• * is time ordered conjunction. Read this as "sequence" or "seq"
• v is time ordered disjunction. Read this as "branch"

The operators all have thier usual meaning in intuisionistic logic. Bind is somewhat like the stepwise operator on a valuation in the fixed point semantics (NOTE: I think this is correct, please check). Bind causes a monotonic increase in the set of unified variables. If the variable already exists with a binding the bindings are unified, or the branch fails. In particular it is important to remember that in general A is not equivelent to ¬¬A except for regular atoms (in the sense of a regular element of a Heyting Algebra). Atoms must be defined as regular explicitly.

A predicate can be defined in the following way.

Notice that parent obtains its value by means of the binding operation. The first element of a form must either be one of the connectives, a modal operator, or a predicate. The implementation of the predicate is determined by looking in the current valuation. The definition of the predicate may at this point be substituted for the predicate.