
Orbital library  
PREV CLASS NEXT CLASS  FRAMES NO FRAMES  
SUMMARY: NESTED  FIELD  CONSTR  METHOD  DETAIL: FIELD  CONSTR  METHOD 
Sigma
 the type of symbols kept in this interpretation.Denotation
 the type of denotating objects.public interface Interpretation
An interpretation associates the symbols in a signature with the entities in the world (for semantics). The arbitrary symbols in the signature are given a meaning with an interpretation, only.
In principle, semantics of syntactic expressions are usually defined with denotational semantics for interpretations, with operational semantics for a calculus, and sometimes with algebraic semantics or logical semantics.
A (denotational) interpretation is a mapping from signs to referents. More precisely
type
τ to elements of the class I(τ):=D_{τ} ≠ ∅.
Especially in computer science, the class I(τ) is often assumed to be a set, even though this is rather irrelevant.
"Wilfrid Hodges. Elementary Predicate Logic. In: Dov M. Gabbay and F. Guenther. Handbook of philosophical logic Volume 1 2nd edition. paragraph 17 theorem 10"
φ:T(Σ)→D is a homomorphism of (typed) Σalgebras, i.e. a family of maps φ:T(Σ)_{τ}→D_{τ}, if  
φ(υ(t))  = φ(υ)(φ(t))  for υ∈Σ_{σ→τ}, t∈T(Σ)_{≤σ}  
Especially  
φ(υ(t_{1},…,t_{n}))  = φ(υ)(φ(t_{1}),…,φ(t_{n}))  for υ∈Σ_{n} is a function, t_{1},…,t_{n}∈T(Σ) 
"Evaluations are the homomorphic continuation of symbol interpretations."Note that the homomorphism conditions for φ include
If a logic is truthfunctional, the semantics of a combined formula can be defined with the combined semantics of the components and junctors. Then the junctors are treated truthfunctionally, that is, every junctor is defined by its corresponding function that maps the combined truthvalues to resulting truthvalues. This is denoted with truthtables.
If we have a truthfunctional logic, we can define the satisfaction relation with truthfunctions
An interpretation I is a satisfying ΣModel of F, if:
In addition to this syntactic aspect, theories, when applied to a particular domain, should just as well explain observed facts.
Now we consider possible equivalence relations of interpretations.
φ:D→E is a homomorphism of interpretations, if  
φ(I(f)(d_{1},…,d_{n}))  = J(f)(φ(d_{1}),…,φ(d_{n}))  if f∈Σ_{n} is a function, d_{1},…,d_{n}∈D  
I(p)(d_{1},…,d_{n})  ⇔ J(p)(φ(d_{1}),…,φ(d_{n}))  if p∈Σ_{n} is a predicate, d_{1},…,d_{n}∈D 
An interpretation associates each sign in the signature Σ with an object value, its interpretation. Especially, our interpretations include valuations (variable assignments). Valuations are a technique introduced by Tarski, for dealing with the semantics of quantifiers.
Logic.satisfy(orbital.logic.imp.Interpretation, orbital.logic.imp.Formula)
,
Signature
,
Map
,
InterpretationBase.EMPTY(Signature)
,
InterpretationBase.unmodifiableInterpretation(Interpretation)
Nested Class Summary 

Nested classes/interfaces inherited from interface java.util.Map 

java.util.Map.Entry 
Method Summary  

boolean 
containsKey(java.lang.Object symbol)
Returns whether the specified symbol is contained in this interpretation assocation map. 
boolean 
equals(java.lang.Object o)
Checks two interpretations for extensional equality. 
java.lang.Object 
get(java.lang.Object symbol)
Get the referent associated with the given symbol in this interpretation. 
Signature 
getSignature()
Get the signature interpreted. 
int 
hashCode()
Get a hash code fitting extensional equality. 
java.lang.Object 
put(java.lang.Object symbol,
java.lang.Object referent)
Set the referent associated with the given symbol in this interpretation. 
void 
putAll(java.util.Map associations)
Copies all of the associations from the specified map to this interpretation. 
void 
setSignature(Signature sigma)
Set the signature interpreted. 
Interpretation 
union(Interpretation i2)
Returns the union of two interpretations. 
Methods inherited from interface java.util.Map 

clear, containsValue, entrySet, isEmpty, keySet, remove, size, values 
Method Detail 

boolean equals(java.lang.Object o)
equals
in interface java.util.Map
equals
in class java.lang.Object
int hashCode()
hashCode
in interface java.util.Map
hashCode
in class java.lang.Object
Signature getSignature()
void setSignature(Signature sigma)
java.lang.IllegalArgumentException
 if sigma does not contain a symbol which is interpreted in the current assocation map.
This is not checked if sigma is null
.java.lang.Object get(java.lang.Object symbol)
Overwrite along with other map operations like Set.contains(Object)
to implement
a different source for symbol associations.
get
in interface java.util.Map
java.util.NoSuchElementException
 if the symbol is not in the current signature Σ.java.lang.Object put(java.lang.Object symbol, java.lang.Object referent)
put
in interface java.util.Map
java.util.NoSuchElementException
 if the symbol is not in the current signature Σ.
TypeException
 if the referent is not of the type of symbol.void putAll(java.util.Map associations)
putAll
in interface java.util.Map
java.lang.IllegalArgumentException
 if associations does contain a symbol which is not contained in the signature.
This is not checked if Σ is null
.
TypeException
 if one of the values is not of the type of its symbol.
java.lang.NullPointerException
 if associations is null
.boolean containsKey(java.lang.Object symbol)
containsKey
in interface java.util.Map
java.util.NoSuchElementException
 if the symbol is not in the current signature Σ.Interpretation union(Interpretation i2)
i2
 the interpretation to merge with this one, resulting in a new interpretation.
(If a symbol is contained in both interpretations, the value of i2 will precede over
the value of this.)
Setops.union(java.util.Collection,java.util.Collection)

Orbital library 1.3.0: 11 Apr 2009 

PREV CLASS NEXT CLASS  FRAMES NO FRAMES  
SUMMARY: NESTED  FIELD  CONSTR  METHOD  DETAIL: FIELD  CONSTR  METHOD 