Orbital library

orbital.logic.sign
Interface Symbol

All Superinterfaces:
java.lang.Comparable, Typed, Variable
All Known Implementing Classes:
SymbolBase, UniqueSymbol

public interface Symbol
extends Typed, Variable, java.lang.Comparable

Represents a symbol of a signature. A symbol is a triple ⟨signifier, type, notation⟩ consisting of a signifier, its type specification, and its notation. Each symbol is either a constant symbol or a variable symbol.

Symbols can be names for various kinds of objects in the (logical) universe:

There should never be two equal symbols (i.e. with equal signifier, type, and notation) with one being constant, and the other variable. And it is also recommended not to use symbols of equal signifier and type but with different notations (except perhaps if they have the same semantics).

Author:
André Platzer
See Also:
Signature, Naming convention
Invariants:
true
Structure:
is String×Type×Notation.NotationSpecification, extends orbital.logic.trs.Variable, extends Comparable
Stereotype:
Structure

Method Summary
 boolean equals(java.lang.Object o)
          Compares two symbols for equality according to their three components.
 Notation.NotationSpecification getNotation()
          Get the notation used when this symbol occurs.
 java.lang.String getSignifier()
          Get the signifier representing this symbol.
 int hashCode()
          Returns the hash code value for this symbol.
 boolean isVariable()
          Whether this symbol is a variable symbol.
 void setNotation(Notation.NotationSpecification notation)
          Set the notation used when this symbol occurs.
 void setSignifier(java.lang.String signifier)
          Set the signifier representing this symbol.
 void setType(Type type)
          Set the type specification of this symbol.
 
Methods inherited from interface orbital.logic.sign.type.Typed
getType
 
Methods inherited from interface java.lang.Comparable
compareTo
 

Method Detail

equals

boolean equals(java.lang.Object o)
Compares two symbols for equality according to their three components. Two symbols are equal if they have the same signifier, type specification and notation. Then it should be asserted that they are either both variable, or both constant, because the sets of variable symbols and constant symbols are usually assumed disjunct.

Overrides:
equals in class java.lang.Object
Postconditions:
o instanceof Symbol → (RES ⇔ (getSignifier().equals(o.getSignifier()) ∧ getType().equals(o.getType()) ∧ getNotation().equals(o.getNotation())))

hashCode

int hashCode()
Returns the hash code value for this symbol. The hash code of a symbol is defined to be the bitwise exclusive or of its components: signifier, type specification, and notation.

Overrides:
hashCode in class java.lang.Object
Preconditions:
true
Postconditions:
getSignifier() xor getType() xor getNotation()

getSignifier

java.lang.String getSignifier()
Get the signifier representing this symbol.

Synonym(!): sign (C.S.Peirce), signifier (Saussure), token. Depending upon terminology, the "name" of a symbol is known as sign, signifier or token.

Generally the three constituents - according to C.S.Peirce - of a sign are (in their special notations, and with todays most common terminology)

Preconditions:
true

setSignifier

void setSignifier(java.lang.String signifier)
Set the signifier representing this symbol.

Preconditions:
signifier≠null

setType

void setType(Type type)
Set the type specification of this symbol.

Parameters:
type - the type specification τ of this symbol.
Preconditions:
type≠null

getNotation

Notation.NotationSpecification getNotation()
Get the notation used when this symbol occurs. This includes precedence and associativity information, as well. The notation is not truely part of the abstract syntax of a formal language, but still useful for formatting and parsing. For this reason, the notation is included as a non-obligate recommendation.

Returns:
the notation used when this symbol occurs.
Preconditions:
true

setNotation

void setNotation(Notation.NotationSpecification notation)
Set the notation used when this symbol occurs. This includes precedence and associativity information, as well.

Parameters:
notation - the notation used when this symbol occurs.
Preconditions:
notation≠null

isVariable

boolean isVariable()
Whether this symbol is a variable symbol.

Note that the distinction between variable symbols and constant symbols is independent of the distinction between variable and constant interpretant functions. Especially, it is independent of the arity of this symbol.

Even though in the case of first-order logic, only object variables can occur, higher-order logic also provides function-variable symbols and predicate-variables. Then there truly is the terminologically confusing special case of variable symbols for constant functions (i.e. functions of arity 0).

Specified by:
isVariable in interface Variable
Returns:
true if this symbol is a variable symbol, and false if this symbol is a constant symbol.
See Also:
Variable
Preconditions:
true
Postconditions:
RES==OLD(RES)

Orbital library
1.3.0: 11 Apr 2009

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