Using Signatures in Type Theory to Represent Situations

Abstract

Signatures have been introduced to represent situations in formal semantics based on modern type theories. In this paper, we study the notion of signature in more details, presenting it formally and discussing its use in representations of situations. In particular, the new forms of signature entries, the subtyping entries and the manifest entries, are formally presented and studied. Besides being signature entries, these two forms of entries may be introduced to form contextual entries as well and this may have interesting implications in applications of the notion of context to, for example, belief contexts.

This work is partially supported by the research grants from Leverhulme, Royal Academy of Engineering and the CAS/SAFEA International Partnership Program for Creative Research Teams.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

Signatures are introduced to represent situations (or incomplete possible worlds) by the second author in [15], where it has been argued that, with the new forms of subtyping entries and manifest entries, signatures are very useful in representing situations in a formal semantics based on modern type theories (MTTs). In this paper, we shall study the notion of signature in a more formal and detailed way.

The notion of signature has been used in describing algebraic structures. Its use in type theory can be found in the Edinburgh Logical Framework [8]. There, signatures are used to describe constants (and their types) in a logical system. This is in contrast to contexts in type theory that describe variables (and their types) which can be abstracted by means of quantification or $\uplambda$-abstraction. We shall study the notion of signature in MTTs by extending the logical framework LF (Chapter 9 of [10]) with signatures to obtain the system LF$_\varSigma$, which can be used similarly as LF in specifying type theories such as Martin-Löf’s type theory [19] and UTT [10].

Signatures as proposed in [15] may contain two new forms of entries: subtyping entries and manifest entries. A subtyping entry $A<_\kappa B$ declares that A is a subtype of B via. coercion $\kappa$. This localises a coercive subtyping relationship as studied in the coercive subtyping framework [11, 17] that was developed for type theory based proof assistants. Subtyping has been proved useful in formal semantics and, specifically for MTT-semantics, it is crucial partly because CNs are interpreted as types rather than predicates (as in Montague semantics). It is very useful to introduce subtyping entries in signatures when they are used to represent situations. Also, we shall explain that the introduction of coherent subtyping entries to signatures preserves the nice properties of the original type theory.

The other new form of signature entries is that of manifest entries. These have the form $c \sim a : A$, which introduces the constant c and assumes that it behaves exactly like the object a of type A.¹ Formally, a manifest entry is just the abbreviation of an ordinary membership entry together with a subtyping entry. The latter enforces the abbreviation: $c \sim a : A$ abbreviates $c : \mathbf 1 _A(a)$, where $\mathbf 1 _A(a)$ is the inductive unit type, together with the subtyping entry $\mathbf 1 _A(a) <_{\xi _{A,a}}A$ with the coercion $\xi _{A,a}$ that maps the object of the unit type to a. Such an extension with manifest entries is sound: meta-theoretically, the extension preserves all of the nice properties of the original type theory. We shall make this clear in more detail in the paper.

Both subtyping and manifest entries can be considered as contextual entries for declaring variables. This makes contributions to the application of contexts. One such example can be found in Ranta’s treatment of belief contexts [23]. We show how to extend this notion of belief context with these new entries. We shall also point out that, if we introduce these to form contextual entries, we should allow the corresponding move to the right of the turnstile: by quantification and $\uplambda$-abstraction for manifest entries and by local coercions for subtyping entries. In particular, for subtyping entries, this requires the introduction of the new form of terms, $\mathbf{coercion~A<_c B}~\mathbf{in}~\mathbf{M}$, to express local coercions² and this may make the meta-theoretical study more sophisticated.

The notion of signature is formally introduced in Sect. 2, where we present the system LF$_\varSigma$ and give an example to illustrate its use in representations of situations. In Sect. 3, the subtyping and manifest entries in signatures are studied: they are shown to be useful in expressing situations and, with further meta-theoretic studies, the extensions with them can be shown to preserve the nice meta-theoretic properties. The potential of adding such new forms of entries as contextual entries is considered in Sect. 4, where we use belief contexts as an example to illustrate that this can be useful.

2 Signatures for Representing Situations

Situations, or incomplete possible worlds, are proposed by the second author to be representable by signatures in MTT-semantics, i.e., when modern type theories are used to give formal semantics [15].

