Orbital library

orbital.logic.imp
Interface Interpretation

Type Parameters:
Sigma - the type of symbols kept in this interpretation.
Denotation - the type of denotating objects.
All Superinterfaces:
java.util.Map
All Known Implementing Classes:
InterpretationBase

public interface Interpretation
extends java.util.Map

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

interpretation
an interpretation I:Σ→D is a family of maps I:ΣτDτ for each type τ, with Also we can identify (D0D)≅D, as well as ℘(D0)={∅,{()}}≅{True,False}. Interpretations are homomorphisms.
homomorphism
φ:T(Σ)→D is a homomorphism of (typed) Σ-algebras, i.e. a family of maps φ:T(Σ)τDτ, if
 
φ(υ(t)) = φ(υ)(φ(t)) for υ∈Σσ→τ, t∈T(Σ)≤σ
Especially
φ(υ(t1,…,tn)) = φ(υ)(φ(t1),…,φ(tn)) for υ∈Σn is a function, t1,…,tnT(Σ)
truth-functional
If for every interpretation I:Σ→D there is a unique continuation φ:T(Σ)→D that is a homomorphism of Σ-algebras, i.e.
φ|Σ = I and φ is homomorphic
Then the logic is called truth-functional, and that unique homomorphism φ is called the (expression) valuation or truth-function, which is again denoted by I.
"Evaluations are the homomorphic continuation of symbol interpretations."
Note that the homomorphism conditions for φ include
φ(¬P) = ¬φ(P), φ(P∧Q) = φ(P)∧φ(Q), φ(P∨Q) = φ(P)∨φ(Q), φ(P→Q) = φ(P)→φ(Q) etc.

If a logic is truth-functional, the semantics of a combined formula can be defined with the combined semantics of the components and junctors. Then the junctors are treated truth-functionally, that is, every junctor is defined by its corresponding function that maps the combined truth-values to resulting truth-values. This is denoted with truth-tables.

If we have a truth-functional logic, we can define the satisfaction relation with truth-functions

I ⊧ F :⇔ I(F) = true
The satisfaction relation defines the semantics of a formula. In effect, it encapsulates the details of truth-functions into a single relation. Although this may not instantly appear to be of advantage, we then receive the freedom of interchanging the satisfaction relation (or even any truth-functions underlying it).

An interpretation I is a satisfying Σ-Model of F, if:

I ⊧ F, i.e. the interpretation satisfies the formula.

theory
A set of formulas T⊆Formula(Σ) is a theory :⇔
TC(T) = {F∈Formula(Σ) ¦ T F}
T∩{F∈Formula(Σ) ¦ ModΣ(F)=∅} = ∅ xor T = Formula(Σ)
theory of a model set
The theory of a set of models M⊆Int(Σ) is
T := Theory(M) := {F∈Formula(Σ) ¦ ∀I∈M I ⊧ F}
This is the model-theoretic way of defining theories.
T is complete, i.e. ∀F∈Formula(Σ) (F∈T xor ¬F∈T).
theory of a formula set
The theory represented by the decidable set of formulas A⊆Formula(Σ) is
T := Theory(A) := C(A) = {F∈Formula(Σ) ¦ A F} = Theory(Mod(A))
A is called the presentation or axiomatization of the theory T which is said to be axiomatizable. The definition as consequence closure is the axiomatic way of defining theories.
T is semi-decidable.

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.

elementary equivalent
Two interpretations I:Σ→D, and J:Σ→E are elementary equivalent, iff
Theory({I}) = Theory({J})
i.e. they satisfy the same formulas of the logic L.
homomorphism
Let I:Σ→D, J:Σ→E be two interpretations.
 φ:DE is a homomorphism of interpretations, if
 
φ(I(f)(d1,…,dn)) = J(f)(φ(d1),…,φ(dn)) if f∈Σn is a function, d1,…,dnD
I(p)(d1,…,dn) ⇔ J(p)(φ(d1),…,φ(dn)) if p∈Σn is a predicate, d1,…,dnD
The interpretations I:Σ→D, and J:Σ→E are isomorphic if there is an isomorphism φ:DE, i.e. a bijective homomorphism. Isomorphic interpretations are elementary equivalent.

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.

Author:
André Platzer
See Also:
Logic.satisfy(orbital.logic.imp.Interpretation, orbital.logic.imp.Formula), Signature, Map, InterpretationBase.EMPTY(Signature), InterpretationBase.unmodifiableInterpretation(Interpretation)
Invariants:
(Σ == null ∨ keySet() ⊆ Σ) ∧ ∀(s,v)∈this s.getType().apply(v)
Structure:
extends java.util.Map
Note:
This interface could be strengthened by extending SortedMap instead of just Map.

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

equals

boolean equals(java.lang.Object o)
Checks two interpretations for extensional equality. Two interpretations are equal if both their signatures and interpretation objects are equal.

Specified by:
equals in interface java.util.Map
Overrides:
equals in class java.lang.Object

hashCode

int hashCode()
Get a hash code fitting extensional equality. .

Specified by:
hashCode in interface java.util.Map
Overrides:
hashCode in class java.lang.Object

getSignature

Signature getSignature()
Get the signature interpreted.


setSignature

void setSignature(Signature sigma)
Set the signature interpreted.

Throws:
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.
Preconditions:
sigma == null || keySet() ⊆ sigma

get

java.lang.Object get(java.lang.Object symbol)
Get the referent associated with the given symbol in this interpretation.

Overwrite along with other map operations like Set.contains(Object) to implement a different source for symbol associations.

Specified by:
get in interface java.util.Map
Throws:
java.util.NoSuchElementException - if the symbol is not in the current signature Σ.
Postconditions:
symbol.getType().apply(RES)

put

java.lang.Object put(java.lang.Object symbol,
                     java.lang.Object referent)
Set the referent associated with the given symbol in this interpretation.

Specified by:
put in interface java.util.Map
Throws:
java.util.NoSuchElementException - if the symbol is not in the current signature Σ.
TypeException - if the referent is not of the type of symbol.
Preconditions:
symbol.getType().apply(referent)

putAll

void putAll(java.util.Map associations)
Copies all of the associations from the specified map to this interpretation.

Specified by:
putAll in interface java.util.Map
Throws:
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.
Preconditions:
(Σ == null ∨ keySet() ⊆ Σ) ∧ ∀(s,v)∈associations

containsKey

boolean containsKey(java.lang.Object symbol)
Returns whether the specified symbol is contained in this interpretation assocation map.

Specified by:
containsKey in interface java.util.Map
Throws:
java.util.NoSuchElementException - if the symbol is not in the current signature Σ.

union

Interpretation union(Interpretation i2)
Returns the union of two interpretations.

Parameters:
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.)
Returns:
i ∪ i2.
See Also:
Setops.union(java.util.Collection,java.util.Collection)
Postconditions:
RES.getClass() == getClass() && this.equals(OLD)

Orbital library
1.3.0: 11 Apr 2009

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