Proposal: [251] Clarification for execution token

Formal

This page is dedicated to discussing this specific proposal

ContributeContributions

ruvavatar of ruv [251] Clarification for execution tokenProposal2022-08-13 20:16:29

Author

Ruv

Change Log

  • 2022-08-13 Initial version

Preceding history

Problem

By the definition of the term "execution token" in Forth-94 and Forth-2012, it's a value that identifies execution semantics. Can such value identify other behavior, e.g. some interpretation semantics or compilation semantics? It's unclear at the first glance.

Solution

Actually, an execution token can identify other semantics too, but only if they are equivalent to the execution semantics that this token identifies.

It is so because for any execution token there exists at least one named or unnamed Forth definition the execution semantics of which are identified by this execution token. So, in any case, an execution token always identifies some execution semantics, but accidentally these semantics can be equivalent to some interpretation semantics, or some compilation semantics, and then it identifies them too. It's unnecessary that they connected to the same Forth definition. Also, consequently, it's impossible that an execution token identifies some compilation semantics, or some interpretation semantics, but doesn't identify the equivalent execution semantics.

To solve the initial problem we can state these basics explicitly in a normative part.

Example

: foo postpone if ;
:noname postpone if ; ( xt )

The execution semantics for foo are equivalent to the compilation semantics for if. xt that is left on the stack identifies the execution semantics for an anonymous Forth definition, and these semantics are equivalent to the compilation semantics for if.

Typical use

When an execution token is intended to perform the interpretation semantics or compilation semantics for a word, the execution semantics that this token identifies should be also described to avoid ambiguity.

Example of wrong use:

  • xt identifies the interpretation semantics of the word X.

Example of right use:

  • The execution semantics identified by xt are equivalent to the interpretation semantics of the word X.
  • Performing the execution semantics identified by xt in interpretation state performs the interpretation semantics of the word X.
  • Executing xt in interpretation state performs the interpretation semantics of the word X.

Actually, the standard contains only three places where the "execution token" notion is used ambiguously — the glossary entries for FIND, NAME>INTERPRET and NAME>COMPILE. These entries have not only this but also some other problems, so they should be corrected anyway. The corresponding proposals are also in progress already.

Proposal

Add into beginning of the section 3.1.3.5 Execution tokens the following paragraph:

For any execution token there exists at least one Forth definition (named or unnamed) the execution semantics of which are identified by this execution token. The execution semantics identified by an execution token may be equivalent to the interpretation semantics or compilation semantics for some word, or to some run-time semantics.

UlrichHoffmannavatar of UlrichHoffmann

The committee considers this proposal formal.

Formal

ruvavatar of ruvNew Version: [251] Clarification for execution token

Hide differences

Author

Ruv

Change Log

(the latest at the top)

  • 2022-09-19 explicitly allow a short formula, describe what it means, better wording, fix some typos
  • 2022-08-13 Initial version

Preceding history

(the latest at the top)

Problem

By the definition of the term "execution token" in Forth-94 and Forth-2012, it's a value that identifies execution semantics. Can such value identify other behavior, e.g. some interpretation semantics or compilation semantics? It's unclear at the first glance.

Solution

Actually, an execution token can identify other semantics too, but only if they are equivalent to the execution semantics that this token identifies.

Actually, an execution token can identify other semantics too, but only if they are equivalent to the execution semantics that this token also identifies.

It is so because for any execution token there exists at least one named or unnamed Forth definition the execution semantics of which are identified by this execution token. So, in any case, an execution token always identifies some execution semantics, but accidentally these semantics can be equivalent to some interpretation semantics, or some compilation semantics, and then it identifies them too. It's unnecessary that they connected to the same Forth definition. Also, consequently, it's impossible that an execution token identifies some compilation semantics, or some interpretation semantics, but doesn't identify the equivalent execution semantics.

It is so because for any execution token there exists at least one named or unnamed Forth definition the execution semantics of which are identified by this execution token. So, in any case, an execution token always identifies some execution semantics, but accidentally these semantics can be equivalent to some interpretation semantics, or some compilation semantics, and then it identifies them too. It's unnecessary that they connected to the same Forth definition. Also, consequently, it's impossible that an execution token identifies some compilation semantics, or some interpretation semantics, but doesn't identify the equivalent execution semantics.

To solve the initial problem we can state these basics explicitly in a normative part.

Example

: foo postpone if ;
:noname postpone if ; ( xt )

The execution semantics for foo are equivalent to the compilation semantics for if. xt that is left on the stack identifies the execution semantics for an anonymous Forth definition, and these semantics are equivalent to the compilation semantics for if.

The execution semantics of foo are equivalent to the compilation semantics for if.

In the same time, a Forth system may provide system-dependent execution semantics of if that are not equivalent to the execution semantics of foo.

Typical use

xt, which is left on the stack, identifies the execution semantics of an anonymous Forth definition, and these execution semantics are equivalent to the compilation semantics for if.

When an execution token is intended to perform the interpretation semantics or compilation semantics for a word, the execution semantics that this token identifies should be also described to avoid ambiguity.

Example of wrong use:

  • xt identifies the interpretation semantics of the word X.

Typical use

Example of right use:

  • The execution semantics identified by xt are equivalent to the interpretation semantics of the word X.
  • Performing the execution semantics identified by xt in interpretation state performs the interpretation semantics of the word X.
  • Executing xt in interpretation state performs the interpretation semantics of the word X.
  • "xt identifies the compilation semantics for the word FOO"
    • It means that the execution token xt identifies the execution semantics which are equivalent to the compilation semantics for the word FOO.
    • In the same time the execution semantics of the word FOO can be different form the execution semantics identified by this xt.
  • "the execution token for the word BAR"
    • It means that this execution token identifies the execution semantics of the word BAR.

Actually, the standard contains only three places where the "execution token" notion is used ambiguously — the glossary entries for FIND, NAME>INTERPRET and NAME>COMPILE. These entries have not only this but also some other problems, so they should be corrected anyway. The corresponding proposals are also in progress already.

  • The execution semantics identified by xt are equivalent to the interpretation semantics for the word BAZ.
    • This seems pretty clear.

Wrong use

Actually, the standard contains only one place where the "execution token" notion is used ambiguously in a normative part — the glossary entry for FIND. Since it says that FIND returns the execution token for a word, but actually this token cannot identify the execution semantics of this word in some cases in dual-xy systems.

In another glossary entry — for NAME>INTERPRET — the language is just slightly non normative, since it uses the form "xt represents" instead of the form "xt identifies".

These entries have not only this but also some other problems, so they should be corrected anyway, and my proposals for them are in progress.

Proposal

Add into beginning of the section 3.1.3.5 Execution tokens the following paragraph:

Add into beginning of the section 3.1.3.5 Execution tokens the following paragraphs:

For any execution token there exists at least one Forth definition (named or unnamed) the execution semantics of which are identified by this execution token.

The execution semantics identified by an execution token may be equivalent to the interpretation semantics or compilation semantics for some word, or to some run-time semantics.

The execution semantics identified by an execution token can be equivalent to the interpretation semantics or compilation semantics for some word, or to some run-time semantics. In such a case this execution token also identifies the corresponding interpretation semantics, compilation semantics, or run-time semantics.

Unless otherwise indicated, the execution token for a named Forth definition identifies the execution semantics for this definition.
Reply New Version