Skip to main content
Share Your Experience: Take the 2024 Developer Survey
7 votes

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 ...
benrg's user avatar
  • 2,157
5 votes

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 ...
Dan Doel's user avatar
  • 2,697
4 votes
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 ...
Dan Doel's user avatar
  • 2,697
4 votes

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 ...
Jason Carr's user avatar
3 votes
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 ...
Derek Elkins left SE's user avatar
3 votes

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 ...
Sebastian Graf's user avatar
3 votes
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 ...
kne's user avatar
  • 2,254
2 votes

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 ...
wlad's user avatar
  • 479
2 votes
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 ...
D.W.'s user avatar
  • 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 ...
Andrej Bauer's user avatar
  • 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 ...
N. Virgo's user avatar
  • 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}{...
Andrew Cann's user avatar

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