orbital.logic.sign
Interface Signature

Type Parameters:

Sigma - the type of symbols kept in this interpretation.

All Superinterfaces:

java.util.Collection, java.lang.Iterable, java.util.Set, java.util.SortedSet

All Known Implementing Classes:

SignatureBase

public interface Signature
extends java.util.SortedSet

A signature Σ is the set of names of all entities in a certain context. Where a name in a signature is called a syntactic symbol. A signature is the vocabulary or alphabet of logical signs of which to build well-formed formulas. It is assumed to be provided effectively.

A signature Σ =: ⋃̇_τ Σ_τ often is partitioned into disjunct sets Σ_τ according to the types τ of its symbols. Then Σ_τ⊆Σ is the subset of symbols of type τ. It can also be partitioned into Σ₀, Σ₁, ... Σ_n according to the arity of its symbols. Constant-symbols are defined as functions of arity 0.

The elements in a signature are of type Symbol in order to ensure type-safety and arity dependency.

Author:

André Platzer

See Also:

ExpressionSyntax.scanSignature(java.lang.String), Expression.getSignature(), SortedSet, SignatureBase.EMPTY, SignatureBase.unmodifiableSignature(Signature)

Invariants:

∀s∈this: s instanceof Symbol ∧ sorted according to precedence

Structure:

extends java.util.SortedSet

Method Summary

Signature	difference(Signature sigma2) Returns the difference to another signature.
boolean	equals(java.lang.Object o) Checks two signatures for extensional equality.
Symbol	get(java.lang.String signifier, java.lang.Object[] arg) Returns the symbol with the specified signifier of a functor.
Symbol	get(java.lang.String signifier, Type maxType) Returns the symbol with the specified signifier.
int	hashCode() Get a hash code fitting extensional equality.
Signature	intersection(Signature sigma2) Returns the intersection of two signatures.
Signature	symmetricDifference(Signature sigma2) Returns the difference to another signature.
Signature	union(Signature sigma2) Returns the union of two signatures.

Methods inherited from interface java.util.SortedSet

comparator, first, headSet, last, subSet, tailSet

Methods inherited from interface java.util.Set

add, addAll, clear, contains, containsAll, isEmpty, iterator, remove, removeAll, retainAll, size, toArray, toArray

Method Detail

equals

boolean equals(java.lang.Object o)

Checks two signatures for extensional equality. Two signatures are equal if they contain the same symbols.

Specified by:

equals in interface java.util.Collection

Specified by:

equals in interface java.util.Set

Overrides:

equals in class java.lang.Object

hashCode

int hashCode()

Get a hash code fitting extensional equality. .

Specified by:

hashCode in interface java.util.Collection

Specified by:

hashCode in interface java.util.Set

Overrides:

hashCode in class java.lang.Object

get

Symbol get(java.lang.String signifier,
           java.lang.Object[] arg)

Returns the symbol with the specified signifier of a functor. Will only return symbols that are applicable to the specified arguments.

The most usual use of the arguments array is to check for its length to distinguish unary minus '-' from binary subtraction '-'. But in principle, type checking could be required as well.

Note: if there are multiple symbols that match the given signifier and arguments, which symbol will be selected is unspecified.

This method equals get(signifier, typeOf(args)→⊤).

Parameters:

signifier - the signifier of the symbol.

arg - the arguments that the functor belonging to the signifier is called with. null, or an array of length 0 can be used for zero arguments.

Returns:

the symbol that has the specified signifier and is applicable to arg, if exists. Returns null otherwise.

See Also:

get(String,Type)

Postconditions:

(RES = ι[s∈this (s.getSignifier().equals(signifier) ∧ succeedes(s.getType().on(typeOf(arg))))] ∨ RES=null) ∧ this.equals(OLD)

get

Symbol get(java.lang.String signifier,
           Type maxType)

Returns the symbol with the specified signifier. Will only return symbols that are compatible with the specified type, i.e. are subtypes of it.

Note: if there are multiple symbols that match the given signifier and type, which symbol will be selected is unspecified.

Parameters:

signifier - the signifier of the symbol.

maxType - the maximum type that the symbol can have.

Returns:

the symbol that has the specified signifier and type ≤ maxType, if exists. Returns null otherwise.

See Also:

get(String,Object[])

Postconditions:

(RES = ι[s∈this (s.getSignifier().equals(signifier) ∧ s.getType().subtypeOf(maxType))] ∨ RES=null) ∧ this.equals(OLD)

union

Signature union(Signature sigma2)

Returns the union of two signatures.

Returns:

sigma ∪ sigma2.

See Also:

Setops.union(java.util.Collection,java.util.Collection)

Postconditions:

RES == this ∪ sigma2 && RES.getClass() == getClass() && this.equals(OLD)

intersection

Signature intersection(Signature sigma2)

Returns the intersection of two signatures.

Returns:

sigma ∩ sigma2.

See Also:

Setops.intersection(java.util.Collection,java.util.Collection)

Postconditions:

RES == this ∩ sigma2 && RES.getClass() == getClass() && this.equals(OLD)

difference

Signature difference(Signature sigma2)

Returns the difference to another signature.

Returns:

sigma ∖ sigma2.

See Also:

Setops.difference(java.util.Collection,java.util.Collection)

Postconditions:

RES == this ∖ sigma2 && RES.getClass() == getClass() && this.equals(OLD)

symmetricDifference

Signature symmetricDifference(Signature sigma2)

Returns the difference to another signature.

Returns:

sigma Δ sigma2.

See Also:

Setops.symmetricDifference(java.util.Collection,java.util.Collection)

Postconditions:

RES == this Δ sigma2 && RES.getClass() == getClass() && this.equals(OLD)