orbital.logic.sign
Interface ExpressionSyntax

All Superinterfaces:

ExpressionBuilder

All Known Subinterfaces:

Logic

All Known Implementing Classes:

ClassicalLogic, FuzzyLogic, MathExpressionSyntax, ModalLogic

public interface ExpressionSyntax
extends ExpressionBuilder

Defines general methods for constructing and handling expressions of a formal language. Implementations of this interface are responsible for analyzing and constructing expressions (like terms, formulas) in the language of the corresponding term algebra defining a specific abstract syntax.

ExpressionSyntax defines a formal language over an alphabet and thus has a corresponding description with a Chomsky grammar defining its abstract syntax. It only defines the abstract syntax in terms of composition (in the sense of semiotics) of signs, whilst the concrete syntax is determined by the parser and the notations of the symbols involved. Implementations define the syntax for the set of legal expressions over a given signature Σ (including a set V of variables and any core symbols). Its language L(Σ) is the set of all well-formed expressions according to this syntax. It is usually a requirement that this language L(Σ) is a decidable set of finite objects over the alphabet Σ, and the alphabet Σ itself is decidable, as well.

Note that the null pointer null is neither an expression nor a symbol, i.e. we generally assume that null∉L(Σ)∪Σ.

Author:

André Platzer

Invariants:

true

Method Summary

Signature	coreSignature() Get the core signature which is supported by the language of this expression syntax.
Expression	createExpression(java.lang.String expression) Create a term representation by parsing a (compound) expression.
Signature	scanSignature(java.lang.String expression) Scan for the signature Σ of all syntactic symbols in an expression.

Methods inherited from interface orbital.logic.sign.ExpressionBuilder

compose, createAtomic

Method Detail

coreSignature

Signature coreSignature()

Get the core signature which is supported by the language of this expression syntax.

The core "signature" contains the logical signs that inherently belong to this term algebra and are not subject to interpretation. Logical signs are logical constants like true, false, and logical operators like ¬, ∧, ∨, →, ∀, ∃. The latter are also called logical junctors.

Note that some authors do not count the core "signature" as part of the proper signature Σ but would rather call it "meta"-signature.

Returns:

the core signature that is valid for every expression following this syntax. Elements in the core signature all have a fixed interpretation.

See Also:

Logic.coreInterpretation()

Postconditions:

RES == OLD(RES) ∧ RES unmodifiable

scanSignature

Signature scanSignature(java.lang.String expression)
                        throws ParseException

Scan for the signature Σ of all syntactic symbols in an expression.

However, note that this method does not necessarily perform rich type querying. Especially for user-defined functions with an arbitrary argument-type structure, it is generally recommended to construct the relevant signature entries explicitly.

Parameters:

expression - the expression that should be scanned for symbol names.

Returns:

Signature of the syntactic symbols in expression except those of the core signature.

Throws:

ParseException - (optional) when the expression is syntactically malformed. Either due to a lexical or grammatical error. (optional behaviour for performance reasons). Will not throw ParseExceptions if createExpression would not either.

See Also:

coreSignature(), "Factory Method"

Preconditions:

expression∈L

Postconditions:

createExpression(expression) instanceof Formula ⇒ createExpression(expression).getSignature().equals(scanSignature(expression))

createExpression

Expression createExpression(java.lang.String expression)
                            throws ParseException,
                                   TypeException,
                                   java.lang.IllegalArgumentException

Create a term representation by parsing a (compound) expression.

In fact, parsing expressions is only possible with a concrete syntax. So implementations of this method are encouraged to define and parse a standard notation which can often be close to the default notation of the abstract syntax.

Parameters:

expression - the compound expression to parse. A string of "" denotes the empty expression. However note that the empty expression may not be accepted in some term algebras. Those parsers rejecting the empty expression are then inclined to throw a ParseException, instead.

Returns:

an instance of Expression that represents the given expression string in this language.

Throws:

ParseException - when the expression is syntactically malformed. Either due to a lexical or grammatical error.

TypeException - if the expression produces a type error. Note that type errors are still a kind of syntactic errors, but should be separated from pure parse exceptions in order to simplify distinction for exception handlers.

java.lang.IllegalArgumentException - if the symbol is illegal for some reasons. This may occur like in ExpressionBuilder.createAtomic(Symbol), and due to the same reasons. However, most of the causes (like f.ex. spaces in the signifier) cannot occur here anyway, except when the parser underlying this method's implementation had errors.

See Also:

Factory Method

Preconditions:

expression∈L(scanSignature(expression))

Note:

could just as well be renamed to parseExpression(String)