The IFF Namespace for Expression Languages

This document gives an introductory discussion of the IFF Namespace for Expression Languages (IFF-EXPR). The axiomatization is given separately.

Architecture

Expressions

In the IFF approach, First Order Logic (FOL) is factored into two main components, a "term component" and an "expression component", plus a third minor extensional component called the "equational component". The term component is determined by function symbols, whereas the expression component is mainly determined by relation symbols. The expression namespace (for the most part) ignores the term component by eliminating function symbols. The central concept in the expression namespace is the expression construction (we use the term "expression" where others use "formula"). In contrast to the term namespace, in the expression namespace the Lawvere construction (see the red sub-diagram in Figure 1) plays a secondary role, since it only consists of representing variations that are the residual aspect of term tuples when function symbols have been eliminated. Variations are maps of indicia, subsets of variables which allow a change of variables through substitution. In the full FOL namespace, expressions will be united with terms by replacing variations with term tuples.

In more detail, the basic notion of the IFF-EXPR namespace is that of an expression language (also called, signature and lexicon). Languages are related through language morphisms. Expressions and expression language morphisms form the category Expr-Lang. The concepts of variable and relation (Figure 1) are the defining attributes of expression languages. The central data structure in the IFF-EXPR is the concept of expression. This recursive construction over languages is the solution to a fixpoint equation (see the blue sub-diagram of Figure 1). In full, the expression construction gives an extended language, with an embedding map connecting a language to its expression extension. The concept of arity is an attribute defined on relations and expressions, in order of increasing generality. The arity of an expression is loosely a set-theoretic upper bound for the variables occurring freely in the expression. Arity is an indicia. Expressions can be either atomic or composite. Atoms are relation-variation pairs that match the relation arity to the variation index. The atom construction, and its relation and variation component attributes, is based upon the pullback along relation arity and variation index. Composites are defined by logical connectives and quantifiers. In the core, following existential graphs, we use only negations, conjunctions and existential quantifications. Other connectives and quantifiers can be defined in terms of these. The holds construction represents atoms as atomic expressions. The negation construction represents expressions as negative expressions. The conjunction construction represents expression subsets as conjunctive expressions. In the basic IFF representation of FOL, the expression subset construction is the power of expressions; in an extended IFF representation of FOL that follows categorical logic, the expression subset construction requires a common arity. The quantification construction represents expression cases as (existentially) quantified expressions. The case construction is a sum construction used by the quantification operator. The case construction, and its indication and projection component attributes, is the coproduct of expression arity. The concepts of composition and identity (Figure 1) are composite constructors for variations.

Figure 1: Basic Expression Functors and Natural Transformations

The basic architecture of expression languages is illustrated in Figure 1. This consists of three sub-diagrams – the expression sub-diagram (upper left), the arity sub-diagram (lower left) and the lawvere sub-diagram (right). The expression sub-diagram and the arity sub-diagram illustrate the fixpoint solution for expressions and the co-recursive definition of expression arity. The lawvere sub-diagram illustrates the Lawvere construction for variations. The fixpoint solution for expressions embeds atoms as atomic expressions via the holds operator, embeds expressions as negative expressions via the negation operator, embeds expression-subsets as conjunctive expressions via the conjunction operator, and embeds expression cases as (existentially) quantified expressions via the quantification operator. Atoms are projected into their relation and variation components, and relation symbols are embedded as atoms.

The nodes in Figure 1 represent basic functors from Expr-Lang the category of expression languages and expression language morphisms to Set the category of (small) sets and set functions. The edges in Figure 1 represent natural transformations between these basic functors. There are five simple functors var, rel, vrtn, case and expr, for variables, relation symbols, variations, expression cases and expressions, respectively. The first three are basic, the fourth is composite and the last is inductively defined. Based on these, there are three composite functors: var ο ℘, expr ο ℘ and vrtn ⊗ vrtn, for indicia (variable subsets), expression-subsets and composable variation-variation pairs, respectively. The ‘⊗’ symbol refers to a matched Cartesian product – the arity of the first variation matches the index of the second variation. Any of the natural transformations in Figure 1 must satisfy naturality conditions. Take for example the expression arity natural transformation

