Spahn 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:\alpha$ is called predication of $a$ 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:\alpha$ is called analytic with respect to some specific inference $I$ if it occurs more than one times in $I$.

Contents

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$. 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 : type$
$environment : type$

subject to the following rules:

Context formation rules

The rule

$(\;) : context$

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

$\frac{\array{\Gamma : context\\ \alpha\gamma : type (\Gamma)}}{(\Gamma,x:\alpha) : context}$

where $\gamma:environment$, $\gamma:\Gamma$, and $\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$

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

$\frac{\gamma:\Gamma\;a:\alpha\gamma}{(\gamma,x=a):(\Gamma,x:\alpha)}$

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

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:

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

Presupposition

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

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

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

3.2.2 Assumptions

Assumption

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

Meaning

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

Meaning is what is referred to $a$ by $\alpha$.

3.2.4 Truths and the role of assumptions

Truth

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

We refer to this fact by saying that $(x:\alpha)$ carries the information that $[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,\dots,x_n:a_n)$ of a context $(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.

Commentary

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

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)

$\Gamma=x_1:\alpha_1,\dots,x_n:\alpha(x_1,\dots,x_n)$

in (resp. by)

$\Delta=y_1:\beta_1,\dots,y_n:\beta(y_1,\dots,y_n)$

is defined by giving a sequence of definitions:

$\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

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. $\Gamma=(x_1:\alpha_1,\dots,x_n:\alpha_n)$ is extended to $\Delta=x_1:\alpha_1,\dots,x_n:\alpha_n,\lt \alpha_{n+1}:type\gt)$

(b) Addition of a new assumption: i.e. $\Gamma=(x_1:\alpha_1,\dots,x_n:\alpha_n)$ is extended to $\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. $\Gamma=(x_1:\alpha_1,\dots,x_n:\alpha_n)$ is “extended” (the resulting expression may be shorter) to $\Delta=(\Gamma,x_k=a:\alpha_k)$

References

• 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

substitution

Revised on August 7, 2012 20:01:50 by Stephan Alexander Spahn? (79.227.185.225)