Re: Formal Semantics of the Java "new" Operator

From: Lauri Alanko (la_at_iki.fi)
Date: 05/01/04

  • Next message: |-|erc: "Re: PROOF that emulators are impossible" 
    Date: 1 May 2004 21:35:44 GMT

    In article <e47110b3.0404301435.49e4989@posting.google.com>,
    Mattias Wikstr?m <mattias_wikst71@hotmail.com> wrote:
    > What I now wonder is: What kind of thing may a location be? I suppose
    > that in mathematics it will typically be a natural number, whereas for
    > a compiler writer it will typically be a relocatable memory address or
    > an "int".

    There are many different ways of implementing a programming language,
    and hence there are many different concrete representations of a
    theoretical "location". A memory address is a common one, but garbage
    collection blurs the relationship: there are infinite locations, but
    only a finite number of addresses, and the GC in some sense maps the
    former to the latter in a safe fashion: no two "live" locations are
    mapped to the same address at the same time.

    > In each of theese cases there is arbitrariness involved: When the
    > "new" operator gets called, an unused number must somehow be chosen.
    > Whenever I encounter arbitrariness in mathematics, I want to
    > understand its precise nature, and preferably do away with it.

    It is indeed arbitrary. Often, in operational semantics, the set of
    locations is not defined at all: its existence is simply postulated.
    Then we of course can not give an algorithm for choosing a new
    location, but we simply require that any new location must not be
    already allocated.

    The following rule from The Definition of Standard ML may illustrate
    this:

    s,E |- exp => ref,s' s',E |- atexp => v,s'' a \notin Dom(mem of s'')
    --------------------------------------------------------------------------
                      s,E |- exp atexp => a,(s'' + {a |-> v})

    What this says is that when a new reference cell is created, then
    _any_ location a can be returned, provided that it does not appear in
    the domain of the current map from locations to values.

    In a sense this means that the semantics is non-deterministic, since
    the returned location is not uniquely defined. I find this a bit
    bothersome, too.

    I don't see any reason why one couldn't just define the locations to
    be numbers. It shouldn't make any practical difference.

    > It seems to me that Java has something that can only be modelled in
    > traditional mathematics at the expence of introducing arbitrariness of
    > a special sort. This suggests using something other than traditional
    > mathematics to do the modelling (Java, at worst ;-) ).

    _All_ formalizations are arbitrary in the sense that the semantics of
    any language can be expressed in many different ways, yet only a
    single one is usually chosen.

    > Denotational semantics was what I primarily had in mind, but instead
    > of trying to find a semantics for Java, I would pick something
    > simpler. Let us say simply typed lambda calculus extended with a new
    > kind of functions that always give /new/ values as their results. I do
    > not know how to formalise this, but if you press me I may figure it
    > out.

    Maybe the simplest extension is "gensym" of lisp: the only thing it
    does is return a new value (a symbol) that is guaranteed to be
    distinct from any others. This is pretty easy to formalize: you don't
    need a mapping, but only an infinite supply of symbols and a way
    choose one that hasn't been allocated yet. Using numbers for symbols,
    this means that gensym can simply return successive numbers, and the
    only state that is needed is the next unallocated number.

    But really, don't take my word for all this. Ask in comp.lang.scheme
    or comp.lang.functional, where there are lots of people who can speak
    with some authority about these things.

    Lauri Alanko
    la@iki.fi

  • Next message: |-|erc: "Re: PROOF that emulators are impossible"

    Relevant Pages

    • Yes You Can Tell The Difference Revisited
      ... they must be relativized and the apparent predication eliminated. ... complicate our semantics in this way (for in semantics as in ... What makes mathematics objective, everyone learns in ... I'm not contending that aesthetic subjectivism is wrong, ...
      (rec.music.makers.guitar.acoustic)
    • Re: Yes You Can Tell The Difference Revisited
      ... they must be relativized and the apparent predication eliminated. ... complicate our semantics in this way (for in semantics as in ... What makes mathematics objective, everyone learns in ... I'm not contending that aesthetic subjectivism is wrong, ...
      (rec.music.makers.guitar.acoustic)
    • Re: Countable models of ZFC
      ... But if you don't like my views about the semantics of mathematics, ... language of set theory which isn't model-theoretic. ... in which the first-order language of set theory is interpreted ...
      (sci.logic)
    • Re: Universal grammar
      ... domain of mathematics. ... One might attempt to pin down this semantics using tree structures ... It is not difficult to write parser that ... logical models for the natural language semantics. ...
      (sci.lang)
    • Re: Formal Semantics of the Java "new" Operator
      ... > a compiler writer it will typically be a relocatable memory address or ... > In each of theese cases there is arbitrariness involved: ... > Whenever I encounter arbitrariness in mathematics, ... A Java interpreter written in Java has this ...
      (comp.theory)