Showing changes from revision #6 to #7:
Added | Removed | Changed
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.
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 . A context in this theory is regarded as a carrier of meaning.
Here the notion of information enters implicitly: Specific elements of proofs are regarded as carriers of information.
Assumptions are assertion condition conditions for judgements. The notion of information is related to the operations performed on the content of contexts.
There are two specific types
subject to the following rules:
saying that contexts can be used as types and that we write contexts in brackets.
where , , and . This rule declares the formation of a type under a environment . It is an extension of a context in some environment.
where the first bracket expects environments and the second- expects contexts.
This rule can be derived from two rules of computation of environments whose genesis is conceptually crucial to this chapter:
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:
The notions of information and knowledge will be defined by the following structural aspects of CTT:
Presuppositions, in the basic form these are type declarations.
Assumptions, these are contained in contexts for dependent types and objects.
Context extension
Categorical judgements
It is important to notice that Presuppositions and Assumptions are thought of as different notions.
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