Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]


Groups > comp.lang.forth > #132292

Re: Semantics as observable behavior (was: single-xt approach in the standard)

From anton@mips.complang.tuwien.ac.at (Anton Ertl)
Newsgroups comp.lang.forth
Subject Re: Semantics as observable behavior (was: single-xt approach in the standard)
Date 2024-09-22 21:04 +0000
Organization Institut fuer Computersprachen, Technische Universitaet Wien
Message-ID <2024Sep22.230424@mips.complang.tuwien.ac.at> (permalink)
References (4 earlier) <vcmbf2$1ifml$1@dont-email.me> <66ef7dc7$1@news.ausics.net> <vcpi98$25spg$1@dont-email.me> <2024Sep22.191342@mips.complang.tuwien.ac.at> <vcpsiu$25spg$4@dont-email.me>

Show all headers | View raw


Ruvim <ruvim.pinka@gmail.com> writes:
>On 2024-09-22 21:13, Anton Ertl wrote:
>> Ruvim <ruvim.pinka@gmail.com> writes:
>>> - All standard programs are single-xt programs (in the part of
>>> user-defined words). Why we should remove the way to document this
>>> programs/words in the standard terms of interpretation semantics,
>>> compilation semantics and execution semantics?
>> 
>> Who proposes removing that?  I often write about the interpretatation
>> and compilation semantics of various words with default compilation
>> semantics or with immediate compilation semantics, and I see nobody
>> who wants to remove that possibility.
>> 
>> Examples:
>> 
>> : foo 1 ;
>> 
>> The execution semantics of FOO are to push 1 on the data stack.
>> The interpretation semantics of FOO are to push 1 on the data stack.
>> The compilation semantics of FOO are append the execution semantics of
>> FOO to the current definition.
>> 
>> : bar state @ ; immediate
>> 
>> The execution semantics of BAR are to push the contents of STATE on
>> the data stack.
>
>Do you agree that this describes an observable behavior, not an 
>implementation?  And all the implementations for execution semantics 
>that show this behavior are observationally equivalent to each other?
>
>For example, this definition:
>
>: bar2  state @ if  state @  else  0  then ; immediate
>
>is observationally equivalent to your `bar`.

Yes.  So what?

>> The interpretation semantics of BAR are to push the contents of STATE
>> on the data stack.
>
>I think, we should use the black box model — specify what can be 
>observed. And according to what can be observed, the interpretation 
>semantics of this word are to push zero on the data stack.

No.

