18

Q1: There are many notions of program equivalence (trace equivalence, contextual equivalence, observational equivalence, bisimilarity) which may or may not take into account things such as time, resource usage, nondeterminism, termination. A lot of work has been done on finding usable notions of program equivalence. For example: Operationally-Based Theories ...


15

The other extreme is to say two programs are equivalent iff they compute the same function (or show the same observable behavior in similar environments). But these are not good: not all programs checking primality are the same. We can add a line of code with no effect on the result and we would still consider it the same program. This is not an extreme: ...


12

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


10

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


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

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


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


2

Q2: I think usual theoretical definitions don't really distinguish between algorithms and programs, but "algorithm" as commonly used is more like a class of programs. For me an algorithm is sort of like a program with some subroutines left not fully specified (i.e. their desired behavior is defined but not their implementation). For example, the Gaussian ...


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