3
$\begingroup$

Given a type hierarchy $(\tau,\sqsubseteq)$ and a signature $(VSym, FSym, PSym, \alpha)$, one says that the typing function $\alpha$ assigns to each variable symbol $x \in VSym$ a non-empty type $A \in \tau \setminus\{\bot\}$ and is written as:

$$ x: A \tag1$$

Furthermore, for every type $A \in \tau \setminus\{\bot\}$, there is a predicate symbol $\Xi A \in PSym$ called the type predicate which tells us if or not a certain $x$ is an instance of type $A$. We write it as:

$$x \Xi A \tag2$$

That makes me think what set constitutes the domain of a predicate symbol. Clearly, if the domain is $VSym$, then $(1)$ and $(2)$ mean exactly the same thing, and therefore, would be a redundancy of definition.

If not, which is surely the case, how do they differ? In particular, can you tell if a certain object is an instance of a certain type and not just a variable symbol with the given type assigned to it (or vice versa)?

More precisely, if a predicate symbol is a function from a certain domain to the set $\{\mathrm{True},\mathrm{False}\}$, what exactly is the domain of this map? Is there any overlap of this domain with $VSym$?

I am reading the chapter on first order logic from Deductive Software Verification – The KeY Book. (I am not fully sure if this question fits in a mathematics or a computer science forum.)

Thank you for your time.


Background:

Please refer to this document (the first couple of pages actually) to update yourself with the relevant ideas and definitions. Here's a brief summary.


A type hierarchy is a pair $\mathscr T = (\tau,\sqsubseteq)$, where

  1. $\tau$ is a set of type symbols;
  2. $\sqsubseteq$ is a partial ordering on $\tau$, called the subtype relation;
  3. there are two designated type symbols, the empty type $\bot \in \tau$ and the universal type $\top \in \tau$ with $ \bot \sqsubseteq A \sqsubseteq \top \forall A \in \tau$.

A signature (for a given type hierarchy $\mathscr T$) is a quadruple $\Sigma = (VSym, FSym, PSym, \alpha)$ of

  • a set of variable symbols $VSym$,
  • a set of function symbols $FSym$,
  • a set of predicate symbols $PSym$, and
  • a typing function $\alpha$,

such that

  • $\alpha(v) \in \tau_q := \tau \setminus\{\bot\}\ \forall v \in VSym$,
  • $\alpha(f) \in \tau_q^* \times \tau_q\ \forall f ∈ FSym$, where $\tau_q^*$ is the set of all (possibly empty) sequences of elements in $\tau_q$, and
  • $\alpha(p) \in \tau_q^*\ \forall p \in PSym$.
  • There is a function symbol $(A) \in FSym$ with $\alpha((A)) = ((\top),A)$ for any $A \in \tau_q$, called the cast to type A.
  • There is a predicate symbol $\doteq \in PSym$ with $α(\doteq) = (\top,\top)$.
  • There is a predicate symbol $\Xi A \in PSym$ with $\alpha(\Xi A) = (\top)$ for any $A \in \tau$, called the type predicate for type A.

Notation: We write

  1. $v : A$ for $\alpha (v) = A$,
  2. $f : A_1,...,A_n \to A$ for $\alpha(f)=((A_1,...,A_n),A)$,
  3. $p: A_1,...,A_n$ for $\alpha(p)=(A_1,...,A_n)$,
  4. $x \Xi A$ (read: $x$ is an instance of $A$) for $\Xi A(x)$,
  5. $x \doteq y$ for $\doteq(x,y)$.

NOTE: Some texts (such as the document linked above) implicitly do the type assignment carried out by $\alpha$ and write down the definition in the standard notation mentioned above.

$\endgroup$
  • $\begingroup$ Basically, you can't write $x:A$ inside the language. The ":" relation lives in the metatheory, only. Instead $x \Xi A$ is an expression inside the language (the theory). $\endgroup$ – chi May 31 '17 at 14:54
6
$\begingroup$

$x:A$ is a statement about objects in the formal system, like, for example, $\vdash 2+4:\texttt{int}$, whereas $x\Xi A$ is an expression in the formal system, like $\texttt{if}~ 2 + 4 ~\texttt{==}~5 ~\texttt{then}~ e_1~ \texttt{else} ~e_2$.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.