2
$\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$ I don't think it is off-topic here, but it would probably fit better and reach a more relevant audience on the CS StackExchange: cs.stackexchange.com On either site, it would be helpful to include the relevant definitions from the book for people who don't have access to the book. $\endgroup$ – Derek Elkins May 30 '17 at 22:36
  • $\begingroup$ I have updated the question with necessary background. :) $\endgroup$ – Nanashi No Gombe May 30 '17 at 22:54
  • $\begingroup$ I looked at that technical report before commenting. It's definitions differ from what you state, particularly it's definition of "signature" lacks $\alpha$ or some analogue. Unless I missed it, it's also completely lacking the $\Xi$ operator. $\endgroup$ – Derek Elkins May 30 '17 at 23:04
  • $\begingroup$ $\alpha$ is implicit. That document summarises the elaborate definition I have introduced in my recent edit. $\endgroup$ – Nanashi No Gombe May 31 '17 at 4:27
4
$\begingroup$

There's a distinction between syntax and semantics and between talking about the logic (meta-logic) and talking within the logic.

$\alpha$ and the $t : A$ notation is talking about the logic, and particularly which terms and formulas are in it. If we have $1+x \in \text{Trm}_\mathsf{Int}$, to know if this is a well-formed term of type $\mathsf{Int}$ requires knowing what the type of $+$, $1$, and $x$ are, e.g. $+ : \mathsf{Int}\times\mathsf{Int}\to\mathsf{Int}$, $1 :\,\to\mathsf{Int}$, and $x:\mathsf{Int}$. Given these we can verify with general rules that $1+x$ is well-formed and has type $\mathsf{Int}$. If $x : \mathsf{Bool}$ instead, then $1+x$ just wouldn't be a well-formed term at all, and there would be no meaning in asking any further questions about the term. Indeed, $(1+x)\Xi\mathsf{Int}$ would itself be an ill-formed formula. A completely analogous situation happens in programming languages. If you have a Java program that's ill-typed, it doesn't make sense to ask how it would behave despite being ill-typed. The meaning of Java programs is simply not defined for ill-typed programs. You could even say ill-typed Java programs aren't actually Java programs at all.