The use of possible worlds in set theory has been a central mechanism within Montagovian approaches of formal semantics, especially, in dealing with intensional phenomena including, for example, belief intensionality among other things. However, the use of set-theoretical possible worlds has given rise to the well-known hyperintensional problem, with various paradoxes associated with it (e.g., the Paris Hilton paradox and the woodchuck-groundhog paradox) [22]. When intensional type theories are employed for formal semantics, types rather predicates over sets are used to interpret CNs and significantly different mechanisms are available in representing and dealing with such phenomena. Using signatures to represent situations is such a proposal.

We shall describe the notion of signature formally, compare it with that of context, and give a simple example of its use in representing situations. In this section. we shall only describe signatures with the traditional membership entries. Contexts with such traditional entries have been used by Ranta [23] and others [3, 6] to represent situations, where they do not consider the issue of difference between variables and constants. We consider signatures rather than contexts here. Note that signatures may contain other forms of entries which are studied in the next section Sect. 3.

2.1 Signatures in Type Theory: A Formal Presentation

Type theories can be specified in a logical framework such as Martin-Löf’s logical framework [19] or its typed version LF [10]. We shall extend LF with signatures to obtain LF$_\varSigma$.

Informally, a signature is a sequence of entries of several forms, one of which is the form of membership entries c : K, which is the traditional form of entries as occurred in contexts (we shall add two other forms of entries in the next section). If a signature has only membership entries, it is of the form $c_1: K_1, \ldots , c_n: K_n$.

LF is a dependent type theory whose types are called kinds in order to be distinguished from types in the object type theory. It has the kind Type of all types of the object type theory and dependent $\varPi$-kinds of the form $(x:K)K'$ (we omit their details here – see [10]). In LF, there are five forms of judgements:

• $\vdash \varGamma$ (or written as ‘$\varGamma \ valid$’), which asserts that $\varGamma$ is a valid context.

• $\varGamma \vdash K\ kind$, which asserts that K is a kind in $\varGamma$.

• $\varGamma \vdash k: K$, which asserts that k is an object of kind K in $\varGamma$.

• $\varGamma \vdash K_1=K_2$, which asserts that $K_1$ and $K_2$ are equal kinds in $\varGamma$.

• $\varGamma \vdash k_1=k_2: K$, which asserts that $k_1$ and $k_2$ are equal objects of kind K in $\varGamma$.

To extend LF with signatures, we amend each form of judgement with a signature $\varSigma$ and add another form of judgements saying that a signature is valid. In other words, LF$_\varSigma$ has the following six forms of judgements:

• $\varSigma \ valid$, which asserts that $\varSigma$ is a valid signature.

• $\vdash _\varSigma \varGamma$, which asserts that $\varGamma$ is a valid context under $\varSigma$.

• $\varGamma \vdash _\varSigma K\ kind$, which asserts that K is a kind in $\varGamma$ under $\varSigma$.

• $\varGamma \vdash _\varSigma k: K$, which asserts that k is an object of kind K in $\varGamma$ under $\varSigma$.

• $\varGamma \vdash _\varSigma K_1=K_2$, which asserts that $K_1$ and $K_2$ are equal kinds in $\varGamma$ under $\varSigma$.

• $\varGamma \vdash _\varSigma k_1=k_2: K$, which asserts that $k_1$ and $k_2$ are equal objects of kind K in $\varGamma$ under $\varSigma$.

All of the inference rules of LF (those in Figs. 9.1 and 9.2 of Chapter 9 of [10]) become inference rules of LF$_\varSigma$ after replacing $\vdash$ by $\vdash _\varSigma$ (and changing the judgement form ‘$\varGamma \ valid$’ to ‘$\vdash _\varSigma \varGamma$’). For instance, the following rule for $\uplambda$-abstraction³ in LF

$$\begin{aligned} \frac{\varGamma , x: K\vdash b: K'}{\varGamma \vdash [x:K]b : (x:K)K'} \end{aligned}$$

becomes, in LF$_\varSigma$,

$$\begin{aligned} \frac{\varGamma , x : K\vdash _\varSigma b: K'}{\varGamma \vdash _\varSigma [x:K]b : (x:K)K'} \end{aligned}$$

