35

First, to reiterate one of cody's points, the Calculus of Inductive Constructions (which Coq's kernel is based on) is very different from the Calculus of Constructions. It is best thought of as starting at Martin-Löf type theory with universes, and then adding a sort Prop at the bottom of the type hierarchy. This is a very different beast than the ...


31

HoTT "suffers" from Gödel incompleteness, of course, since it has a computably enumerable language and rules of inference, and we can formalize arithmetic in it. The authors of the HoTT book were perfectly aware of its incompletness. (In fact, this is quite obvious, especially when half of the authors are logicians of some sort). But does incompleteness "...


22

I've often wanted to try and summarize each dimension of the $\lambda$-cube and what they represent, so I'll give this one a shot. But first, one should probably try to dis-entangle various issues. The Coq interactive theorem prover is based on an underlying type theory, sometimes lovingly called the calculus of inductive constructions with universes. You'...


21

If you look at Notes on Chapter 8 you will see what has already been formalized, and I think that's a lot. There are the Coq HoTT library and the Agda HoTT-Agda library which formalize large chunks of Homotopy Type Theory. To get things done in Coq we needed a special version of Coq that was patched just for the purposes of HoTT. However, Coq is moving in ...


12

As far as I understand, in Agda it is possible to represent all of that (i.e. all of Chapter 2 -- there is a library on github which does; AFAIK, the same is true of Coq). It is only when you get to later chapters that things get dicey. There are two obvious items: The circle. This is represented (in Agda) using a postulate, and so is not as nice as ...


10

Set theory is doing you some harm here and the sooner you liberate yourself from it the better it will be for your understanding of computer science. Forget the intersections and unions. People get this idea that $\forall$ and $\exists$ are like $\bigcap$ and $\bigcup$, which is the sort of thing the Polish school was doing a long time ago with Boolean ...


9

I think that the type system you want is elementary affine logic with fixpoints. A distinctive feature (actually, the distinctive feature) of light logics, including elementary linear/affine logic, is that types do not ensure termination: unlike usual logical system, cut-elimination follows from a structural property of proofs (namely, stratification), the ...


9

You can't do this using the traditional Church encoding for Bool: #Bool = ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool ... because you can't write a (useful) function of type: #Bool → * The reason why, as you noted, is that you can't pass in * as the first argument to #Bool, which in turn means that the True and False arguments may not be types. ...


9

If you want to include a fixpoint combinator in the language, you don't need to change anything to the syntax of types or the rules to type existing expressions. All it takes is adding one constant, a rule to type it and a rule to reduce expressions containing it: $$ \dfrac{}{\mathsf{fix} : (\tau \rightarrow \tau) \rightarrow \tau} \qquad \mathsf{fix} \, ...


9

First, note that nothing turns on the presence or absence of the empty type: if you have a nonlinear calculus with function types and unrestricted recursive types, then it is inconsistent. Indeed, your derivation works regardless of the type of the answer -- the very same term you have works for $\mu a.\; a \to X$ for any $X$. This is known as Curry's ...


9

It sounds like you want an overview of normalization arguments for type systems with positive datatypes. I'd recommend Nax Mendler's PhD dissertation: http://www.nuprl.org/documents/Mendler/InductiveDefinition.html. As the date suggests, this is pretty classic work. The basic intuition is that an ordinal $\lambda$ can be associated to any element of a ...


8