whose source category is the category of expression languages Expr-Lang, whose target category is the category of sets Set, whose source functor is the expression functor expr : Expr-Lang → Set, whose target functor is the indicia functor var ο ℘ : Expr-Lang → Set, and whose L^th component for any expression language L is the expression arity function #(L) : expr(L) → ℘var(L). Then, for any expression language morphism f : L₁ → L₂, expression arity must satisfy the commuting diagram expr(f) · #(L₂) = #(L₁) · ℘var(f), which represents two conditions: (1) the naturality condition of the expression arity natural transformation for the expression language morphism f, and (2) the fact that the expression language morphism f preserves expression arity. A similar assertion can be made for any of the natural transformations in Figure 1; and this is axiomatized in this namespace. In addition, a third condition holds for any of the Lawvere-related natural transformation axiomatized in this namespace. Take for example, the variation arity natural transformation

whose L^th component for any expression language L is the variation arity function #(L) : vrtn(L) → ℘var(L). Then, for any expression language morphism f : L₁ → L₂, variation arity must satisfy the commuting diagram vrtn(f) · #(L₂) = #(L₁) · ℘var(f), which represents three conditions: (1) the naturality condition of the variation arity natural transformation for the expression language morphism f, (2) the fact that the expression language morphism f preserves variation arity; and (3) the fact that the Lawvere functor preserves the target (arity) of variations.

Figure 2: Expression Monad Functors and Natural Transformations

• the expression monad endofunctor endo : Expr-Lang → Expr-Lang, which maps an expression language L to the extension expression language endo(L), whose variables are the same, but whose relations are L-expressions,
• the unit natural transformation η : id ⇒endo : Expr-Lang → Expr-Lang, whose source functor is the identity functor on Expr-Lang, whose target functor is the expression monad endofunctor endo, and whose L^th component is the embedding expression language morphism η(L) : L → endo(L), which is identity on variables and the expression embedding map on relations, and
• the multiplication natural transformation μ : endo ο endo ⇒endo : Expr-Lang → Expr-Lang, whose source functor is the expression monad endofunctor composed with itself, whose target functor is the expression monad endofunctor endo, and whose L^th component is the collapsing expression language morphism μ(L) : endo(endo(L)) → endo(L), which is identity on variables and the expression collapsing map on relations (expressions-on-expressions).

In contract to the universal algebra situation discussed above, this monad is not associated with free algebras, but with "free expression languages" – for any expression language L, the extension expression language endo(L) is free over L. We use this to extend the notion of a expression language morphism to the freer notion of a expression language interpretation where the image of source relation symbols is not restricted to target relation symbols, but can be mapped to target expressions. The algebraic semantics can likewise be extended.

Abstract Syntax

The notion of abstract syntax is a technical term introduced by John McCarthy: “The predicates and functions whose existence and relations define the syntax, are precisely those needed to translate from the language, or to define the semantics”. The abstract syntax of FOL expression languages is the highest meta-level needed in order to define the syntax and model theory of FOL expression languages. The orientation in the McCarthy statement is towards the notion of an abstract data type, which defines the abstract syntax and formal semantics of data types. In general, abstract syntax consists of a collection of synthetic/constructor operators, a collection of analytic/selector operators, and a collection of axioms that related the syntax. For recursive data types, the synthetic/constructor operators are unpacked from the initial (or final) fixpoint solution (bijection) of a set equation(s). The analytic/selector operators are inverse to the synthetic/constructor operators, and this is the content of the axiomatization for the abstract data type. In fact, the axioms form subcollections, which are in one-one correspondence with the synthetic/constructor operators (and their analytic/selector inverses). The analytic/selector functions are partial functions, each has an associated Boolean test for its domain, and the correct analytic programming style is to test for “in domain” before applying any of the analytic/selector functions. Finally, to quote McCarthy, “if both the analytic and synthetic functions are given, we do not have the difficult and sometimes unsolvable analysis problems that arise when languages are described synthetically only".

