# Tag Info

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 ...
• 30.9k

### 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 ...
• 30.9k
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 ...
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.
• 8,233

### 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 ...
• 12.1k
Accepted

• 361
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 ...
• 162k

### "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 ...
• 72.6k
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 ...
• 2,727
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 ...
• 573
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 ...
• 278k

### "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} \...
• 278k
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$....
• 9,847

### "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 ...
• 310
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 ...
• 8,233
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 ...
• 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 ...
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 ...
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'...
• 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 ...
• 2,727

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