I don't want to make a statement about "all linear lambda calculi" since it's hard to make that precise, but for pure linear lambda-calculus the answer is yes. One way to enforce linearity in pure lambda calculus is by trying to type application and abstraction using the linear implication $A \multimap B$, $$ \frac{\Gamma \vdash t:A\multimap B\quad \Delta\...


8

I posted this to TYPES, but its probably worth copying here as well: In "The system F of variable types, fifteen years later", Girard remarks that there was no particular reason for the name F: However, in [3] it was shown that the obvious rules of conversion for this system, called F by chance, were converging. There may be another explanation in ...


8

Coq without Prop is not strong enough, because it's basically Martin-Löf type theory with universes. Coq with Prop is strong enough, because you can encode sets of normalizing terms via predicates $S : \mathrm{Term} \to \mathrm{Prop}$, and impredicative universal quantification lets you express arbitrary intersections.


8

I think there may be a little nuance that can be applied to the situation, where 2 different possible hats may be applied, and which both are valid views of type systems. View 1: Types are intrinsic In this view, it makes no sense to talk about a program/term independently of its type. In addition $\forall$s and $\exists$s are really "forall"s and ...


7

Spoiler: the types are isomorphic. First let me clarify what might be meant by "isomorphic". Say that two datatypes $S$ and $T$ are isomorphic if there are maps $f : S \to T$ and $g : T \to S$ such that $f(g(v)) = v$ for every value $v : T$ and $g(f(u)) = u$ for every value $u : U$. Let us fix a type $A$. We can then write your equations without the ...


7

There are plenty such typing systems. Most work is based on the linear/affine typing system introduced in (1) and generalised in (2). Here are the main works on this subject. In (3) the typing system ensures a precise match with PCF (int its call-by-name variant -- changing to call-by-value is easy). In (4) the typing system gives a precise interpretation ...


7

If you implement an evaluator for the terms of a language $A$ in a total system $B$, and you have furthermore proven that your evaluator is correct, that is for every $t$ well-typed in $A$, $$\mathrm{eval}(t) \simeq_A t $$ where $\simeq_A$ is the equality in $A$, then you have only shown that $\simeq_A$ is decidable. If furthermore $\simeq_A$ naturally ...


7

Since the CoC has dependent types and system $F$ does not, I'll assume you mean a function whose types is in system $F$, but whose definition can only be written in CoC. Luckily in this case we can restrict to system $F_\omega$, which can express the same non-dependent functions as CoC, by some erasure argument. In general, a rule of thumb to construct such ...


6

Cook-Reckhow propositional proof systems are nonunifrom. E.g. the computational complexity counterpart to the class of polynomial-size $\mathsf{Extended Frege}$ proofs is the nonuniform complexity class $\mathsf{P/poly}$. We have to look at their uniform counterparts: E.g. the proof complexity counterpart for $\mathsf{P}$ are bounded arithmetic theories ...


6

Two remarks first: I have used the "randomly generate terms and check that they are well-typed" approach (you mention that "untyped" terms are generated, you can also randomly generate terms in a Church-style grammar with explicit type annotations) and it worked very well in practice, it revealed all the bugs there was to find on this particular part of the ...


6

Part of the problem is we cannot say that we have a checker for categorical judgments, because these often reduce to hypothetical judgments. For instance, the categorical judgment $M\in A\to B$ reduces to a hypothetico-general judgment. In practice, the way that you implement this kind of type theory is by formalizing rules for hypothetico-general equality &...


6

One approach to such questions is via encodings. Say you have a language $L_1$ and a language $L_2$ and you want to show that they are somehow "the same", you can do this by finding an encoding $$ \newcommand{\SEMBTYPE}[1]{\ulcorner #1 \urcorner} \newcommand{\SEMB}[1]{\lbrack\!\lbrack #1 \rbrack\!\rbrack} \SEMB{\cdot} : L_1 \rightarrow L_2 $$ ...


6

The relationship that you're looking for is indeed well-defined, but IMO it's not quite the right thing to look at. For example: Type checking for terms in the simply-typed lambda calculus is linear time, but normalizing terms in the STLC exceeds any fixed tower of exponentials (i.e., $O(2^{2^{2^{\ldots n}}})$. Type checking for System F is linear time, but ...


6

One solution is indeed to restrict to substituting with synthesizing expressions. You can only hope to replace variables with terms of the same mode (i.e. inferrable terms), anything else just won't fit. It is not that restrictive in the sense that usually a checkable term together with a type annotation gives you an inferrable term. This embedding is ...


6

The key observation is that whether the substitution theorem holds, depends on the definition of substitution. For the usual definition of substitution of terms for variables, the substitution theorem is only true for substituting synthesizing terms for variables. Indeed, if you introduce separate grammatical classes for synthesizing and checking terms, ...


6

Another good source for going beyond strictly positive types is the PhD thesis of Ralph Matthes: http://d-nb.info/956895891 He discusses extensions of System F with (strictly) positive types in chapter 3 and proves many strong normalisation results in chapter 9. There are a few interesting ideas discussed in chapter 3. We can add least fixed points for any ...


6

I'll first point you to Types for the Scott Numerals by Plotkin, Cardelli and Abadi, where they show how to encode Scott numerals in plain old system F. This at least shows that you can write the "natural" recursion principles on Scott numerals, and because they correspond to recursors in this encoding, they are guaranteed to terminate. However, if you want ...


6

The standard well-formed-related predicate can be relatively easily extended to handle untyped PHOAS. The main subtlety is how to handle reduction at the type level. Here's a start of a two-place relation for well-typed in Coq: Require Import Coq.Lists.List. Reserved Infix "@" (left associativity, at level 11). Local Open Scope list_scope. Inductive expr ...


6

The discussion in the section surrounding that paragraph in Pierce's book explains why this is so. In particular, consider the definition of "type system" given on the page before: A type system is a tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute. ...


Only top voted, non community-wiki answers of a minimum length are eligible