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 σ₁×σ₂×…×σ_n→τ by formally setting σ := σ₁×σ₂×…×σ_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⊆Σ₀, 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.