Naming conventions: Enumerability vs semi-decidability vs recognisability

[yforster]

Regarding the naming definition we started in #41, I did some (limited) research what standard resources call "recursively enumerable". (My opinion then follows below)

Rogers:

Definition A is recursively enumerable if either A = 0 or there exists a recursive f such that A = range f.

Wikipedia:

In computability theory, traditionally called recursion theory, a set S of natural numbers is called recursively enumerable, computably enumerable, semidecidable, provable or Turing-recognizable if:

There is an algorithm such that the set of input numbers for which the algorithm halts is exactly S.

Or, equivalently,

There is an algorithm that enumerates the members of S. That means that its output is simply a list of the members of S: s1, s2, s3, ... . If necessary, this algorithm may run forever.

Cutland:

A is recursively enumerable if the function f given by f (x) = 1 if x in A, f (x) = undefined if x not in A is computable.

Soare:

A set A is recursively enumerable (r.e.) if A is the domain of some p.r. function.

Kozen:

recursively enumerable (r.e.) if it is L(M) for some Turing machine M,

Stanford Encyclopedia (article by Immerman)

S is r.e. if and only if there is some Turing machine, M, such that S is the image of the function computed by M

nlab:

recursively enumerable sets, which are domains of partial recursive functions f:ℕ k→ℕf: \mathbb{N}^k \to \mathbb{N}, or equivalently images of total recursive functions.

Consensus seems to be that there is absolutely no consensus.

In the synthetic world, the situation is better (but probably just because of less publications compared to traditional computability):

Bauer (First steps in synthetic computability theory):

A set A is enumerable, or countable, if there exists a surjection > e : N → 1 + A, called an enumeration of A.

Richman (Church's thesis without tears) [I redacted the definition because in the paper it's with an example]

(recursively enumerable) if we can enumerate the elements of A via a function a : nat -> nat s.t. forall x in A, exists n, a n = x

My opinion:

The situation in related work is messy. I think we shouldn't follow any reference and just choose the names which describe the concepts they define best.

Recursive enumerability / enumerability should in my opinion thus be concerned with the range of a function, and I think the definition we picked in the CPP'19 paper with Dominik and Gert is exactly right (plus it agrees with Bauer, probably because we were inspired by him).

Bauer also defines semi-decidable propositions as semidecidable (P : Prop) := exists f : nat -> bool, P <-> exists n, f n = true. I like this naming convention (lifted to predicates), but I am in principle not against calling this "recognisability", as we have done in the H10 paper.

@mrhaandi @DmxLarchey @dominik-kirst Maybe let's share opinions here and then do a PR for the library which moves all the definitions (plus their informative counterparts) to the same place?

[DmxLarchey]

Very good ... let us start from this review

[DmxLarchey]

@yforster I guess "p.r." in the def. of Soare means "partial recursive" and not "primitive recursive"

@yforster In the H10 paper, we used recognisable as "equivalent to the termination predicate of a Minsky machine". In this sense, there is no chance it matches any synthetic notion ...