7 votes
Accepted

Is iszero of the untyped lambda calculus sound and complete?

No, iszero does not have to test whether two functions are equal. It only has to detect a difference between them, i.e., extract enough information to tell whether ...
Andrej Bauer's user avatar
  • 28.3k
6 votes
Accepted

Program equivalence wherein the programs are known to always halt

As a counter-example to this, consider the Context-Free Equivalence problem: it's undecidable to determine, given two context free languages, whether they accept the same set. If your problem were ...
Joey Eremondi's user avatar
6 votes

Turing Machines and Logic

Since Turing machines have three options (accept, reject, not halt), you have a few options as to what class of languages correspond to Turing machines. The recursively enumerable sets aren't closed ...
TomKern's user avatar
  • 279
6 votes

Density of semantics in syntax

In terms of related work, Marek Zaionc and collaborators have been studying similar kinds of questions for some time. The following paper includes many results: René David, Katarzyna Grygiel, Jakub ...
Noam Zeilberger's user avatar
5 votes

Turing Machines and Logic

The paper Some Turing-Complete Extensions of First-Order Logic by Antti Kuusisto also provides some examples, where you enrich first-order logic with the ability to modify the input structure, and ...
Denis's user avatar
  • 8,598
5 votes

Density of semantics in syntax

Let's look at a simple example of a toy programming language with unary natural numbers and a "predecessor" operation. $$t ::= 0 \mid S~t \mid p~t$$ whose semantics is given by the following ...
gasche's user avatar
  • 2,040
4 votes

Program equivalence wherein the programs are known to always halt

Consider programs $e_1$, $e_2$ and numbers of time steps $t$. Let $f_i(t)$ be the output of $e_i$ after $t$ steps, and let $f_i(t)$ output a special message like "none" if there's no output yet. ...
Bjørn Kjos-Hanssen's user avatar
3 votes
Accepted

Is there an efficient algorithm to check for duplicator-invariant equivalence on symmetric interaction combinators?

This does not answer your main question but concerns the following point: I'm looking for an equivalence on interaction nets that implies lambda calculus read-back equivalence, but that also ...
Damiano Mazza's user avatar
3 votes

Is iszero of the untyped lambda calculus sound and complete?

The iszero function is sound, in the sense that it returns true only for functions which are $\beta\eta$ equal to the $\bf{zero}$...
cody's user avatar
  • 13.7k
2 votes
Accepted

Why are these two definitions of PLS equivalent?

In general, searching a neighborhood for a better solution and reporting the whole neighborhood are two different things. There are for example some exponential neighborhoods, that is, neighborhoods ...
Christian Komusiewicz's user avatar
1 vote

Turing Machines and Logic

There is a rich field known as descriptive complexity which studies the connection between computability/complexity and logic; I highly recommend checking out Immerman's book or the summary page on ...
Caleb Stanford's user avatar
1 vote
Accepted

Are the `ArrowApply` and `Monad` typeclasses equivalent?

The problem with your counterexample is that the type you presented is not a valid instance of ArrowApply as far as I can tell. You didn't present what the ...
Max New's user avatar
  • 1,653

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