In addition, in LF$_\varSigma$, we have the rules in Fig. 1 for signatures (and contexts), concerning their validity and their roles of making basic assumptions, where $\langle \rangle$ is the empty sequence and $dom(p_1: K_1,\ \ldots \ p_n: K_n) = \{p_1, \ldots ,p_n\}$.

Fig. 1.

Rules for signatures/contexts in LF$_\varSigma$.

Note that the assumptions in a signature or in a context can be derived – this is characterised by the third rule and the last rule in Fig. 1, respectively.

Remark 1

The membership entry c : K in a signature declares that c is a constant of kind K. This is different from a contextual entry x : K that declares x to be a variable. Note that a variable can be abstracted by, for example, quantification or $\uplambda$-abstraction as exemplified by a rule like the one below, where Prop is the universe of logical propositions:

$$\begin{aligned} \frac{\varGamma ,\ x: K\vdash _\varSigma P: Prop}{\varGamma \vdash _\varSigma \forall x:K.P: Prop} \end{aligned}$$

However, constants in signatures can never be abstracted in this way – that is why they are called constants. Therefore, signatures can adequately be used to represent situations. Also, because the constants in signatures cannot be abstracted, it is easier meta-theoretically to add new forms of entries to signatures than to contexts (see later).

2.2 Use of Signatures to Represent Situations: A Simple Example

Signatures can adequately be used to represent situations, or incomplete possible worlds, in the MTT-semantics. This possibility can easily be understood whenever one realises that types represent collections of objects just like sets, although types are syntactic (or, better, proof-theoretic) entities different from sets in set theory. Intuitively, the similarity between types and sets is one of the crucial reasons that MTT-semantics can be viewed as model-theoretic, while the differences between types and sets and, especially that the former are proof-theoretically defined, are why MTT-semantics can be also viewed as proof-theoretic (see [15] for more details).

That signatures can be used to represent situations is the other facet that the MTT-semantics is model-theoretic. Here, we use an example given in [15] to illustrate how signatures can be used to represent situations.

Example 1

The example, taken from Chapter 10 of [24], is about an (imagined) situation in the Cavern Club at Liverpool in 1962 where the Beatles were rehearsing for a performance. This situation can be represented as follows.

• 1. The domain of the situation consists of several peoples including the Beatles (John, Paul, George and Ringo), their manager (Brian) and a fan (Bob). This can be represented be means of the following signature $\varSigma _1$:

  $$\begin{aligned} \varSigma _1\equiv & {} D: Type,\\&John: D,\ Paul: D,\ George: D,\ Ringo: D,\ Brian: D,\ Bob: D \end{aligned}$$

• 2. The assignment function assigns, for example, predicate symbols such as B and G to the propositional functions expressing ‘was a Beatle’ and ‘played guitar’, respectively. We can introduce the following in our signature to represent such an assignment function:

  $$\begin{aligned} \varSigma _2 \equiv \;&B: D\rightarrow Prop,\ b_J: B(John),\ \ldots ,\ b_B:\lnot B(Brian),\ b_{B}': \lnot B(Bob), \\&G: D\rightarrow Prop,\ g_J: G(John),\ \ldots , \ g_G: \lnot G(Ringo),\ \ldots \end{aligned}$$

The signature that represents the situation will be of the form $\varSigma \equiv \varSigma _1,\ \varSigma _2, \ldots , \varSigma _n$. We shall then have, for instance,

$$ \vdash _\varSigma G(John)\ \ true\ \ and \ \ \vdash _\varSigma \lnot B(Bob)\ \ true. $$

where G(John) and B(Bob) are the semantic interpretations of John played Guitar and Bob was a Beatle, respectively.

3 Subtyping and Manifest Entries in Signatures

In the last section, we introduced signatures with only traditional membership entries. In this section, we consider two other forms of entries – the subtyping entries and manifest entries: introducing them into signatures, discussing meta-theoretic implications and illustrating their uses in representing situations.

