Orbital library

All Superinterfaces:
Typed
All Known Subinterfaces:
Expression.Composite, Formula, Formula.Composite
All Known Implementing Classes:
LogicBasis

`public interface Expressionextends Typed`

An interface for representations of expressions.

This interface is implemented by objects representing syntactic expressions like those created by `ExpressionBuilder.createAtomic(Symbol)`, `ExpressionBuilder.compose(Expression,Expression[])`, or `ExpressionSyntax.createExpression(String)`. Objects representing compound expressions implement `Expression.Composite`, which can be used for decomposition and analysis of compound expressions.

Given a `signature` Σ we define a general term algebra and thus the (abstract) syntax of the expressions. However, the abstract syntax notation does not say anything about the particular syntax.

free algebra of terms
The free algebra of terms over a signature Σ is a universal Σ-algebra (with ∅ as axioms) and also an instance of it. It is defined by
 T(Σ) := ⋃̇τ T(Σ)τ The terms (or expressions) of `type` τ are T(Σ)τ := Στ `atomic symbols` ∪ {υ(t) ¦ υ∈T(Σ)σ→τ and t∈T(Σ)≤σ} `composites` (ascriptors) be minimal, i.e. min fix The corresponding abstract syntax is T(Σ)τ → Στ `atomic symbols` | T(Σ)σ→τ (T(Σ)≤σ) `composites` (ascriptors) The terms of subtypes of τ are T(Σ)≤τ := ⋃ρ≤τ T(Σ)ρ
Note that the case of composite symbols also includes compound symbols with compositors of higher arity n and type σ1×σ2×…×σnτ by formally setting σ := σ1×σ2×…×σn. This brief notation is justified formally by `currying` or product construction. Also note that υ is not restricted to functions and predicates, but is a meta-variable that may stand for any syntactic compositor.

With the above decomposition, terms are a graded magma with the magma Τ of types as graduation. Also Σ⊆T(Σ) operates (left and right) on T(Σ) by an action with which the graduation is compatible. However the compositions involved are partial and may result in errorneous type ⊥ or undefined terms.

For a set X with Σ∩X⊆Σ0, T(Σ∪X) is also a Σ-algebra of terms over Σ generated by X.

Author:
André Platzer
`ExpressionBuilder`, `ExpressionBuilder.createAtomic(Symbol)`, `ExpressionBuilder.compose(Expression,Expression[])`, `ExpressionSyntax.createExpression(String)`

Nested Class Summary
`static interface` `Expression.Composite`
The base interface for all composite expressions that are composed of other expressions.

Method Summary
` Signature` `getSignature()`
Get the subsignature appearing in this expression.

Methods inherited from interface orbital.logic.sign.type.Typed
`getType`

Method Detail

### getSignature

`Signature getSignature()`
Get the subsignature appearing in this expression.

Returns:
the subset of Σ consisting of those symbols that occur in this expression.

Orbital library
1.3.0: 11 Apr 2009