| |
1 |
- Zhaohui Luo
- Dept of Computer Science
- Royal Holloway, Univ of London
|
2 |
- Historical developments:
- Logical paradoxes
- Ramified type theory (predicativity, Russell/Poincare)
- Simple type theory (impredicative, Ramsay/Church)
- Modern type theories – basic concepts
- Curry-Howard principle of propositions-as-types
- eg, AàB for AÉB
- Dependent types
- eg, Px:A.B(x) for "x:A.B(x)
- eg, Vect(A,n) where n : Nat
- Inductive types (Nat, Sx:A.B, List(A), Tree(A), Ordinals, …)
|
3 |
- Modern type theories – systems
- Predicative type theory [Martin-Löf 73/84]
- (intuitionistic, first-order, predicative)
- Impredicative type theories:
- F/Fw [Girard 72] (2nd-order/higher-order propositional logic)
- CC [Coquand-Huet 88] (higher-order logic – HOL)
- ECC/UTT [Luo 90/94] (HOL with inductive types/universes)
- (intuitionistic, higher-order, impredicative)
|
4 |
- Two extreme positions
- Neo-platonism (eg, set-theoretic foundation: Gödel/Manddy)
- Revisionists (eg, intuitionism: Brouwer/Martin-Löf)
- A pragmatic/“neutral” position – “pluralism”
- Various maths based on different logical foundations
- “Mathematical pluralism”
|
5 |
- Consider the “combinations” of the following and their “negations”:
- (C) Classical logic
- (I) Impredicative definitions
- We would have
- (CI) Ordinary (classical, impredicative) math
- Classical set theory/simple type theory, HOL/Isabelle
- (C°I°) Predicative constructive math
- Martin-Löf’s TT, Agda/NuPRL
- (C°I) Impredicative constructive math
- CID/ECC/UTT, Coq/Lego/Plastic
- (CI°) Predicative classical math
- Weyl, Feferman, Simpson, …
- Uniform foundational framework for formalisation to support pluralism?
|
6 |
- Proof assistants based on TTs
- Computer systems for interactive theorem proving
- System examples
- Agda (Sweden/Japan) and NuPRL (USA), implementing Martin-Löf’s type theory
- Coq (France), Lego/Plastic (UK), implementing UTT/CID
- Application examples
- (Computer science, omitted)
- Formalisation of mathematics
- Fundamental Theorem of Algebra
- Four-colour Theorem
|
7 |
- Why – motivations
- Uniform foundation for a variety of maths? (mathematical pluralism)
- Set-theoretic reasoning in type theory?
- How – LTT, a type-theoretic framework
|
8 |
- Strong mechanisms for type-theoretic reasoning
- Eg, inductive reasoning for inductive types
- (Nat, Trees, language syntax, …)
- Set-theoretic reasoning in type theory?
- Types are NOT sets! (confusions likely!)
- There are non-inductive sets!
- “a : A” – judgemental, meta-level
- “s Î S” – propositional
- Lack of support to set-theoretic reasoning in current TTs
|
9 |
- How should set-theoretic reasoning be supported?
- Traditional (untyped) ZF set theory? (cf, Isabelle/ZF)
- Combining with type-theoretic reasoning?
- Two roles of (the usual notion of) sets:
- (i) domain/range of functions: f : AàB.
- (ii) separation/selection from a domain: { x : A | P(x) }
- Now, types for (i) and typed sets for (ii)!
|
10 |
- Type-theoretic framework LTT
- LTT = LF + Logic-enriched TTs + Typed Sets
- LF – Logical framework (cf, Edin LF, Martin-Löf’s LF, PAL+, …)Logic-enriched type theories [Aczel/Gambino02,06]
- Typed sets: sets with base types (see later)
- Alternatively, LTT = Logics + Types Logic Types
- Logics – specified in LF \ /
- Types – inductive types + types of sets \ /
LF
|
11 |
- Types and propositions:
- Type and El(A): kinds of types and objects of type A
- Eg, inductive types like N, Sx:A.B, List(A), Tree(A), …
- Eg, types of sets like Set(A)
- Prop and Prf(P): kinds of propositions and proofs of proposition P
- Eg, "x:A.P(x) : Prop, where A : Type and P : (A)Prop.
- Eg, DN[P,p] : Prf(P), if P : Prop and p : Prf(¬¬P).
- Induction rules
- Linking the world of logical propositions and that of types
- Enabling proofs about objects of types
|
12 |
- Formation and introduction
- N : Type
- 0 : N
- succ(n) : N, for n : N
- Elimination over types and computation:
- ElimT(C,c,f,n) : C(n), for C(n) : Type where n : N
- Plus computational rules for ElimT: eg,
- ElimT(C,c,f,0) = c
- ElimT(C,c,f,succ(n)) = f(n,ElimT(C,c,f,n))
- Induction over propositions:
- ElimP(P,c,f,n) : P(n), for P(n) : Prop where n : N
- Key to prove logical properties of natural numbers
|
13 |
- Typed sets
- Set(A) : Type for A : Type
- { x:A | P(x) } : Set(A)
- t Î { x:A | P(x) } means P(t)
- Impredicativity and predicativity
- Impredicative sets (LTTi)
- A can be any type (e.g., Set(B))
- P(x) can be any proposition
- eg, P(x) = $s:Set(N). sÎS & xÎs, for S : Set(Set(N))
- Predicative sets (LTTp)
- Universes of small types and small propositions
- A must be small (in particular, A is not Set(…))
- P(x) must be small (not allowing quantifications over sets)
|
14 |
- Case studies
- (Simple) Implementation of LTT in Plastic (Callaghan)
- Formalisation of Weyl’s predicative math (Adams & Luo)
- Analysis of security protocols
- Future work
- Comparative studies with other systems, examples including
- Embedding ACA0 in LTTp (proof to be checked)
- Compare LTTi with ZF
- Comparative studies in practical reasoning
- Eg, packages for set-theoretic reasoning in LTT (cf, Isabelle/ZF)
|
15 |
- Z. Luo. A type-theoretic framework for formal reasoning with different logical foundations. ASIAN’06, LNCS 4435. 2007.
- R. Adams and Z. Luo. Weyl's predicative classical mathematics as a logic-enriched type theory. TYPES’06, LNCS 4502. 2007.
- Available from http://www.cs.rhul.ac.uk/home/zhaohui/type.html
|
|
|