In earlier work, these forms of entries were considered contextual entries: contextual manifest entries were first studied in [12] and contextual subtyping entries (in so-called coercion contexts) in [14]. Here in this section, we consider them as entries in signatures, as proposed in [15]. For this reason, they are not only useful in representing situations, but are also simpler meta-theoretically, since they are introducing constants rather than variables and, as a consequence of the subtyping entries, one does not need to introduce corresponding terms for the purpose of making abstraction operations possible (see Sect. 4 for further discussion in this last respect).

3.1 Subtyping Entries and Their Uses

Coercive subtyping has been studied for subtyping and abbreviations in MTTs and the associated proof assistants [11, 17].⁴ Introducing subtyping entries (to either signatures or contexts) is to localise the coercive subtyping mechanism, which has been studied globally in earlier research.

Syntactically, the system LF$_\varSigma$ is extended with the judgement forms $\varGamma \vdash _\varSigma A<_\kappa B: Type$ (we shall often just write $A<_\kappa B$ even when A and B are types) and $\varGamma \vdash _\varSigma K<_\kappa K'$. A subtyping entry to signatures can be introduced by means of the first rule in Fig. 2, where (A)B is the kind of functional operations from A to B. The second rule in Fig. 2 expresses that the subtyping assumptions in a signature are derivable. Then the rules for coercive subtyping [17], albeit extended for judgements with signatures, are all applicable. For instance, if signature $\varSigma$ contains $A<_\kappa B$ and $B<_{\kappa '}C$, we can derive $A<_{\kappa '\circ \kappa }C$ under $\varSigma$.

It is worth pointing out that validity of a signature is not enough anymore when we consider subtyping entries in signatures. For signature $\varSigma$ to be legal, we need the subtyping assumptions in $\varSigma$ to be coherent in the sense that, informally, all coercions between any two types are equal, i.e., in some appropriate subsystem,⁵ if $\varGamma \vdash _\varSigma A<_\kappa B$ and $\varGamma \vdash _\varSigma A<_{\kappa '}B$, then $\varGamma \vdash _\varSigma \kappa = \kappa ': (A)B$.

It is then possible to show that the conservativity result in [17] can be carried over to the current setting⁶ and, in particular, if the original type theory is strongly normalising, so is the type theory extended with the subtyping entries. As a consequence, the extension with subtyping entries preserves logical consistency – a basic requirement for a type theory to be employed for formal semantics.

Introducing subtyping entries makes using type theory for formal semantics much more convenient. First of all, it is now possible for one to localise subtyping assumptions. In some specific situations, some special subtyping relations may reasonably be assumed, which may not be reasonable in general. For instance, only in a cafe or restaurant would it be reasonable to say

• (1) The ham-sandwich left without paying the bill.

In representing a situation in a cafe, we might reasonably assume the following subtyping entry:

$$\begin{aligned} Ham\text {-}sandwich < Human, \end{aligned}$$

which will then allow the sentence (1) to be semantically interpreted as intended. Such reference transfers are studied by Nunberg [20] among others.

Fig. 2.

Rules for subtyping entries in signatures.

3.2 Manifest Entries and Their Uses

A manifest entry is of the form

$$\begin{aligned} c\sim a&: A \end{aligned}$$

(2)

Informally, it assumes that c behaves exactly like a of type A. Alternatively, one can think that in any place that we could use an object of type A, we could use c which actually plays the role of a. Signatures can be extended with manifest entries:

$$\begin{aligned} {(*)} \quad \quad \quad \frac{\vdash _\varSigma A: Type\ \ \ \vdash _\varSigma a: A\ \ \ c\not \in dom(\varSigma )}{\varSigma ,\ c \sim a: A\ valid} \end{aligned}$$

where Type is the kind of all types (in the object type theory). In fact, such manifest entries can be introduced by means of special membership entries with the help of the coercive subtyping mechanism. We now proceed with its formal description.

Manifest entries can be regarded as abbreviations of special membership entries [12] with the help of the coercive subtyping mechanism [11, 17]. Formally, to add the above manifest entry (2) to a signature is to add the following two entries:

$$\begin{aligned} c:\mathbf 1 _A(a),\&\quad \mathbf 1 _A(a) <_{\xi _{A,a}}A \end{aligned}$$

(3)

where $\mathbf 1 _A(a)$ is the inductive unit type parameterised by A : Type and a : A, whose only object is $*_A(a)$, and $\xi _{A,a}(x) = a$ for every $x:\mathbf 1 _A(a)$. It is now easy to see that, if an expression has a hole that requires a term of type A, we can use c to fill that hole; then the whole expression is equal to that with the hole filled by a. For example, if the expression is $f(\_)$, then f(c) is equal to f(a).

Note that the subtyping entries involving $\xi$ form coherent signatures; in particular, if for two manifest entries $c\sim a: A$ and $d\sim b: B$ we have $\mathbf 1 _A(a)=\mathbf 1 _B(b)$ and $A=B$, then $\xi _{A,a} = \xi _{B,b}$, as coherence requires. Put in another way, if the subtyping entries in a signature are coherent, the signature is coherent since its manifest entries do not cause incoherence. Therefore, the extension with manifest entries in signatures preserves the nice properties of the original type theory such as strong normalisation and logical consistency.

Manifest entries can considerably reduce the complexity of representation, as the following example shows.

Example 2

With manifest entries, the situation in Example 1 can be represented as the following signature:

$$\begin{aligned} D \sim a_D: Type,\ B \sim a_B : D\rightarrow Prop,\ G \sim a_G : D\rightarrow Prop,\ \ldots \ \ldots \end{aligned}$$

(4)

where

• $a_D = \{John,\ Paul,\ George,\ Ringo,\ Brian,\ Bob\}$ is a finite type,

• $a_B: D\rightarrow Prop$, the predicate ‘was a Beatle’, is an inductively defined function such that $a_B(John) = a_B(Paul) = a_B(George) = a_B(Ringo) = True$ and $a_B(Brian)=a_B(Bob) = False$, and

• $a_G: D\rightarrow Prop$, the predicate ‘played guitar’, is an inductively defined function such that $a_G(John) = a_G(Paul) = a_G(George) = True$ and $a_G(Ringo) = a_G(Brian) = a_G(Bob) = False$.

In other words, $\varSigma _1$ in Example 1 is now expressed by the first entry of (4) and $\varSigma _2$ in Example 1 by the second and third entries of (4).

Manifest entries in signatures can be used to represent infinite situations such as those with infinite domains. With traditional membership entries (as in the traditional notion of context), we can only describe finite domains as we have done in Example 1. What if the domain D is infinite? This can be done by using a manifest entry – as in Example 2, we can assume that

$$\begin{aligned} D \sim Inf : Type, \end{aligned}$$

where Inf is some inductively defined type with infinitely many objects. Similarly, one can assume an infinite predicate over the domain, represented as:

$$\begin{aligned} P\sim \text {P-defn} : D\rightarrow Prop, \end{aligned}$$

where $\text {P-defn}$ is also inductively defined.

4 Subtyping and Manifest Entries in Contexts

The subtyping or manifest entries may be introduced in contexts as well. If this were done, it would further widen the uses of contexts in their applications. However, before introducing them and illustrating their uses be means of belief contexts, we should make clear that introducing contextual subtyping entries (and manifest entries, which have associated subtyping entries via $\xi$) complicates meta-theoretic studies. Until now, although the proposal of introducing contextual subtyping entries was already made in 2009 [13], the corresponding meta-theoretic studies have not been carried out in detail (for an initial study of this, see [16]) and further studies are needed.

Because a contextual entry should be able to be abstracted or moved to the right of turnstile (see Remark 1), it is necessary to introduce a new form of terms so that subtyping assumptions in a context can be represented as local coercions in terms. An term with a local coercion is of the form

$$\begin{aligned} \mathbf{coercion~A<_\kappa B}~\mathbf{in}~\mathbf{M}, \end{aligned}$$

which indicates that the scope in which subtyping $A<_\kappa B$ takes effects is term M – it does not take effect outside M. Local coercions are introduced the rules like the following:

$$\begin{aligned} \frac{\varGamma , A<_\kappa B\vdash _\varSigma k: K}{\varGamma \vdash _\varSigma (\mathbf{coercion~A<_\kappa B}~\mathbf{in}~\mathbf{k}) : (\mathbf{coercion~A<_\kappa B}~\mathbf{in}~\mathbf{K})} \end{aligned}$$

where the parentheses are there for readability, but not necessary.

Ranta [23] has proposed an account of belief intensionality in which he uses contexts to model agents’ beliefs as a sequence of membership entries.⁷ The idea is simple and it is based on the assumption that contexts can be seen as the equivalent type theoretic notion of a (partial) world as found in the traditional Montagovian semantics. Ranta introduces an agent’s belief context: for agent p, p’s belief context may be:

$$\begin{aligned} \varGamma _p = x_1: A_1,\dots ,x_n: A_n. \end{aligned}$$

A belief operator is then introduced: for a proposition A, $B_p(A)$ is true just in case that A is true in p’s belief context $\varGamma _p$, which is equivalent to saying that $\varPi x_1:A_1 ... \varPi x_n:A_n.A$ is true.⁸

In a case like (5):

• (5) John believes that all woodchucks are woodchucks $\Rightarrow$ John believes all woodchucks are groundhogs.

the sentences are evaluated against the agent’s belief context. If, from John’s belief context, one cannot derive the belief that ‘all woodchucks are groundhogs’,⁹ the unwanted entailment (5) does not go through. Similar considerations apply to the Hesperus/Phosphorus examples shown below:

• (6) The Ancients believed that Hesperus is Hesperus.

• (7) The Ancients believed that Hesperus is Phosphorus.

In a coarse grained system like Montague Semantics [7, 18], (7) follows from (6) [21, 22]. For the account as sketched here, this is not the case. If a logical equality between Hesperus and Phosphorus cannot be derived from the belief context of the Ancients, say $B_{A}$, then (7) does not follow from (6).

Similar considerations apply to the Paris-Hilton paradox which says that if Paris Hilton knows she is Paris Hilton, then she also knows either (a) that every nontrivial zero of the zeta-function has real part 1/2 (if this is indeed the case) or (b) knows that this is not the case (if it is not). Let us call this disjunction R. In effect, the Paris Hilton paradox says that if Paris Hilton knows that she is Paris Hilton, she also knows whether the Riemann hypothesis is true [21]. This is because in the set-theoretical semantics, necessary true propositions have the same meaning since they are functions from possible worlds to truth values. Both sentences, i.e. Paris Hilton knows that Paris Hilton is Paris Hilton and Paris Hilton knows that R, are analytically true, i.e. true in every world and as such have the same meaning, which means that one can be substituted for the other! In the above approach, this is not true and the analysis does not suffer from this problem.¹⁰

Remark 2

Another interesting note is that the above approach to belief contexts allows us to represent embedded beliefs. For example, the following sentence (8) can be expressed (9):

• (8) John believes that George believes that John is handsome.

• (9) $B_J(B_G(A))$, where A is the proposition expressing ‘John is handsome’.

It is interesting to note that, from the above, we cannot conclude that $B_J(A)$ (‘John believes that John is handsome’).

If we introduce subtyping entries and manifest entries into contexts, we would then be able to make the above mechanism for beliefs more powerful. Here are some examples:

• In one’s belief context, there can be subtyping entries like $Man<Human$ (or even unreasonably $Human<Man$).

• Infinite beliefs can be expressed by manifest entries. In particular, we can use inductive definitions to capture infinitely many entries by means of finitely many entries.

Formally, when contexts are extended with subtyping (and manifest) entries, the belief operator $B_p(P)$ can be defined as follows.

Definition 1

First, define $B_\varGamma$ for arbitrary context $\varGamma$ as follows.

• If $\varGamma = \langle \rangle$, then $B_\varGamma (P) = P$.

• If $\varGamma = x: A, \varGamma _0$, then $B_\varGamma (P) = \varPi x:A.\ B_{\varGamma _0}(P)$.

• If $\varGamma = A<_\kappa B, \varGamma _0$, then $B_\varGamma (P) = \mathbf{coercion~A<_\kappa B}~\mathbf{in}~\mathbf{B_{\varGamma _0}(P)}$.

Then, let p be an agent and P a $\varGamma _p$-proposition. Define the belief operator as

$$\begin{aligned} B_p(P) = B_{\varGamma _p}(P). \end{aligned}$$

Remark 3

In the above definition, we have not considered manifest entries because a manifest entry can be represented by an ordinary membership entry together with a subtyping entry and, therefore, the above definition covers manifest entries as well.