summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/Logics/CTT.tex

changeset 9695 | ec7d7f877712 |

parent 7159 | b009afd1ace5 |

child 12679 | 8ed660138f83 |

--- a/doc-src/Logics/CTT.tex Mon Aug 28 13:50:24 2000 +0200 +++ b/doc-src/Logics/CTT.tex Mon Aug 28 13:52:38 2000 +0200 @@ -40,16 +40,16 @@ Assumptions can use all the judgement forms, for instance to express that $B$ is a family of types over~$A$: \[ \Forall x . x\in A \Imp B(x)\;{\rm type} \] -To justify the {\CTT} formulation it is probably best to appeal directly -to the semantic explanations of the rules~\cite{martinlof84}, rather than -to the rules themselves. The order of assumptions no longer matters, -unlike in standard Type Theory. Contexts, which are typical of many modern -type theories, are difficult to represent in Isabelle. In particular, it -is difficult to enforce that all the variables in a context are distinct. -\index{assumptions!in {\CTT}} +To justify the CTT formulation it is probably best to appeal directly to the +semantic explanations of the rules~\cite{martinlof84}, rather than to the +rules themselves. The order of assumptions no longer matters, unlike in +standard Type Theory. Contexts, which are typical of many modern type +theories, are difficult to represent in Isabelle. In particular, it is +difficult to enforce that all the variables in a context are distinct. +\index{assumptions!in CTT} -The theory does not use polymorphism. Terms in {\CTT} have type~\tydx{i}, the -type of individuals. Types in {\CTT} have type~\tydx{t}. +The theory does not use polymorphism. Terms in CTT have type~\tydx{i}, the +type of individuals. Types in CTT have type~\tydx{t}. \begin{figure} \tabcolsep=1em %wider spacing in tables \begin{center} @@ -81,29 +81,29 @@ \cdx{tt} & $i$ & constructor \end{tabular} \end{center} -\caption{The constants of {\CTT}} \label{ctt-constants} +\caption{The constants of CTT} \label{ctt-constants} \end{figure} -{\CTT} supports all of Type Theory apart from list types, well-ordering -types, and universes. Universes could be introduced {\em\`a la Tarski}, -adding new constants as names for types. The formulation {\em\`a la - Russell}, where types denote themselves, is only possible if we identify -the meta-types~{\tt i} and~{\tt t}. Most published formulations of -well-ordering types have difficulties involving extensionality of -functions; I suggest that you use some other method for defining recursive -types. List types are easy to introduce by declaring new rules. +CTT supports all of Type Theory apart from list types, well-ordering types, +and universes. Universes could be introduced {\em\`a la Tarski}, adding new +constants as names for types. The formulation {\em\`a la Russell}, where +types denote themselves, is only possible if we identify the meta-types~{\tt + i} and~{\tt t}. Most published formulations of well-ordering types have +difficulties involving extensionality of functions; I suggest that you use +some other method for defining recursive types. List types are easy to +introduce by declaring new rules. -{\CTT} uses the 1982 version of Type Theory, with extensional equality. -The computation $a=b\in A$ and the equality $c\in Eq(A,a,b)$ are -interchangeable. Its rewriting tactics prove theorems of the form $a=b\in -A$. It could be modified to have intensional equality, but rewriting -tactics would have to prove theorems of the form $c\in Eq(A,a,b)$ and the -computation rules might require a separate simplifier. +CTT uses the 1982 version of Type Theory, with extensional equality. The +computation $a=b\in A$ and the equality $c\in Eq(A,a,b)$ are interchangeable. +Its rewriting tactics prove theorems of the form $a=b\in A$. It could be +modified to have intensional equality, but rewriting tactics would have to +prove theorems of the form $c\in Eq(A,a,b)$ and the computation rules might +require a separate simplifier. \begin{figure} \tabcolsep=1em %wider spacing in tables -\index{lambda abs@$\lambda$-abstractions!in \CTT} +\index{lambda abs@$\lambda$-abstractions!in CTT} \begin{center} \begin{tabular}{llrrr} \it symbol &\it name &\it meta-type & \it priority & \it description \\ @@ -113,7 +113,7 @@ \subcaption{Binders} \begin{center} -\index{*"` symbol}\index{function applications!in \CTT} +\index{*"` symbol}\index{function applications!in CTT} \index{*"+ symbol} \begin{tabular}{rrrr} \it symbol & \it meta-type & \it priority & \it description \\ @@ -160,7 +160,7 @@ \] \end{center} \subcaption{Grammar} -\caption{Syntax of {\CTT}} \label{ctt-syntax} +\caption{Syntax of CTT} \label{ctt-syntax} \end{figure} %%%%\section{Generic Packages} typedsimp.ML???????????????? @@ -168,16 +168,16 @@ \section{Syntax} The constants are shown in Fig.\ts\ref{ctt-constants}. The infixes include -the function application operator (sometimes called `apply'), and the -2-place type operators. Note that meta-level abstraction and application, -$\lambda x.b$ and $f(a)$, differ from object-level abstraction and -application, \hbox{\tt lam $x$. $b$} and $b{\tt`}a$. A {\CTT} -function~$f$ is simply an individual as far as Isabelle is concerned: its -Isabelle type is~$i$, not say $i\To i$. +the function application operator (sometimes called `apply'), and the 2-place +type operators. Note that meta-level abstraction and application, $\lambda +x.b$ and $f(a)$, differ from object-level abstraction and application, +\hbox{\tt lam $x$. $b$} and $b{\tt`}a$. A CTT function~$f$ is simply an +individual as far as Isabelle is concerned: its Isabelle type is~$i$, not say +$i\To i$. -The notation for~{\CTT} (Fig.\ts\ref{ctt-syntax}) is based on that of -Nordstr\"om et al.~\cite{nordstrom90}. The empty type is called $F$ and -the one-element type is $T$; other finite types are built as $T+T+T$, etc. +The notation for~CTT (Fig.\ts\ref{ctt-syntax}) is based on that of Nordstr\"om +et al.~\cite{nordstrom90}. The empty type is called $F$ and the one-element +type is $T$; other finite types are built as $T+T+T$, etc. \index{*SUM symbol}\index{*PROD symbol} Quantification is expressed by sums $\sum@{x\in A}B[x]$ and @@ -387,7 +387,7 @@ |] ==> snd(p) : B(fst(p)) \end{ttbox} -\caption{Derived rules for {\CTT}} \label{ctt-derived} +\caption{Derived rules for CTT} \label{ctt-derived} \end{figure} @@ -470,7 +470,7 @@ \section{Rule lists} The Type Theory tactics provide rewriting, type inference, and logical reasoning. Many proof procedures work by repeatedly resolving certain Type -Theory rules against a proof state. {\CTT} defines lists --- each with +Theory rules against a proof state. CTT defines lists --- each with type \hbox{\tt thm list} --- of related rules. \begin{ttdescription} @@ -514,14 +514,14 @@ equal_tac : thm list -> tactic intr_tac : thm list -> tactic \end{ttbox} -Blind application of {\CTT} rules seldom leads to a proof. The elimination +Blind application of CTT rules seldom leads to a proof. The elimination rules, especially, create subgoals containing new unknowns. These subgoals unify with anything, creating a huge search space. The standard tactic -\ttindex{filt_resolve_tac} +\ttindex{filt_resolve_tac} (see \iflabelundefined{filt_resolve_tac}{the {\em Reference Manual\/}}% {\S\ref{filt_resolve_tac}}) % -fails for goals that are too flexible; so does the {\CTT} tactic {\tt +fails for goals that are too flexible; so does the CTT tactic {\tt test_assume_tac}. Used with the tactical \ttindex{REPEAT_FIRST} they achieve a simple kind of subgoal reordering: the less flexible subgoals are attempted first. Do some single step proofs, or study the examples below, @@ -563,8 +563,8 @@ CTT} equality rules and the built-in rewriting functor {\tt TSimpFun}.% \footnote{This should not be confused with Isabelle's main simplifier; {\tt - TSimpFun} is only useful for {\CTT} and similar logics with type - inference rules. At present it is undocumented.} + TSimpFun} is only useful for CTT and similar logics with type inference + rules. At present it is undocumented.} % The rewrites include the computation rules and other equations. The long versions of the other rules permit rewriting of subterms and subtypes. @@ -583,11 +583,11 @@ \section{Tactics for logical reasoning} -Interpreting propositions as types lets {\CTT} express statements of -intuitionistic logic. However, Constructive Type Theory is not just -another syntax for first-order logic. There are fundamental differences. +Interpreting propositions as types lets CTT express statements of +intuitionistic logic. However, Constructive Type Theory is not just another +syntax for first-order logic. There are fundamental differences. -\index{assumptions!in {\CTT}} +\index{assumptions!in CTT} Can assumptions be deleted after use? Not every occurrence of a type represents a proposition, and Type Theory assumptions declare variables. In first-order logic, $\disj$-elimination with the assumption $P\disj Q$ @@ -598,7 +598,7 @@ refer to $z$ may render the subgoal unprovable: arguably, meaningless. -Isabelle provides several tactics for predicate calculus reasoning in \CTT: +Isabelle provides several tactics for predicate calculus reasoning in CTT: \begin{ttbox} mp_tac : int -> tactic add_mp_tac : int -> tactic @@ -728,7 +728,7 @@ \section{The examples directory} -This directory contains examples and experimental proofs in {\CTT}. +This directory contains examples and experimental proofs in CTT. \begin{ttdescription} \item[CTT/ex/typechk.ML] contains simple examples of type-checking and type deduction.