# Tag Info

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 ...
• 29.2k
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 ...
• 2,942

### 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 ...
• 489

### 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 ...
• 4,561

### 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 ...
• 8,903

### 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 ...
• 2,040

### 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. ...
• 4,485

### 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}$...
• 13.9k
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 ...
• 5,493