13

Comparing two programming languages is difficult is a difficult problem, and far from being solved. The key issue is that there are many different ways languages can be compared, and none of them is compelling. The most widely used approach, coming from logic, is to consider translations between the languages to be compared. The general idea is as ...


11

I refer you to Chapter 9 of the HoTT book. In particular, a category is defined in such a way that isomorphic objects are equal, see Definition 9.1.6. As Example 9.1.15 points out, there really isn't a reasonable notion of "skeletality" in HoTT. This is so because equality is so weak that it already means "isomorphic". Furthermore, Theorem 9.4.16 says ...


9

The problem you describe has definitely been considered (I remember discussing it in grad school, and at the time already it had been discussed long before then), though I can't point to any particular references in the literature. Possibly because it is linearly equivalent to uncolored graph isomorphism, as follows (this is true even for canonical forms). ...


8

The recognition problem is equivalent to the graph isomorphism (recognition) problem, and the invariant problem is equivalent to the graph isomorphism invariant problem. To reduce the current problem to graph isomorphism, given an m×n matrix A, let S be the set of integers which appear as an entry of A at least once. We construct a graph G(A) with m+mn+|S| ...


7

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 the given function represents a 0 or not. You could ask the same question about equality testing. It is possible to implement an equality test eq for numbers (exercise, but implement predecessor ...


6

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 decidable, we could use it to determine CFL equivalence, since it's always possible to turn a CFL into an always-halting Turing machine. So even for countably ...


6

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 Kozic, Christophe Raffalli, Guillaume Theyssier, Marek Zaionc. Asymptotically almost all λ-terms are strongly normalizing. Logical Methods in Computer Science,...


5

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 rewrite rules $$p~(S~t) \to t \qquad p~0 \to 0$$ with $$\mathsf{size}(0) = 1 \qquad \mathsf{size}(S~t) = 1 + \mathsf{size}(t) \qquad \mathsf{size}(p~t) = 1 + \...


4

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. Then $f_1$ and $f_2$ both always halt, but you can't decide if they always output the same - see Rice's Theorem.


3

I read your last comment in the Joshua's correct answer; if you need to transform EQ-GI to colored GI (i.e. you are in trouble with the colors assigned to the equivalence classes) you can use the following reduction: Suppose that the starting graphs are $G_1 = (V_1, E_1)$, $G_2 = (V_2, E_2)$ and there are $q$ equivalence classes; then you can add to each ...


3

The iszero function is sound, in the sense that it returns true only for functions which are $\beta\eta$ equal to the $\bf{zero}$ function. The iszero function is only complete modulo termination: there is no finite method to determine for an arbitrary f whether iszero f is going to return true, false or simply run forever. This is where undecidability rears ...


2

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 whose size grows exponentially in the input length $n$, that can be searched in polynomial time for a better solution, see for example A study of exponential ...


1

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 implementation of app but the only one I could come up with (where you use the input stream function once and then discard it) doesn't satisfy the 2nd and 3rd ArrowApply laws. What definition of app did ...


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