Share Your Experience: Take the 2024 Developer Survey

# Tag Info

### Can a total programming language be Turing-complete?

I'm pretty sure McBride isn't claiming that a total programming language can be Turing complete, just that it's a useless distinction in practice. You can take any program in a partial language and ...
• 2,157

### Can a total programming language be Turing-complete?

A rhetorical question to keep in mind: would anyone take you seriously if you said ZFC is "not Turing complete" and therefore insufficient to express the algorithms that we write in ...
• 2,697
Accepted

### Does co-inductive and co-recursive types also have their recursors?

To understand coinduction, it helps to understand the categorical presentation of induction (since, as far as I know, coinduction comes from dualizing it there). The idea behind induction is that we ...
• 2,697

### How to write a coterminating, effectful program?

In these sorts of cases, one idiomatic way is to run it with gas, and to create one non-total gas value to let you finish the program. Yes, perhaps Idris should offer a combinator for IO that allows ...
• 326
Accepted

### Proving with co-induction principles

What likely makes it confusing is that you are doing very different things in inductive versus coinductive cases. This is somewhat alluded to by Chlipala's reference to "infinite proofs"1. (Another ...
• 12.1k

### Can a total programming language be Turing-complete?

I'm inclined to disagree with McBride here, for the simple reason that while you can express program semantics totally via coinduction, it is not enough to solve the halting problem for the object ...
Accepted

### When can the coinduction hypothesis be used?

First, let me recall least and greatest fixed points for $\subseteq$. We are working relative to some set $U$, the universe. In the case of (co)inductive definitions, $U$ is the set of all terms. A ...
• 2,254

### Coinduction in mathematical analysis?

The signed digit representation of Real Numbers seems like an efficient approach for: Defining the arithmetic operations and proving their algebraic properties. This was done already in a Master's ...
• 479
Accepted

### Bisimulations: Proof that the following LTS are not bisimilar

The left diagram has a b and the right diagram has a c. Thus, the pair $(2,4')$ does not satisfy the conditions required to be a bisimulation. In particular, the book is correct that those two ...
• 161k
1 vote

### "Largest set" in coinductive definitions

I think the precise definition of a final coalgebra might help. Fix a set of symbols $\Sigma$. For any set $X$ define $F(X) = \Sigma \times X$, and for any $f : X \to Y$ let $F(f) : F(X) \to F(Y)$ be ...
• 30.8k
1 vote

### "Largest set" in coinductive definitions

Here is a tentative self-answer. I think it must just be that there is an additional requirement that wasn't mentioned in the tutorials I read, namely that one of the destructors must apply to each ...
• 976
1 vote

### Definition of M-type in type theory

As far as I can tell, these are the rules: $$\frac{A:Type\quad x:A⊦B:Type}{(M x:A)B(x):Type}-\text{M-Formation}$$ \frac{C:Type\quad t: C\rightarrow \Sigma(a: A)(B[a / a]\rightarrow C)\quad c:C}{...
• 351

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