: [execute] execute ; immediate
s" bar" find-name name>interpret ] [execute] [ . \ prints -1

Use FIND-NAME or FIND-NAME-IN based on TRAVERSE-WORDLIST if the system
at hand does not implement FIND-NAME yet.

>> The compilation semantics of BAR are to push the contents of STATE on
>> the data stack.
>
>
>
>Anton, forgive me for being blunt, but I think your understanding of 
>"interpretation semantics" and "compilation semantics" for words whose 
>execution semantics depend on STATE is useless both in practice and in 
>theory.

It's very useful, in particular for predicting how a system behaves.
I leave it up to you whether you consider this theory or practice.

>Take a look at my next rationale.
>
>When I'm interested in the interpretation semantics of a word, I'm 
>interested in precisely the behavior that can be *observed* when the 
>Forth text interpreter encounters the name of this word in 
>interpretation state.  And if I specify the interpretation semantics for 
>a word, I specify namely this behavior.

Now coming back from wishful thinking to reality, that's not how
systems behave.

>If we say that the term "interpretation semantics" means something else 
>in some cases, we should introduce another term to denote the behavior 
>that can be observed when the Forth text interpreter encounters the name 
>of a word in interpretation state.

It's the other way 'round: The standard specifies the interpretation
semantics and compilation semantics of words (either explicitly, or
through default mechanisms), and the text interpreter then performs
the interpretation semantics when it encounters the word in interpret
state, and it performs the compilation semantics when it encounters
the word in compilation state.

In the example above, the standard specifies unambiguously how the
execution semantics of BAR derives from STATE and @, and how the
interpretation semantics and compilation semantics of BAR are derived
from the execution semantics of BAR.

>> With that we can then determine what code like
>> 
>> : bla postpone bar ; immediate
>> bla .     \ prints 0
>> ] bla [ . \ prints -1
>> 
>> should do; I show the output in comments.  I just tested gforth,
>> iforth, SwiftForth, and VFX Forth, and unsurprisingly they all produce
>> the output shown in the comments.
>> 
>
>[1] Well, I can see only one reason for using another meaning for the 
>"interpretation semantics" and "compilation semantics" terms than given 
>above: to represent the classic implementation of `postpone` as 
>conforming to what is formally specified in Forth-94, without accepting 
>into the standard the proposed ambiguous condition (see [2]).  But it is 
>better to honestly say that "postpone" appends execution semantics of 
>the word if this word is an immediate word. There is no need to blur the 
>meaning of terms.

The meaning of the compilation semantics of BAR is crystal-clear, and
likewise the interpretation semantics of BLA and the compilation
semantics of BLA.  There is nothing blurred here.

As to the definition of POSTPONE, it is very straightforward, and
every system implements it correctly.  No need for a redefinition.

They may not be what you wish for, but they are clearly defined.

- anton
-- 
M. Anton Ertl  http://www.complang.tuwien.ac.at/anton/home.html
comp.lang.forth FAQs: http://www.complang.tuwien.ac.at/forth/faq/toc.html
     New standard: https://forth-standard.org/
   EuroForth 2024: https://euro.theforth.net

Back to comp.lang.forth | Previous | NextPrevious in thread | Next in thread | Find similar


Thread

single-xt approach in the standard Ruvim <ruvim.pinka@gmail.com> - 2024-09-17 14:54 +0400
  Re: single-xt approach in the standard minforth@gmx.net (minforth) - 2024-09-17 11:20 +0000
    Re: single-xt approach in the standard Ruvim <ruvim.pinka@gmail.com> - 2024-09-17 15:59 +0400
      Re: single-xt approach in the standard Anthony Howe <achowe@snert.com> - 2024-09-17 14:58 -0400
        Re: single-xt approach in the standard dxf <dxforth@gmail.com> - 2024-09-18 13:39 +1000
          Standardization process (was: single-xt approach in the standard) Ruvim <ruvim.pinka@gmail.com> - 2024-09-18 11:07 +0400
            Re: Standardization process dxf <dxforth@gmail.com> - 2024-09-18 20:16 +1000
              Re: Standardization process Ruvim <ruvim.pinka@gmail.com> - 2024-09-18 14:51 +0400
                Re: Standardization process dxf <dxforth@gmail.com> - 2024-09-18 23:39 +1000
                Re: Standardization process Ruvim <ruvim.pinka@gmail.com> - 2024-09-18 18:41 +0400
              Re: Standardization process Ruvim <ruvim.pinka@gmail.com> - 2024-09-18 15:59 +0400
        Re: single-xt approach in the standard Ruvim <ruvim.pinka@gmail.com> - 2024-09-18 12:44 +0400
          Re: single-xt approach in the standard Gerry Jackson <do-not-use@swldwa.uk> - 2024-09-18 21:59 +0100
            Re: single-xt approach in the standard albert@spenarnc.xs4all.nl - 2024-09-19 10:17 +0200
            Standard testsuite (was: single-xt approach in the standard) Ruvim <ruvim.pinka@gmail.com> - 2024-09-19 12:24 +0400
              Re: Standard testsuite (was: single-xt approach in the standard) albert@spenarnc.xs4all.nl - 2024-09-19 10:54 +0200
  Re: single-xt approach in the standard mhx@iae.nl (mhx) - 2024-09-17 12:15 +0000
    Re: single-xt approach in the standard Ruvim <ruvim.pinka@gmail.com> - 2024-09-17 17:04 +0400
      Re: single-xt approach in the standard minforth@gmx.net (minforth) - 2024-09-17 13:58 +0000
        Re: single-xt approach in the standard Ruvim <ruvim.pinka@gmail.com> - 2024-09-17 18:55 +0400
          Re: single-xt approach in the standard albert@spenarnc.xs4all.nl - 2024-09-17 17:22 +0200
      Re: single-xt approach in the standard dxf <dxforth@gmail.com> - 2024-09-21 12:51 +1000
        Re: single-xt approach in the standard Ruvim <ruvim.pinka@gmail.com> - 2024-09-21 15:42 +0400
          Re: single-xt approach in the standard dxf <dxforth@gmail.com> - 2024-09-22 12:15 +1000
            Re: single-xt approach in the standard anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2024-09-22 07:54 +0000
              Re: single-xt approach in the standard albert@spenarnc.xs4all.nl - 2024-09-22 12:05 +0200
              Re: single-xt approach in the standard dxf <dxforth@gmail.com> - 2024-09-23 13:34 +1000
                Re: single-xt approach in the standard Anthony Howe <achowe@snert.com> - 2024-09-23 10:45 -0400
                Re: single-xt approach in the standard dxf <dxforth@gmail.com> - 2024-09-24 14:50 +1000
                Re: single-xt approach in the standard dxf <dxforth@gmail.com> - 2024-09-25 10:35 +1000
            Re: single-xt approach in the standard Ruvim <ruvim.pinka@gmail.com> - 2024-09-22 20:57 +0400
              Re: single-xt approach in the standard anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2024-09-22 17:13 +0000
                Semantics as observable behavior (was: single-xt approach in the standard) Ruvim <ruvim.pinka@gmail.com> - 2024-09-22 23:53 +0400
                Re: Semantics as observable behavior (was: single-xt approach in the standard) anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2024-09-22 21:04 +0000
                Re: Semantics as observable behavior Ruvim <ruvim.pinka@gmail.com> - 2024-09-23 02:01 +0400
                Re: Semantics as observable behavior Ruvim <ruvim.pinka@gmail.com> - 2024-09-23 11:36 +0400
              Re: single-xt approach in the standard albert@spenarnc.xs4all.nl - 2024-09-22 21:34 +0200
                Re: single-xt approach in the standard Ruvim <ruvim.pinka@gmail.com> - 2024-09-23 00:02 +0400
                Re: single-xt approach in the standard albert@spenarnc.xs4all.nl - 2024-09-23 09:40 +0200
                Re: single-xt approach in the standard minforth@gmx.net (minforth) - 2024-09-23 08:42 +0000
              Re: single-xt approach in the standard dxf <dxforth@gmail.com> - 2024-09-23 15:28 +1000
                Standard compliance for systems (was: single-xt approach in the standard) Ruvim <ruvim.pinka@gmail.com> - 2024-09-23 10:56 +0400
                Re: Standard compliance for systems dxf <dxforth@gmail.com> - 2024-11-22 16:49 +1100
                Re: Standard compliance for systems minforth@gmx.net (minforth) - 2024-11-22 10:11 +0000
                Re: Standard compliance for systems mhx@iae.nl (mhx) - 2024-11-22 11:35 +0000
                Re: Standard compliance for systems minforth@gmx.net (minforth) - 2024-11-22 13:11 +0000
                Re: Standard compliance for systems mhx@iae.nl (mhx) - 2024-11-22 15:26 +0000
                Re: Standard compliance for systems dxf <dxforth@gmail.com> - 2024-11-23 11:54 +1100
                Re: Standard compliance for systems albert@spenarnc.xs4all.nl - 2024-11-23 14:09 +0100
                Re: Standard compliance for systems dxf <dxforth@gmail.com> - 2024-11-24 12:02 +1100
      Re: single-xt approach in the standard Stephen Pelc <stephen@vfxforth.com> - 2024-09-21 14:47 +0000
        Re: single-xt approach in the standard Ruvim <ruvim.pinka@gmail.com> - 2024-09-21 23:18 +0400
          Re: single-xt approach in the standard Stephen Pelc <stephen@vfxforth.com> - 2024-09-22 12:09 +0000
            Re: single-xt approach in the standard anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2024-09-22 14:28 +0000
            Re: single-xt approach in the standard albert@spenarnc.xs4all.nl - 2024-09-22 21:20 +0200
      Re: single-xt approach in the standard albert@spenarnc.xs4all.nl - 2024-09-22 11:53 +0200
        Re: single-xt approach in the standard Ruvim <ruvim.pinka@gmail.com> - 2024-09-23 01:15 +0400
          Re: single-xt approach in the standard albert@spenarnc.xs4all.nl - 2024-09-23 10:36 +0200
            Re: single-xt approach in the standard mhx@iae.nl (mhx) - 2024-09-23 09:32 +0000
              Re: single-xt approach in the standard albert@spenarnc.xs4all.nl - 2024-09-23 13:57 +0200
              Re: single-xt approach in the standard anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2024-09-23 17:02 +0000
                Re: single-xt approach in the standard mhx@iae.nl (mhx) - 2024-09-23 19:20 +0000
            Re: single-xt approach in the standard Ruvim <ruvim.pinka@gmail.com> - 2024-09-23 14:16 +0400
              Re: single-xt approach in the standard anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2024-09-23 16:52 +0000
                Re: single-xt approach in the standard Ruvim <ruvim.pinka@gmail.com> - 2024-09-25 11:27 +0400
    Re: single-xt approach in the standard albert@spenarnc.xs4all.nl - 2024-09-17 17:18 +0200
  Re: single-xt approach in the standard Anthony Howe <achowe@snert.com> - 2024-09-17 15:12 -0400
    Re: single-xt approach in the standard anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2024-09-17 19:25 +0000
      Re: single-xt approach in the standard Anthony Howe <achowe@snert.com> - 2024-09-24 07:08 -0400
    Re: single-xt approach in the standard Stephen Pelc <stephen@vfxforth.com> - 2024-09-17 23:04 +0000
      Re: single-xt approach in the standard Ruvim <ruvim.pinka@gmail.com> - 2024-09-18 10:10 +0400
        Re: single-xt approach in the standard mhx@iae.nl (mhx) - 2024-09-18 06:38 +0000
          Re: single-xt approach in the standard Ruvim <ruvim.pinka@gmail.com> - 2024-09-19 12:26 +0400
    Re: single-xt approach in the standard Ruvim <ruvim.pinka@gmail.com> - 2024-09-18 14:34 +0400
      Re: single-xt approach in the standard Ruvim <ruvim.pinka@gmail.com> - 2024-09-18 16:41 +0400
      Re: single-xt approach in the standard Hans Bezemer <the.beez.speaks@gmail.com> - 2024-09-18 18:43 +0200
        Re: single-xt approach in the standard albert@spenarnc.xs4all.nl - 2024-09-19 10:36 +0200
          Re: single-xt approach in the standard Hans Bezemer <the.beez.speaks@gmail.com> - 2024-09-20 14:58 +0200
  Re: single-xt approach in the standard anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2024-09-17 21:15 +0000
  Re: single-xt approach in the standard Ruvim <ruvim.pinka@gmail.com> - 2024-09-18 12:15 +0400
  Re: single-xt approach in the standard peter.m.falth@gmail.com (PMF) - 2024-09-21 21:28 +0000
    Re: single-xt approach in the standard anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2024-09-22 07:23 +0000
    Re: single-xt approach in the standard Ruvim <ruvim.pinka@gmail.com> - 2024-09-22 21:34 +0400

csiph-web