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

From	Ruvim <ruvim.pinka@gmail.com>
Newsgroups	comp.lang.forth
Subject	Semantics as observable behavior (was: single-xt approach in the standard)
Date	2024-09-22 23:53 +0400
Organization	A noiseless patient Spider
Message-ID	<vcpsiu$25spg$4@dont-email.me> (permalink)
References	(3 earlier) <66ee34a2$1@news.ausics.net> <vcmbf2$1ifml$1@dont-email.me> <66ef7dc7$1@news.ausics.net> <vcpi98$25spg$1@dont-email.me> <2024Sep22.191342@mips.complang.tuwien.ac.at>

Show all headers | View raw

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`.

> 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.  *All* 
implementations for interpretation semantics that show this behavior are 
observationally equivalent to each other. The same black box argument 
applies to compilation semantics too.  See bellow.

> 
> 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.

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. And if I want to perform the 
interpretation semantics for a word, I want to perform namely this 
behavior. And there are no exceptions to this!

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.

But in fact we don't need the term "interpretation semantics" for 
anything else [1]. Nobody has given any rationale for that.

Then, why do we need to introduce *another* term?  Let us always use the 
term "interpretation semantics" in exactly this meaning.

The same applies to the term "compilation semantics".

> 
> 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.

[2] https://github.com/ForthHub/discussion/discussions/103#sect.excusing

--
Ruvim

Back to comp.lang.forth | Previous | Next — Previous 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