From: Marshall on
On Mar 12, 6:09 am, Patricia Shanahan <p...(a)acm.org> wrote:
>
> There has been a long term trend in computer science to assume that the
> current limit on hardware integer arithmetic is so large that there is
> no need to allow for integer overflow. So far, it has not worked.

I love the understatedness of "has not worked."

I wonder if it wouldn't be useful for a programming language to
have both arbitrary-precision integers and naturals, as well as
machine-sized signed and unsigned ints. In a sufficiently
expressive language, it would be possible to formalize
the properties of these as rings.


Marshall
From: Patricia Shanahan on
Marshall wrote:
> On Mar 12, 6:09 am, Patricia Shanahan <p...(a)acm.org> wrote:
>> There has been a long term trend in computer science to assume that the
>> current limit on hardware integer arithmetic is so large that there is
>> no need to allow for integer overflow. So far, it has not worked.
>
> I love the understatedness of "has not worked."
>
> I wonder if it wouldn't be useful for a programming language to
> have both arbitrary-precision integers and naturals, as well as
> machine-sized signed and unsigned ints. In a sufficiently
> expressive language, it would be possible to formalize
> the properties of these as rings.

Many languages do have arbitrary range integers. For example, Java has
java.math.BigInteger. Haskell has Integer. Those types cannot overflow,
but your program may run out of memory. Unfortunately, they tend to be
much worse performance, and bigger memory footprint, than the bounded
range machine integers. The machine integers are usually used for most
housekeeping activities, such as indexing data structures.

Patricia
From: tchow on
In article <0f-dne3xYo6a1gfWnZ2dnUVZ_jidnZ2d(a)earthlink.com>,
Patricia Shanahan <pats(a)acm.org> wrote:
>I'm really looking forward to seeing a good theory of limits and
>calculus that completely avoids the idea of an infinite sequence. I
>think that may be even harder than calculating the largest possible
>intermediate result.

What exactly do you mean by "avoids the idea"? Do you just mean that
the formalism makes no mention of infinite sequences? Even if the
formalism avoids it, the "idea" behind the formalism might secretly
be motivated by infinite sequences. Indeed, it's hard to imagine any
treatment of calculus that cannot be thought of in terms of infinite
sequences, at least informally.

Depending on how strict your criteria are, formalizing calculus without
explicit mention of infinite sequences is not difficult. It can certainly
be done in first-order Peano arithmetic, and I think much of it can even
be done in primitive recursive arithmetic.
--
Tim Chow tchow-at-alum-dot-mit-dot-edu
The range of our projectiles---even ... the artillery---however great, will
never exceed four of those miles of which as many thousand separate us from
the center of the earth. ---Galileo, Dialogues Concerning Two New Sciences
From: Transfer Principle on
On Mar 11, 10:58 pm, Transfer Principle <lwal...(a)lausd.net> wrote:
> So it may be helpful to
> find a theory T such that V_7 is a model of T.

Correction: It may be helpful to find a theory T such that V_7 is the
largest possible model of T. In other words, T has no model of
strictly larger cardinality than that of V_7, and so in particular, it
has no infinite models.
From: Transfer Principle on
On Mar 12, 10:10 am, tc...(a)lsa.umich.edu wrote:
> In article <0f-dne3xYo6a1gfWnZ2dnUVZ_jidn...(a)earthlink.com>,
> Patricia Shanahan  <p...(a)acm.org> wrote:
> >I'm really looking forward to seeing a good theory of limits and
> >calculus that completely avoids the idea of an infinite sequence. I
> >think that may be even harder than calculating the largest possible
> >intermediate result.
> Depending on how strict your criteria are, formalizing calculus without
> explicit mention of infinite sequences is not difficult.  It can certainly
> be done in first-order Peano arithmetic, and I think much of it can even
> be done in primitive recursive arithmetic.

But the formalization of calculus must be relatively _simple_ --
perhaps
nearly as simply as it can be done in ZFC. Otherwise, the standard
theorists will point out that the theory is less "powerful" and more
"cumbersome" to use than just doing calculus with ZFC and a complete
ordered field.

Indeed, we recall how Marshall Spight has already mentioned how the
so-called "cranks" are trying to some up with theories that are "less
powerful" and "more work to use" just to avoid some counterintuitive
notion (in this case infinitude). So we need an ultrafinitist theory
that
_doesn't_ fit Spight's description of "less powerful" and "more work
to use."