Initial Fixpoints

For any ω-continuous Set endofunctor F : Set → Set, there is an initial fixpoint solution X^@ to the equation F(X) ≅ X. Any such fixpoint solution has an increasing approximation sequence X₀ = Ø, X₁ = F(Ø), …,X_n+1 = F(X_n), … X^@ = lim_n(X_n) starting from the empty set, constructing each successive step by endofunctor application, and "ending" at the fixpoint solution. The expression data type is a recursive data type compactly axiomatized as the fixpoint solution

α : fixpt(L)(expr(L)) → expr(L)

(bijection) of the fixpoint set equation

with the fixpoint set operator fixpt(L)(X), which is the sum of (1) the constant set of atoms atm(L), (2) the variable set X, (3) the power set ℘X and (4) the coproduct of the arity function #_L : X → ℘expr(L). The synthetic/constructor operators are unpacked from the fixpoint solution bijection α. For any expression language L, the set of expressions expr(L) and the expression arity function #_L : expr(L) → ℘var(L) are corecursively defined. The case component of the expression set is the coproduct of the arity function case(L) = ∑(#_L), and the source of the arity function is the expression set. The approximation sequence for the fixpoint solution of expressions starts as: X₀ = Ø, X₁ = atm(L) + true, … , and ends as the complete expression set X^@ = expr(L)in the limit (fixpoint), where atm(L) is a set constant and true is the conjunction of the empty subset of the empty set. In co-recursive parallel, the arity function approximation sequence starts as the empty arity function #_L : Ø → ℘var(L) at step 0, the atomic arity function #_L : atm(L) + true → ℘var(L) at step 1 where the arity of true is empty, … , and ends as the complete expression arity function #_L : expr(L) → ℘var(L) in the limit (fixpoint). The coproduct of these approximate arity functions is clearly increasing.

Example

The classic case of an abstract datatype is the stack datatype. This can be used to guide us in specifying the abstract syntax for FOL expression languages. An axiomatization for stack goes as follows:

• Since this is parametric, there is a name for the parameter type ‘P’. There is a name for the stack datatype ‘stk(P)’.

• There is a collection of synthetic/constructor operators on stacks:

  empty(P) : stk(P)

  push(P): P ×stk(P) → stk(P)

  where ‘empty(P)’ denotes the empty stack and ‘push(P)(p, s)’ places the item p ∈ P of type P onto the top of stack s ∈ stk(P). The stack data type is a recursive data type compactly axiomatized as the fixpoint solution

  α : (1 + P ×stk(P)) → stk(P)

  (bijection) of the simple linear fixpoint set equation

  1 + (P ×X) ≅ X

  where the synthetic/constructor operators are unpacked from the fixpoint solution bijection α.

• There is a collection of analytic/selector operators on stacks with the two subgroup clusters in one-one correspondence with the two synthetic/constructor operators (their inverse):

  is-empty(P) ⊆ stk(P)

  is-nonempty(P) ⊆ stk(P)
  top(P) : stk(P) → P
  pop(P)  : stk(P) → stk(P)

  where ‘is-empty(P)(s)’ is the Boolean test that returns true when the stack s ∈ stk(P) is empty and false otherwise, ‘is-nonempty(P)(s)’ is the complementary Boolean test, ‘top(P)(s)’ returns the “top” of stack s ∈ stk(P), and ‘pop(P)(s)’ returns the “rest” of stack s ∈ stk(P). Since both top and pop are partial functions whose domain is the set of nonempty stacks, the correct analytic programming style is to test for nonempty stack before applying either of these functions.

