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

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

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

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

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

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

### 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}$...
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 ...
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 ...
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 ...

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