Re: Can you spot a flaw in this argument?

Re: Can you spot a flaw in this argument?

[Prof. Peter Johnstone]

Dear Gregory,

I think the problem resides in what you mean by "no internal structure".
If by this you mean that the *set* of names has no internal structure,
then it's obviously impossible -- to require the set to have decidable
equality is to impose internal structure on it. But it's still possible
for the names themselves to be atomic: you can identify the set of names
with the set of natural numbers (which has lots of internal structure,
including decidable equality) without identifying the individual names
with von Neumann-style natural numbers (or Russell-style cardinals,
or ...)

Peter Johnstone

On Thu, 25 Jun 2009, Meredith Gregory wrote:

> All,
>
> This is an argument about effective theories and so i would love to hear
> from the topos-theory crowd. i'll state the argument in lowly computational
> terms, using two distinct proposals for foundational models of computing:
> the lambda calculus and the ?-calculus. Both the lambda calculus and the
> ?-calculus suffer a dependence on a theory of names (aka variables). Both
> require two things of whatever theory of names is provided to them:
>
>   - at least countably infinitely many names
>   - an effective equality on names
>
> Now, to this recent proposals[1] add a third constraint, namely
>
>   - names are atomic -- they have no internal structure

...

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Can you spot a flaw in this argument?

[Meredith Gregory]

All,

This is an argument about effective theories and so i would love to hear
from the topos-theory crowd. i'll state the argument in lowly computational
terms, using two distinct proposals for foundational models of computing:
the lambda calculus and the π-calculus. Both the lambda calculus and the
π-calculus suffer a dependence on a theory of names (aka variables). Both
require two things of whatever theory of names is provided to them:

   - at least countably infinitely many names
   - an effective equality on names

Now, to this recent proposals[1] add a third constraint, namely

   - names are atomic -- they have no internal structure

To my way of thinking these three constraints are incompatible. i cannot see
how to make an effective equality on a countably infinite set of entities
that have no internal structure on which to rest the equality check. It
seems to me that the only possible expression of the equality is an infinite
table which states the results of comparing every single pair of atoms --
which is not going to fit into any realizable model of computation of which
i'm aware and understand.

Is there a way around this? If there is, i would be eternally grateful to be
enlightened.

The reason i focus on foundational proposals for theories of computation is
that one could drop the atomic requirement and allow names to have internal
structure, but because of the other two constraints one is dangerously close
to sneaking into a supposedly foundational account a theory of names that is
-- itself -- already sufficiently rich to model computation. (For example,
in many implementations of lambda or π-calculus, names are ultimately
represented as integers.) This would appear to undermine the foundational
character of the model of computation in question. This has led me to
constructions in which the internal structure of names *reflects* the
structure of computations. In fact, this idea has a simple monadic
characterization, but that's for another discussion.

i've already posted to this list an intuitive account of red/black set
theories that also side-step the issue of atoms with no structure which
allows to recast the FM-Set-Theory-based accounts of names onto what appears
to me to be the only construction that meets all the requirements mentioned
above: sufficiently many names, effective equality, restricting internal
structure of names to the structure of the proposal at hand. Again, if there
is a way to skate around this argumentation or debunk it, please consider
this a sincere call for help to do so.

Best wishes,

--greg

[1] See the Gabbay-Pitts papers on using FM-Set Theory for an account of
fresh names and alpha-equivalence.

-- 
L.G. Meredith
Managing Partner
Biosimilarity LLC
1219 NW 83rd St
Seattle, WA 98117

+1 206.650.3740

http://biosimilarity.blogspot.com


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]