The rules in the technical report more or less build in the subsumption rule that you could write as: if $t \in \text{Trm}_A$ and $A \sqsubseteq B$ then $t \in \text{Trm}_B$. Therefore, for every well-formed term $t$, $t \in \text{Trm}_\top$. In particular, for a predicate symbol $p(A)$, $p(t)$ is a well-formed formula for any $t\in\text{Trm}_B$ where $B\sqsubseteq A$, so as far as any formula is concerned, a term of type $B$ is just as good as a term of type $A$. The definition of semantics they give just outright states, using their notation, $D^B \subseteq D^A$ if $B\sqsubseteq A$. Completeness with respect to this notion of semantics requires the subsumption rule. As for $\Xi A$, there need to be rules or axioms describing it. Now, as a meta-logical statement, you could say: whenever $t \in \text{Trm}_A$, the theorem $t\Xi A$ is provable. An instance of this would be since $1+1 \in \text{Trm}_\mathsf{Int}$, $(1+1)\Xi\mathsf{Int}$ is provable. So this meta-theorem is saying, for every term $t$ such that $t \in \text{Trm}_A$, we can find a proof of $t\Xi A$. In contrast, within the logic we have the statement $\forall x:A.x\Xi A$ (or using the notation in the technical report: $\forall A\ x; x\Xi A$). This is a single theorem within the logic. In fact, $\forall x.x\Xi\top$ is true, but the meta-logical statement "everything is a well-formed term of type $\top$" definitely is not as not everything is a well-formed term or even anything like a term. Going by the technical report, I assume $\Xi A$ is related to the $\text{instance}_A$ function symbol which leads to $\forall \top\ x;(x\Xi A \iff \exists A\ y; y \doteq x)$ as the defining axiom for $\Xi A$. (I've tweaked it slightly as for their JFOL the axiom for $\text{instance}_A$ is restricted to "Objects" which is not the top type in their hierarchy. As far as I can tell, $\text{instance}_\mathsf{int}(3)$ is left unspecified if $\mathsf{int}$ is a primitive Java type i.e. $\mathsf{int}\not\sqsubseteq \mathsf{Object}$ where $3:\,\to\mathsf{int}$.)

There's a similar syntax versus semantics issue in your question about predicate symbols. A predicate symbol is not "a function to the set $\{\text{True}, \text{False}\}$". A predicate symbol is, as its name suggests, just a symbol, a piece of syntax. Classical first-order logic happens to have a sound and complete semantics where we can interpret formulas as picking out subsets of the Cartesian product of interpretations of the types of its domain which we can then identify with characteristic functions, but there is absolutely no need to do this. We can work entirely syntactically, and computer scientists tend to lean this way as programming itself is highly syntactic. It is also the case that this interpretation is not sound and complete for other logics. If you are dead set on working semantically, the domain of a predicate symbol $p(A, B)$, for example, is the Cartesian product $[\![A]\!]\times[\![B]\!] \subseteq [\![\top]\!]\times[\![\top]\!]$ where $[\![\_]\!]$ is the interpretation function that sends a type to a set. There is an interpretation function sending terms to elements of the appropriate set, which I'll also write $[\![\_]\!]$, such that $[\![t]\!]\in[\![A]\!]$ when $t \in \text{Trm}_A$. So the interpretation of the variable symbol $x : A$ will be in the domain of the interpretation of a predicate $p(A)$. (To be completely pedantic, we interpret terms, not variable symbols, and variable symbols only embed into terms; they aren't necessarily terms in and of themselves.) The term part of the interpretation is a set function $\text{Trm}_A \to [\![A]\!]$ for each type $A$. This function need not be surjective, which is to say there can be elements of $[\![A]\!]$ which don't correspond to any term. So, the interpretation of a type, i.e. $[\![A]\!]$ is an arbitrary set which must satisfy some rules. We can map terms into this set, but the elements are not (usually) terms themselves and there can be other elements. The interpretation of predicate and function symbols needs to correctly work with all elements of these sets, even ones that don't correspond to terms. Again, none of this interpretation stuff is at all necessary to work with or understand the logic. Indeed, computer implementations usually don't use this at all and operate purely syntactically. (Model checking does leverage semantics though.) It's certainly a rich field and it provides a different perspective to the logic, but it is not necessary.

Summarizing, $x : B$ is data provided which is used to define what a well-formed formula is. It is used to produce the meta-logical predicate $t\in\text{Trm}_A$ stating that a term $t$ is well formed and has type $A$ (similarly for formulas). $t\Xi A$ is a formula within the logic that can be formally proven or refuted with the rules of the logic. Semantically, $[\![\Xi A]\!] = [\![A]\!]\subseteq[\![\top]\!]$. In some ways $\Xi A$ does kind of internalize the typing judgement. We could eliminate all types except for $\top$ and instead of having for $p : A,B$, $p(t_1,t_2)$ where $t_1 \in \text{Trm}_A$ and $t_2 \in\text{Trm}_B$, we could say this is really an abbreviation for $t_1\Xi A \land t_2\Xi B \land p(t_1,t_2)$ where $p : \top,\top$ and $t_1, t_2 \in\text{Trm}_\top$. Nevertheless, for the purpose of semantics, the roles of $\Xi A$ and the typing judgement are different. The typing judgement specifies what the domains of the interpretation functions are while $\Xi A$ is just an element of one of those domains.

$\endgroup$
  • $\begingroup$ You have explained it beautifully. What I gather from reading your answer is that the predicate $\Xi A$ takes its input from $\mathrm{Trm}_\top$ and returns TRUE if the given input is from $\mathrm{Trm}_A$. Is that right? $\endgroup$ – Nanashi No Gombe May 31 '17 at 20:33
  • $\begingroup$ I have a few follow-up questions. When you say $1:int,$ it surely means $1\in VSym.$ Moreover, $1\in\mathrm{Trm}_{int}.$ This means $1+1\in\mathrm{Trm}_{int}$ but it may not be necessarily true that $1+1\in VSym.$ If a term is not a variable symbol, by the defn. of the typing function $\alpha,$ the claim $1+1:int$ does not make sense unless we redefine $\alpha$ such that it maps $\mathrm{Trm}_A\to A.$ Secondly, how do you know that if $t:A$ and $A \sqsubseteq B$ then $t:B$? All I can see is that given this premise, $(B)t: B$. Lastly, how would you ever prove $t \Xi A$ without interpretation? $\endgroup$ – Nanashi No Gombe May 31 '17 at 20:45
  • $\begingroup$ They use the colon notation for more than just variable symbols, so they would write $1:\to\mathsf{Int}$ indicating that $1$ is a constant symbol of type $\mathsf{Int}$. I extended $t:A$ to be $t\in\text{Trm}_A$ generally, but I've rewritten it to coincide with their notation more closely. The idea is indeed that given $\alpha$ providing types for the primitive function symbols/predicate symbols/variables, you can extend that to a typing for arbitrary terms/formulas. This is what they do in their definition of $\text{Trm}_A$. I've edited the answer to respond to the other questions. $\endgroup$ – Derek Elkins May 31 '17 at 23:36

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.