Orbital library

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 Σ0, Σ1, ... Σ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)

Orbital library
1.3.0: 11 Apr 2009

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