Orbital library

orbital.logic.sign
Interface Expression

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

public interface Expression
extends 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
See Also:
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

Copyright © 1996-2009 André Platzer
All Rights Reserved.