Primiero, information and knowledge, chapter 3, formal representation of the notion of information

category: reference

This entry is about a section of the text

This chapter 3 is the technical heart of the book. It gives an epistemic interpretation of CTT (constructive type theory) in terms of knowledge and information. This interpretation is explicated by considering CTT as a framework for the representation of knowledge processes with the operation of retrieving and extending knowledge. This formalization abstracts common processes in computer science. The interpretation given here is due to Giuseppe Primiero and is partially based on ideas of Borghuis, Kamarredine and Nederpelt.

Basic notions in this type theoretical framework are that of context (coinciding with the notion of context familiar to type theorists) and that of environment (which has been presented by Peer Martin-Löf 1991a who attributes this notion to Peter Landin) which is the logical translation of the notion of computer memory.

Terminological remark (predication)

In philosophical logic a typing judgement a:αa:\alpha is called predication of aa in α\alpha.

In this case ():α(-):\alpha is called the category of objects predicated in α\alpha.

We say the object α\alpha on the right of the colon is meaning referring.

Terminological remark (analyticity)

In philosophical logic a typing judgement a:αa:\alpha is called analytic with respect to some specific inference II if it occurs more than one times in II.


3.1 CTT as the general framework: informal description

3.1.1 Formalization of knowledge and information

Types are general concepts

The equivalence of types and concepts means that every judgement establishes the predication of a concept. A type is an element in the category of predication ():type(-) : type. A context in this theory is regarded as a carrier of meaning.

Proofs are justifications for judgements

Here the notion of information enters implicitly: Specific elements of proofs are regarded as carriers of information.

Contexts contain collections of assumptions for judgements

Assumptions are assertion conditions for judgements. The notion of information is related to the operations performed on the content of contexts.

3.1.2 Contexts: formal explanation

The calculus of contexts and environments

calculus of contexts and environments?

There are two specific types

context:typecontext : type
environment:typeenvironment : type

subject to the following rules:

Context formation rules

The rule

():context(\;) : context

is saying that contexts can be used as types and that we write contexts in brackets.

Γ:context αγ:type(Γ)(Γ,x:α):context\frac{\array{\Gamma : context\\ \alpha\gamma : type (\Gamma)}}{(\Gamma,x:\alpha) : context}

where γ:environment\gamma:environment, γ:Γ\gamma:\Gamma, and α:type\alpha: type. This rule declares the formation of a type α\alpha under a environment γ\gamma. It is an extension of a context in some environment.

Environment formation rules

The rule

():():context(\;):(\;): context

in the first bracket expects environments and in the second- expects contexts.


This rule can be derived from two rules of computation of environments whose genesis is conceptually crucial to this chapter:

Environment computation rule 1
Environment computation rule 2

To avoid the circularity arising in the formalization of contexts we need some inductive construction called updating. Contexts are hence built by successive updating of the elements in it:

Updating of contexts
Calculus of contexts
Updating of environments

3.2 Representation of knowledge and information

The notions of information and knowledge will be defined by the following structural aspects of CTT:

  1. Presuppositions, in the basic form these are type declarations.

  2. Assumptions, these are contained in contexts for dependent types and objects.

  3. Context extension

  4. Categorical judgements

It is important to notice that Presuppositions and Assumptions are thought of as different notions.

3.2.1 Presuppositions


A presupposition for a judgement a:αa:\alpha is a judgment which is needed for the judgement a:αa:\alpha to make sense.

For example a:αa:\alpha has as α:type\alpha:type as a presupposition. We write in this case <α:type>\lt\alpha:\type\gt to indicate that α:type\alpha:type is a presupposition (for some judgement).

Notice that we could call α:type\alpha:type a type declaration of the type α\alpha and a:αa:\alpha an instatiation of the type α\alpha.

3.2.2 Assumptions


The notion of assumption enters the definition of a dependent type. An assumption is the aspect on which a dependent type depends.

The aspect of a dependent type which depends (on some assumption) we could call knowable object.

3.2.3 Types and meaning declarations


We say the object α\alpha on the right of the colon in a:αa:\alpha is meaning referring.

Meaning is what is referred to aa by α\alpha.

