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:

• function-symbols for functions of type σ→τ. A function f of arity (number of arguments) n is sometimes denoted as f/n. Function-symbols especially include
  • constant symbols of type ι (as functions of arity 0).

    Note

    however, that we could as well avoid constant symbols, and just use defined free variables, instead. Or if we restrict sets of formulas to finite sets, then we could just as well turn constants into existentially quantified variables.
• predicate-symbols for relations of type (σ)
  • atomic propositions of type ο (as predicates of arity 0).
  • properties of objects (represented as unary predicates).
  • relations between objects (represented as n-ary predicates).
• types τ of type * and the corresponding type identifier predicates τ of type (⊤).
• type constructors, f.ex. of type (*→*)→* or any other kind.
• variables x of a set V⊆Σ, where
  • object variables are variable terms of type ι.
  • function-variables are variable "frames" of functions.
  • predicate-variables are variable "frames" of relations.

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)

• signifier
• signified (especially in computer science these are often C.S.Peirce's interpretants).
• object

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)