• These operators satisfy the defining stack abstract data type semantics:

  is-nonempty(P)(empty(P))

  which states that the empty stack is empty.

  ∀(p : P, s : stk(P)) (is-nonempty(P)(push(P)(p, s)) & top(P)(push(P)(p, s)) = p & pop(P)(push(P)(p, s)) = s)

  which states that the result of a push is a nonempty stack, whose top is the thing pushed and whose pop is the original stack.

  ∀(s : stk(P)) (is-nonempty(P)(s) ⇒ (push(P)(top(P)(s), pop(P)(s)) = s))

  which states that every nonempty stack is constructible using the push operator from its top and pop.

Expressions

Figure 3: The Expression Fixpoint Solution

Turning now towards the IFF first order logic languages, we need to axiomatize the abstract syntax for terms and expressions. For simplicity in the IFF expression languages, we will just express the traditional FOL part, but we do not express the FOL term operators or FOL term abstract data typesemantics and we do not include equations, but we do express all of the core IFF FOL expression abstract syntax. An axiomatization for stack goes as follows.

The abstract syntax of expression languages is illustrated in Figure 3. The abstract syntax of FOL expressions is parametric: there is a name for the parameter language or lexicon ‘L’ and also a name for FOL expressions ‘expr(L)’. There is a collection of synthetic/constructor operators, a collection of analytic/selector partial operators and axioms that relate the two collections.

There is a collection of four synthetic/constructor operators on expressions:

where '◊ _L((R, α))’ constructs the atomic expression of an arbitrary atom (R, α) ∈ atm(L) = ∪_{X∈ var(L)} rel( L)(X) ×vrtn( L)^X consisting of an X-ary relation symbol R ∈ rel( L)(X) and a variation α ∈ vrtn( L)^X with index X, ‘¬_L(φ)’ constructs the negation of an arbitrary L-expression φ ∈ expr(L), ‘Λ _L({φ₁, φ₂, …, φ _n})’ constructs the conjunction of an arbitrary subset of L-expressions {φ₁, φ₂, …, φ _n} ∈ ℘ expr(L), and ‘∃_L((φ,  x))’ constructs the existential quantification of an arbitrary expression case (φ, x) ∈ case(L) ⊆  expr(L)× var(L) consisting of an arbitrary L-expression φ ∈ expr(L) and a variable x ∈ var(L) with x ∈ arity(L)(φ). The four synthetic/constructor operators are individually injective and jointly surjective.

There is a collection of analytic/selector operators on expressions, with the four subgroup clusters in one-one correspondence with the four synthetic/constructor operators (their inverses):

These operators satisfy the defining FOL expression abstract syntax (abstract datatype semantics).

Atomic

which states that any FOL expression constructed by the holds operator is atomic and is decomposable into the original relation symbol and variation.

which states that every atomic FOL expression is constructible using the holds operator on its component relation and variation.

Negative

which states that any FOL expression constructed by the negation operator is negative and is decomposable into the original L-expression ψ ∈ expr(L).

which states that every negative expression is constructible using the negation operator on the underlying expression.

Conjunctive

which states that any FOL expression constructed by the conjunction operator is conjunctive and is decomposable into the original L-expression subset Φ ∈ ℘ expr(L).

which states that every conjunctive expression is constructible using the conjunction operator on the underlying expression subset.

Existential Quantification

which states that any expression constructed by the existential uantification operator is existentially quantified and is decomposable into the original L-case (φ, x) ∈ case(L) consisting of an arbitrary L-expression φ ∈ expr(L) and a variable x ∈ var(L) with x ∈ arity(L)(φ).

which states that every existential expression is constructible using the existential quantification operator on its component expression and bound variable.

Partition

Finally, following John McCarthy we require that each expression satisfy exactly one of these Boolean predicates. That is, that an expression is either (1) an atom, (2) a negation, (3) a conjunction or (4) an existential quantification,

but not any two such things (there are 6 possibilities).

That is, that those four domains partition the set of expressions. Actually, these two axioms are embedded within the fixpoint solution and we are just making them explicit here.

The SUO-IFF documents contain many unicode characters, and so require a recent browser. But even some recent browsers fail to render SUO-IFF properly. You can test your browser here.