Skip to main content
18 votes
Accepted

What is induction-induction?

Supplemental 2016-10-03: I mixed up induction-induction and induction-recursion (not the first time I did that!). My apologies for the mess. I updated the answer to cover both. I find the ...
Andrej Bauer's user avatar
  • 30.9k
10 votes

In Agda's GADT, are "parameterized" and "indexed" different semantically?

The following explanation lacks mathematicial precision but should explain what is going on. A GADT is a special case of a recursive type. A recursive type $T$ is a solution of a type equation of the ...
Andrej Bauer's user avatar
  • 30.9k
9 votes
Accepted

In Coq, what does it mean to have an inductive type where the right-hand side of ":" is Prop?

Inductive types are similar to Haskell's data, but they are more general. An inductive definition in Set describes a way to ...
Gilles 'SO- stop being evil''s user avatar
8 votes
Accepted

How to derive dependently typed eliminators?

The canonical reference for this is Peter Dybjer, Inductive Families, which gives a pretty comprehensive treatment of inductive families based on eliminators.
cody's user avatar
  • 8,233
8 votes

Can properties such as memory usage of a function be expressed in a dependently typed language?

Yes, it can. While conceptually it's not that difficult, it hasn't been studied all that much. One aspect of the field is cost semantics such as the research done by Guy Blelloch. In the vein of ...
Derek Elkins left SE's user avatar
7 votes
Accepted

Example of inductive sets that are neither least nor greatest fixed point

Here's a non-trivial example: Suppose we want to define inductively a subset of reals, so we work on the complete lattice $\mathcal{P}(\mathbb{R})$ ordered by inclusion. Then, consider the rules $$ \...
chi's user avatar
  • 14.6k
6 votes

How to derive dependently typed eliminators?

You might find some of our recent papers on this useful, as we derive eliminators for lambda-encoded datatypes. For example, see this one for generic derivation of eliminators, and this one for the ...
Aaron Stump's user avatar
6 votes

Example of inductive sets that are neither least nor greatest fixed point

Any set is a fixed point of the empty set of rules or of the trivial rule $x\in X\Rightarrow x\in X$.
David Richerby's user avatar
4 votes
Accepted

In Agda's GADT, are "parameterized" and "indexed" different semantically?

Yes and no. The obvious difference is that indexed types are able to vary in the result type of each constructor. So you can do: data T : ℕ → Set where t : T 5 ...
Dan Doel's user avatar
  • 2,727
4 votes

How to define the natural numbers as a W-type?

The formation and introduction rules for W-types, as given on n-cat lab, are: $$\frac{A:Type\quad x:A⊦B:Type}{(W x:A)B(x):Type}-\text{Formation}$$ $$\frac{a:A\quad t:B(a)\rightarrow W}{sup(a,t):W}-\...
Andrew Cann's user avatar
4 votes
Accepted

Prefix encoding of algebraic data types

A code is prefix-free if there does not exist any distinct two values v, w such that ...
D.W.'s user avatar
  • 162k
4 votes

"Smallest set" term in the trees set definition

The set of unranked $Σ$-trees, denoted by $T$, is the smallest set of strings over $Σ$ and the parenthesis symbols ‘)’ and ‘(’ such that for each $a∈Σ$ and $w∈T^∗$, $a(w)$ is in $T$. What we have ...
Raphael's user avatar
  • 72.6k
4 votes
Accepted

Greatest fixpoint of the type of lists

The greatest fixed point cannot contain only the infinite lists, because it must contain all the elements of the least fixed point (and every other fixed point). Another way to see this is that just ...
Dan Doel's user avatar
  • 2,727
3 votes
Accepted

Finite list induction principle and the tail eliminator

I am totally lost on how to approach this problem since the eliminator seems to be able to provide just function defined on the whole family List′A(n) and not on the sub-family List′A(s(n)). The ...
gallais's user avatar
  • 573
3 votes
Accepted

What kinds of problems are modeled by a recursive definition of a set of strings?

The definition you quote is a formal definition of strings which is particularly conducive to induction. There are many other ways to define strings, for example as sequences of letters, or more ...
Yuval Filmus's user avatar
2 votes

"Smallest set" term in the trees set definition

You have to prove that $a)($ doesn't belong to $T$. You can start with constructing $T$, as follows. Let $T_0 = \emptyset$, and for $n \in \mathbb{N}$, define $$ T_{n+1} = \bigcup_{a \in \Sigma} \...
Yuval Filmus's user avatar
2 votes
Accepted

"Smallest set" term in the trees set definition

I think that is trivial according to the rule of how the strings are formed: $a(w)$. But if you need a formal proof then you could prove it as following using induction on the length of strings in $T$....
fade2black's user avatar
  • 9,847
2 votes

"Smallest set" term in the trees set definition

This use of the phrase "smallest set", or "smallest set with respect to inclusion" is generally taken to be synonymous with "the intersection of all sets satisfying this criterion" (as long as ...
Eric Towers's user avatar
2 votes
Accepted

Is mutual inductive type definition essential in coq core language?

It is always possible, as you noted, to translate a mutual inductive family into a non-mutual family, in much the same way as you described. A couple of difficulties though: If your mutual inductives ...
cody's user avatar
  • 8,233
2 votes
Accepted

Restrictions needed on ADT for totality

The constraint covariant type recursion (type constructor should not appear in negative position in a constructor argument) excludes this ...
chi's user avatar
  • 14.6k
1 vote
Accepted

Datatypes as initial algebras

An empty product is the same thing as a terminal object by definition of the product: it's an object $1$ such that for every object $A$, there is a unique morphism $1_A : A \rightarrow 1$. ($1$ is a ...
Gilles 'SO- stop being evil''s user avatar
1 vote

Finite list induction principle and the tail eliminator

What follows is just a little modification of the idea proposed in the accepted answer, nevertheless I think it can be of interest to other readers. Here's a way to build tail We can consider the ...
Giorgio Mossa's user avatar
1 vote

"Smallest set" term in the trees set definition

There are sets $T$ that satisfy the condition given (for each $a \in \Sigma$ and $w \in T^*$, $a(w) \in T$) which do contain badly-structured trees like $a)($; however, there is also a set that doesn'...
chridd's user avatar
  • 11
1 vote

Is it possible that the universe of types could be closed?

I'm uncertain what you're referring to exactly, but I can remark on a few things. The first is that the usual problem with W-types is that encoding inductive types with them does not necessarily give ...
Dan Doel's user avatar
  • 2,727

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