Re: On raw strings in <origin> commit field

[Mark H Weaver <mhw@netris.org>]

Hi Liliana,

Earlier, I wrote:
> Sorry, but this is not even close to a valid argument that the set of
> possible push actions to a Git repo is uncountable.  In fact, it's quite
> easy to prove that the set is countable.  Any mathematician will know this.

I suppose I should give a proof.  I'll give two proofs.

First I'll give a very simple proof that depends on assuming that every
push action can be uniquely represented as a message of finite length.

You may imagine this representation as being something like the output
of "git log --patch --format=fuller" but with _every_ piece of
information that git has about the pushed commits included.

Better yet, you could imagine the representation as being closer to what
git push actually sends to the server: a set of references to mutate,
and a pack of objects reachable by those references.  As an
optimization, there is a more complex two-way exchange to avoid sending
objects that the server already has, but for purposes of this proof you
could imagine eliminating that optimization.

Anyway, if you'll accept that every push action can be represented as a
message of finite length, then the proof is very simple:

Observe that there exists a one-to-one correspondence between push
actions and a subset of messages of finite length, and moreover that
there exists a one-to-one correspondence between messages of finite
length and a subset of the natural numbers.

Therefore, there exists a one-to-one correspondence between push actions
and a subset of the natural numbers.  Thus, the set of push actions is
countable, by definition.  Q.E.D.

=-=-=

If you don't accept the assumption above, here's a more detailed proof
that could be adapted to *any* kind of action that can be communicated
over a digital communications channel in finite time:


First, note that every push action can be performed by exchanging a
finite number of messages of finite length between the client and
server, hereafter referred to as a "finite exchange".

Let P be the set of possible push actions.

Let V be the subset of finite exchanges that represent a push action,
hereafter referred to as a "valid exchange".

Let f : V -> P be a function that maps valid exchanges to the push
actions that they represent.

Observe that f is surjective, i.e. for all p in P, there exists v in V
such that f(v) = p.  In other words, for every push action, there exists
at least one valid exchange that represents that push action.

Since f : V -> P is a surjective function, it follows that the
cardinality of V is greater than or equal to the cardinality of P.

Now, note that any valid exchange can be represented as a bit string of
finite length, and therefore as a natural number.  (There are many ways
to do this; the details are left as an exercise).

Therefore, the set V of valid exchanges is in one-to-one correspondence
with a subset of the natural numbers, and is therefore countable, by
definition.

Since V is countable, and it has cardinality greater than or equal to
the cardinality of P, it follows that P (the set of push actions) is
also countable.  Q.E.D.

      Mark

-- 
Disinformation flourishes because many people care deeply about injustice
but very few check the facts.  Ask me about <https://stallmansupport.org>.