3.2.4 Truths and the role of assumptions


By definition of CTT a judgement is true if it has a proof.

We refer to this fact by saying that (x:α)(x:\alpha) carries the information that [x/a]:type[x/a]:type is true.

3.2.5 Defining information

Recall that by definition types are general concepts.

Informational data

Every typing judgements in a context is (by definition) informational data.

For example type declarations, assumptions and derived judgements are informational data with respect to the specific contexts they occur in.

Informational state

A prefix (=initial segment) (x 1:a 1,,x n:a n)(x_1:a_1,\dots,x_n:a_n) of a context (x 1:a 1,,x n:a n,x n+1:a n+1,,x n+k:a n+k):=Γ(x_1:a_1,\dots,x_n:a_n,x_{n+1}:a_{n+1},\dots,x_{n+k}:a_{n+k}):=\Gamma we could call an informational state in Γ\Gamma.

Knowledge state

We could call the collection of all judgements in an informational state its (underlying) knowledge state.


A context Δ\Delta is a carrier of information. We could think of the class of all extensions (see below) {ΓΔ|Γ:context}\{\Gamma\leftarrow \Delta|\Gamma:context\} of the class of all information contained in Δ\Delta.

3.3 Contexts as constructive possible worlds

3.3.1 introducing orderings: Kripke models

3.4 The knowledge framework

3.4.1 Updating information, extending knowledge

Informational updating

An interpretation of (also called updating of …by or extension of…by)

Γ=x 1:α 1,,x n:α(x 1,,x n)\Gamma=x_1:\alpha_1,\dots,x_n:\alpha(x_1,\dots,x_n)

in (resp. by)

Δ=y 1:β 1,,y n:β(y 1,,y n)\Delta=y_1:\beta_1,\dots,y_n:\beta(y_1,\dots,y_n)

is defined by giving a sequence of definitions:

x 1=f 1(y 1,,y m):α 1 x n=f n(y 1,,y m):α n(f 1(y 1,,y m),,f n(y 1,,y n))\array{ x_1=f_1(y_1,\dots,y_m):\alpha_1 \\ \vdots \\ x_n=f_n(y_1,\dots,y_m):\alpha_n(f_1(y_1,\dots,y_m),\dots, f_n(y_1,\dots,y_n)) }
Extension of contexts

see also [Ranta1994] pp.145-147

An extension ΓΔ\Gamma\leftarrow \Delta of a context Γ\Gamma by a context Δ\Delta as defined above can be derived by the following basic cases:

(a) Addition of a type declaration (Introduction of a new context): i.e. Γ=(x 1:α 1,,x n:α n)\Gamma=(x_1:\alpha_1,\dots,x_n:\alpha_n) is extended to Δ=x 1:α 1,,x n:α n,<α n+1:type>)\Delta=x_1:\alpha_1,\dots,x_n:\alpha_n,\lt \alpha_{n+1}:type\gt)

(b) Addition of a new assumption: i.e. Γ=(x 1:α 1,,x n:α n)\Gamma=(x_1:\alpha_1,\dots,x_n:\alpha_n) is extended to Δ=x 1:α 1,,x n:α n,x n+1:α n+1)\Delta=x_1:\alpha_1,\dots,x_n:\alpha_n, x_{n+1}:\alpha_{n+1})

(c) variable substitution (addition of a definition): i.e. Γ=(x 1:α 1,,x n:α n)\Gamma=(x_1:\alpha_1,\dots,x_n:\alpha_n) is “extended” (the resulting expression may be shorter) to Δ=(Γ,x k=a:α k)\Delta=(\Gamma,x_k=a:\alpha_k)

3.4.2 The structure of knowledge


  • Borghuis, Kammarredine, Nederpelt, Formalizing Belief Revision in Type Theory, BibTex

  • Peer Martin-Löf, Contexts and environments, unpublished notes by P. Mäenpaä and A. Rata of a series of lectures given at Stockholm University

  • Aarne Ranta: type-theoretical grammar, 1994, Oxford University Press


Last revised on August 7, 2012 at 20:01:50. See the history of this page for a list of all contributions to it.