11institutetext: Delft University of Technology, The Netherlands
22institutetext: Swansea University, United Kingdom
22email<EMAIL_ADDRESS>
# Fundamental Constructs in Programming Languages

(Submitted Draft)

Peter D. Mosses 1122 0000-0002-5826-7520

###### Abstract

Specifying the semantics of a programming language formally can have many
benefits. However, it can also require a huge effort. The effort can be
significantly reduced by translating language syntax to so-called fundamental
constructs (funcons). A translation to funcons is easy to update when the
language evolves, and it exposes relationships between individual language
constructs.

The PLanCompS project has developed an initial collection of funcons
(primarily for translation of functional and imperative languages). The
behaviour of each funcon is defined, once and for all, using a modular variant
of structural operational semantics. The definitions are available online.

This paper introduces and motivates funcons. It illustrates translation of
language constructs to funcons, and how funcons are defined. It also relates
funcons to notation used in previous frameworks, including monadic semantics
and action semantics.

###### Keywords:

Funcons Programming constructs Formal specification

##  1 Introduction

Many constructs found in (high-level) programming languages combine several
behavioural features. For example, call-by-value parameter passing in an
imperative language involves order of evaluation, allocating storage and
initialising its contents, local name binding, and lexical scoping. Such
language constructs generally provide conciseness and clarity in programs, and
may support efficient implementation techniques (e.g., stack-based storage);
but their behaviour can be quite difficult to understand, and tedious to
specify directly.

Moreover, constructs in different languages may look the same but have very
different behaviour (e.g., the notorious ‘`x=y`’), or look different but have
exactly the same behaviour (e.g., ‘`while...do...`’ and ‘`while(...){...}`’).
Relatively minor differences between similar language constructs in different
languages include order of evaluation in expressions, and the effect of
arithmetic overflow. The evolution of programming languages has resulted in a
huge diversity of language constructs and their variants. Some of the
constructs are quite simple, but no programming lingua franca has emerged.

The PLanCompS project111https://plancomps.github.io is aiming to isolate a
collection of fundamental constructs (‘funcons’) from which the behaviour of
all existing high-level programming language constructs can be composed.
Funcons should be significantly simpler than typical language constructs, in
general:

  * •

Each funcon should affect only a single behavioural feature.

  * •

Variants of funcon behaviour (e.g., evaluating their arguments in a different
order) should be obtainable by composition.

  * •

Funcons should abstract from details related to implementation efficiency.

The definition of a funcon determines its name, its signature, and its
behaviour. Each funcon name should have a _unique_ definition, so that it
always refers to the same signature and behaviour, regardless of where the
reference occurs. To support reuse, funcon definitions need to be _fixed_ and
_permanent_ : changing or removing funcons would undermine the validity of
translations that use them. In particular, adding a new funcon to a collection
must never require changes to the previous definitions.

Version control is superfluous for funcons; translations of language
constructs to funcons, in contrast, may need to change when the specified
language evolves. For example, the illustrative language IMP includes a plain
old while-loop with a Boolean-valued condition; the following rule translates
its execution to the funcon while-true, which has exactly the required
behaviour:

Rule $\displaystyle{\color[rgb]{0,0,.545}\textsf{execute}}\llbracket\
\textsf{{\color[rgb]{.752,.752,.752}`}{while}{\color[rgb]{.752,.752,.752}'}}\
\textsf{{\color[rgb]{.752,.752,.752}`}{(}{\color[rgb]{.752,.752,.752}'}}\
{\color[rgb]{0,0,0}\textit{BExp}}\
\textsf{{\color[rgb]{.752,.752,.752}`}{)}{\color[rgb]{.752,.752,.752}'}}\
{\color[rgb]{0,0,0}\textit{Block}}\ \rrbracket=$
$\displaystyle\quad{\color[rgb]{.545,0,0}\textsf{while-
true}}({\color[rgb]{0,0,.545}\textsf{eval-bool}}\llbracket\
{\color[rgb]{0,0,0}\textit{BExp}}\
\rrbracket,{\color[rgb]{0,0,.545}\textsf{execute}}\llbracket\
{\color[rgb]{0,0,0}\textit{Block}}\ \rrbracket)$

The behaviour of the funcon while-true is fixed. But suppose the IMP language
evolves, and a Block can now execute a statement ‘break;’, which is supposed
to terminate the closest-enclosing loop. We can extend the translation with
the following rule:

Rule $\displaystyle{\color[rgb]{0,0,.545}\textsf{execute}}\llbracket\
\textsf{{\color[rgb]{.752,.752,.752}`}{break}{\color[rgb]{.752,.752,.752}'}}\
\textsf{{\color[rgb]{.752,.752,.752}`}{;}{\color[rgb]{.752,.752,.752}'}}\
\rrbracket={\color[rgb]{.545,0,0}\textsf{abrupt}}({\color[rgb]{.545,0,0}\textsf{broken}})$

The funcon ${\color[rgb]{.545,0,0}\textsf{abrupt}}(V)$ terminates execution
abruptly, signalling its argument value $V$ as the reason for termination. The
translation of ‘while(true){break;}’ is now the funcon term
${\color[rgb]{.545,0,0}\textsf{while-
true}}({\color[rgb]{.545,0,0}\textsf{true}},{\color[rgb]{.545,0,0}\textsf{abrupt}}({\color[rgb]{.545,0,0}\textsf{broken}}))$.
However, the behaviour of ${\color[rgb]{.545,0,0}\textsf{while-
true}}({\color[rgb]{.545,0,0}\textsf{true}},X)$ is to terminate abruptly when
$X$ does – so this translation would lead to abrupt termination of _all_
enclosing while-loops! We cannot change the definition of while-true, so we
are forced to change the translation rule. The following updated translation
rule reflects the extension of the behaviour of while-loops with handling of
abrupt termination due to break-statements (and specifies that abrupt
termination for any other reason is propagated):

Rule $\displaystyle{\color[rgb]{0,0,.545}\textsf{execute}}\llbracket\
\textsf{{\color[rgb]{.752,.752,.752}`}{while}{\color[rgb]{.752,.752,.752}'}}\
\textsf{{\color[rgb]{.752,.752,.752}`}{(}{\color[rgb]{.752,.752,.752}'}}\
{\color[rgb]{0,0,0}\textit{BExp}}\
\textsf{{\color[rgb]{.752,.752,.752}`}{)}{\color[rgb]{.752,.752,.752}'}}\
{\color[rgb]{0,0,0}\textit{Block}}\ \rrbracket=$
$\displaystyle\quad{\color[rgb]{.545,0,0}\textsf{handle-abrupt}}($
$\displaystyle\quad\quad{\color[rgb]{.545,0,0}\textsf{while-
true}}({\color[rgb]{0,0,.545}\textsf{eval-bool}}\llbracket\
{\color[rgb]{0,0,0}\textit{BExp}}\
\rrbracket,{\color[rgb]{0,0,.545}\textsf{execute}}\llbracket\
{\color[rgb]{0,0,0}\textit{Block}}\ \rrbracket),$
$\displaystyle\quad\quad{\color[rgb]{.545,0,0}\textsf{if-true-
else}}({\color[rgb]{.545,0,0}\textsf{is-
equal}}({\color[rgb]{.545,0,0}\textsf{given}},{\color[rgb]{.545,0,0}\textsf{broken}}),{\color[rgb]{.545,0,0}\textsf{null-
value}},{\color[rgb]{.545,0,0}\textsf{abrupt}}({\color[rgb]{.545,0,0}\textsf{given}})))$

Handling abrupt termination of the current iteration due to continue-
statements is similar. (The specialised funcons
${\color[rgb]{.545,0,0}\textsf{handle-break}}(X)$ and
${\color[rgb]{.545,0,0}\textsf{handle-continue}}(X)$ can be used to express
the same behaviour more concisely.)

The PLanCompS project has developed an initial collection of funcons [23,
Funcons-beta], and demonstrated their use in some language specifications [23,
Languages-beta]. The collection aims to combine simplicity with
expressiveness: the funcons are simple enough to understand and define, yet
translation of many language constructs222Funcons for declarative and
graphical languages have not yet been developed. to funcons is also reasonably
simple. Funcon behaviour is defined using a modular variant [16, 20] of
structural operational semantics [24], based on value-computation transition
systems [5].

##### Contributions.

The reader is assumed to be interested in programming languages, and familiar
with their main concepts. The research on which this paper is based has been
published elsewhere [2, 5, 6, 16, 18, 19, 20]. The main aims here are to
motivate the general idea of funcons, and illustrate how they can be used to
explain the behaviour of programming language constructs:

  * •

We explain some general features of funcons (Sect. 2).

  * •

We consider how to manage collections of several hundred funcons (Sect. 3).

  * •

We analyse various facets of funcon behaviour (Sect. 4).

  * •

We illustrate translation of language constructs to funcons and explain how to
validate such translations (Sect. 5).

  * •

We illustrate how to define a funcon independently, once and for all (Sect.
6).

  * •

We relate funcons to auxiliary operations defined in denotational semantics,
to monads, and to the combinators used in action semantics (Sect. 7).

  * •

We conclude with plans for future development of funcons (Sect. 8),

Appendix 0.A gives an informal summary of the funcons defined in Funcons-
beta.333Appendix 0.A is to be omitted in the final version, and made available
on arXiv.

The rest of this paper is structured as responses to questions that readers
might ask about funcons. The author welcomes further questions, as well as
comments on the given responses.

##  2 The Nature of Funcons

Let us start by trying to clarify some general features of funcons.

  * •

_What aspects of behaviour do funcons represent?_

Funcons abstract from details related to implementation efficiency, such as
storage allocation algorithms and communication protocols. They express
implementation independent behaviour that arises when programs are executed.
They also express linguistic features on which that behaviour depends, such as
scopes of bindings.

  * •

_Can funcons be implemented efficiently?_

Funcons need to be executable, to support validation of language translations.
Their current implementation uses Haskell generated directly from their
definitions [3]. The efficiency of executing funcon terms is adequate for
running unit tests and typical test programs, but not applications.

  * •

_How complicated are funcons ?_

One might expect that funcons should be as simple as possible. In fact the aim
is for funcons to be not too complicated, not too simple – just right!

In the physical sciences, molecules are characterised and understood primarily
in terms of chemical bonds between their constituent atoms, and atoms are
formed from protons, neutrons, and electrons; protons and neutrons are
themselves composed from sub-atomic particles, such as quarks. To explain a
molecule in terms of sub-atomic particles might be possible, but unhelpful.
Language constructs are analogous to molecules, and funcons to atoms.

Introducing a funcon that corresponds directly to a complicated language
construct would make the funcon analysis of that language construct trivial,
but a direct definition of the funcon behaviour would then become complicated.
At the other extreme, taking pure function abstraction and application as the
only funcons would make analysis and specification of language constructs as
complicated as in (pre-monadic) denotational semantics.

  * •

_Can funcons have alternative behaviours?_

No, never. The behaviour of common language constructs, such as assignment
expressions and procedure calls, often varies significantly between different
language. For example, the order of evaluation of the two sides of an
assignment expression is left to right in some languages, right to left in
others, or may even be implementation-dependent; and the result may be the
target variable or the assigned value. The funcon for assignment needs to have
a behaviour from which all those variations can be obtained by composition
with other funcons.

  * •

_Are funcons independent?_

Funcons are often independent, but not always. For instance, the definition of
the funcon while-true specifies the reduction of
${\color[rgb]{.545,0,0}\textsf{while-true}}(B,X)$ to a term involving the
funcons if-true-else and sequential:

Funcon $\displaystyle{\color[rgb]{.545,0,0}\textsf{while-
true}}(B:\mathop{\Rightarrow}{\color[rgb]{.545,0,0}\textsf{booleans}},X:\mathop{\Rightarrow}{\color[rgb]{.545,0,0}\textsf{null-
type}}):\mathop{\Rightarrow}{\color[rgb]{.545,0,0}\textsf{null-type}}$
$\displaystyle\quad\leadsto{\color[rgb]{.545,0,0}\textsf{if-true-
else}}(B,{\color[rgb]{.545,0,0}\textsf{sequential}}(X,{\color[rgb]{.545,0,0}\textsf{while-
true}}(B,X)),{\color[rgb]{.545,0,0}\textsf{null-value}})$

Duplication of $B$ before starting to evaluate it is essential, in case it
needs to be re-evaluated after the execution of $X$. We could introduce an
auxiliary term constructor for that, but it is simpler to make use of if-true-
else and sequential.

  * •

_Do features of funcons interact?_

No. Feature interactions in software development tend to arise when
requirements are incomplete. An often cited example involves a flood
prevention system that turns off the water supply, and a sprinkler system that
depends on that water; the requirements regarding flood prevention should
include checking the safety of turning the water off…

The complete requirement for each funcon is to provide the behaviour specified
in its definition. The behaviour of its arguments is required to be consistent
with its signature, but there are no implicit requirements on the behaviour of
combined funcons.

  * •

_Can funcons be used as a programming language?_

Composing funcons is similar to the original idea of Unix: plugging simple
commands together to produce complex behaviour.444Nowadays, a Unix command
often has a multitude of obscure options, documented in a manual ‘page’ that
fills many screens. Not-so-fundamental constructs could be defined as
abbreviations for frequently-needed funcon compositions; a coating of
‘syntactic sugar’ would be needed to avoid an unwelcome plethora of
parentheses in larger funcon compositions. The main drawback would be the
comparatively low implementation efficiency.

  * •

_Can funcons be higher-order?_

Funcons can represent higher-order functions as values, but funcons are not
themselves higher-order: they require funcon terms as arguments. However, it
easy to define funcons for common idioms of higher-order programming (maps,
filters, folds, etc.).

  * •

_Do funcons have algebraic properties?_

Yes: many binary funcons are associative, with left and right units; some are
also commutative. These properties hold for a notion of bisimulation for
value-computation transition systems [5], which provide the foundations for
funcon definitions. This bisimulation is preserved when new funcons are added.
Funcon terms are written as applicative expressions, and associativity allows
binary funcons to be extended to longer sequences of arguments.

  * •

_Can I use my favourite proof assistant to prove properties of funcons?_

Some years ago, the modular variant [16] of structural operational semantics
used to define funcons was implemented in the Coq proof assistant, and modular
proofs of some properties were carried out [11]. In a related line of work
[30], a different method for modular proofs in Coq has been developed. Modular
proofs depend only on the definitions of the funcons involved, and remain
sound when funcon definitions are combined, so in principle, they could be
archived together with the collection of funcons.

##  3 Collections of Funcons

The Funcons-beta collection includes several hundred funcons. Management of
such a collection is non-trivial.

  * •

_How can we classify funcons?_

Most high-level programming languages distinguish syntactically between
commands (a.k.a. statements), declarations, and expressions. When executed,
commands generally have effects; declarations bind names to values; and
expressions compute values. However, such syntactic distinctions are not
universal: for instance, expressions sometimes subsume commands, and sequences
of commands may include declarations. Grammars for programming language syntax
(abstract as well as concrete) typically introduce many further syntactic
distinctions. A universal set of syntactic sorts that encompasses all
programming languages is not available.

For funcons, we have a single syntactic sort of terms. Funcon terms are
similar to expressions in functional programming languages: they compute
values of any type. A funcon term corresponding to a command computes a fixed
null value, and a term corresponding to a declaration computes a value
environment, mapping names to values.

We classify individual funcons according to their contribution to the
behaviour of enclosing funcon terms. The behaviour of some funcons involves
auxiliary entities, representing various kinds of effects. For instance,
funcons for name binding use an auxiliary environment entity to represent the
current bindings.

  * •

_How do we refer to a particular funcon in a collection?_

A collection of funcons is like an open package: the names of the funcons are
visible externally. Neither the classification of funcons nor the paths to
their definitions affects references to funcon names.

The name of each funcon should clearly suggest its behaviour, to support
casual reading of funcon terms and the potential use of funcons as a
controlled vocabulary for informal discussion and comparison of programming
languages. We can use plural words (e.g., lists) to distinguish type names
from other value names. When a funcon corresponds directly to a familiar
concept, a single well-chosen word can be adequate, but otherwise several
words may be needed. Moreover, different datatypes may have closely related
operations, yet the names for the corresponding funcons have to be distinct,
due to the absence of overloading: the name of the datatype can be added as a
prefix of the name, e.g., integer-add.555Currently, Funcons-beta does not
support namespaces in collections of funcons.

Suggestive names can be quite long, and abbreviations may be needed in some
situations (e.g., classrooms, examinations, presentations). Abbreviations can
be defined as explicit aliases for funcons, For instance, alloc-init is
defined as an alias for allocate-initialised-variable.

  * •

_Do funcons evolve?_

After a collection of funcons has been released, the behaviour of all the
funcons in it needs to be fixed and permanent, since changes could affect or
break their external uses. All uses of a particular funcon name thus refer to
the same behaviour.

However, the collection itself can evolve: by extension with new funcons. This
must not require changes to the definitions of the previous funcons. New
funcons need to be carefully checked and tested before they are added, since
their definitions cannot be revoked.

Names of funcons always refer implicitly to the current version of a
collection. Evolving collections of funcons have no need for version numbers,
since once a name has been defined, adding names for new funcons (or even new
aliases for the same funcon) cannot invalidate references to names.

  * •

_Will the Funcons-beta collection of funcons ever be finalised?_

Funcons-beta is a release candidate. After further polishing, review, and
experimental use, the collection of funcons and their documentation are to be
released for general use. However, it will always be possible to add new
funcons to the collection, to support new concepts, or to provide alternative
ways of expressing existing concepts.

##  4 Facets of Funcons

When funcon terms are executed, their behaviour may have many facets: apart
from computing results, funcon behaviour can involve name bindings, imperative
variables, abrupt termination, interaction, etc. Facets that are not needed
for a particular term can be ignored.

In this section, we introduce the main facets of the Funcons-beta collection.
Appendix 0.A provides an informal summary of the funcons; their definitions
are available online [23, Funcons-beta].

  * •

_How are funcon terms executed?_

Funcon terms compute values whenever their computations terminate normally. A
funcon takes a sequence of argument terms, and may compute a sequence of
values. Its signature specifies how many arguments it takes, the type of
values to be computed by each argument, and the types of the values that the
funcon computes. Individual arguments may be required to be pre-computed
values; the funcon definition specifies how its behaviour combines the
computations of any remaining arguments.

  * •

_Does each funcon take a fixed number of arguments?_

Not necessarily: a funcon signature can specify that an argument at some
position is optional, or that it can be a sequence. Sequence arguments are
often used to extend associative binary funcons to longer argument sequences.
They are also used for funcons that correspond directly to conventional
notation for (finite) lists and sets, e.g.,
${\color[rgb]{.545,0,0}\textsf{list}}(V_{1},\dots,V_{n})$ for
$[V_{1},\dots,V_{n}]$.

  * •

_How do funcons represent data?_

Data that programs process when executed is represented by funcon terms
classified as values. Some funcons are value constructors: they are inert, and
have no computational behaviour themselves. Values are classified as primitive
values, composite values, or abstractions.

Conceptually, primitive values are atomic, and not constructed from other
values. Booleans, numbers, characters, and a null value are all classified as
primitive. For large (or infinite) types of primitive values, however, it is
infeasible to declare a separate constructor for each value. So in practice,
funcons used to construct primitive values usually take other values as
arguments.

Composite values are constructed from finite sequences of argument values. The
types of composite values include parametrised algebraic data types, with a
generic representation. Various algebraic datatypes are defined, and new ones
can be introduced. Composite values include also built-in parametrised types
of sets, maps, multi-sets, and graphs.

Abstractions are values formed by a value constructor
${\color[rgb]{.545,0,0}\textsf{abstraction}}(X)$ with an unevaluated argument
$X$. Values are called ground when they are constructed entirely from
primitive and composite values, without abstractions.

Appendix 0.A.1.1 summarises the funcons for representing data.

  * •

_What kind of behaviour do funcons for data operations have?_

Data operations in programs are generally represented by funcons whose only
behaviour is to evaluate their arguments and compute a value. Partial data
operations (e.g., integer division, or selecting the head of a list) compute
the empty sequence when their arguments are not in their domain of definition.

Value types are themselves values, so funcons can take types as arguments and
give them as results. Apart from supporting dependent types, this generality
is needed to represent ordinary type constructors as funcons.

  * •

_How do funcons express flow of control?_

Funcons intended purely for specifying normal control flow generally determine
the order of execution of their arguments. They include sequential or
interleaved command execution and expression evaluation, deterministic and
non-deterministic choice between computations, and command iteration. These
funcons do not contribute otherwise to behaviour.

Funcons that represent data operations always evaluate all their arguments,
allowing interleaving.

Appendix 0.A.2 summarises the funcons for representing control flow.

  * •

_How do funcons express flow of data?_

A computation may involve multiple uses of the same data, e.g., so as to
assign it to a variable as well as provide it as a result. It may also involve
execution of the same computation with different data. The funcons for
specifying such data flow involve a ${\color[rgb]{.545,0,0}\textsf{given-
value}}(V)$ entity that can be set to a computed value $V$, and subsequently
referenced as given.

Appendix 0.A.3 summarises the funcons for representing data flow.

  * •

_How do funcons specify scopes of bindings?_

An occurrence of a name in a program either binds the name, or refers to
whatever is currently bound to the name. Binding occurrences are usually found
in declarations, parameter specifications, and patterns; references to names
are ubiquitous. Sequences of declarations have the effect of successively
extending (or perhaps overriding) the current bindings with the bindings due
to the individual declarations.

Funcons use conventional environments $\rho$ (mapping names to values) to
represent both the current bindings and the bindings computed by declarations.
The ${\color[rgb]{.545,0,0}\textsf{environment}}(\rho)$ entity represents the
current bindings, and the binding for an individual name $I$ can be inspected
using the funcon ${\color[rgb]{.545,0,0}\textsf{bound-value}}(I)$; the
environment representing the computed bindings is an ordinary composite value.

Some languages include various constructs for composing declarations, and
these are represented directly by funcons that compute environments. However,
the funcons corresponding to recursive declarations represent circularity by
creating cut-points called links, which involves a separate entity.

Appendix 0.A.4 summarises the funcons for representing name binding.

  * •

_Do funcons have static scopes for bindings?_

The difference between static and dynamic scopes concerns procedural
abstraction. A value that represents an abstraction is constructed from an
unevaluated argument $X$ by the funcon
${\color[rgb]{.545,0,0}\textsf{abstraction}}(X)$. The abstraction value can be
subsequently enacted, which evaluates the argument $X$ – potentially in a
different context from that where the abstraction value was constructed.

Constructed abstraction values thus naturally have dynamic scopes for
bindings. To obtain static scopes, the funcon
${\color[rgb]{.545,0,0}\textsf{closure}}(X)$ computes a closure value: an
abstraction whose argument evaluation starts by ignoring the current bindings
and restoring the abstraction-time bindings.

  * •

_How do funcons distinguish between constant and mutable variables?_

In programming languages, imperative variables usually have names. It may be
tempting to regard variable names as bound directly to values: bindings become
mutable, and assignment to a variable name updates its binding. Constants then
correspond to single-assignment variables. However, such a simplistic
conceptual analysis does not easily extend to concepts such as aliasing and
call by reference.

A more satisfactory conceptual basis for imperative variables is to regard
them as independent storage locations.666Funcons have not yet been developed
for ‘relaxed’ memory models or data marshalling. The declaration of a named
variable involves the allocation of storage (optionally with an initial value)
together with binding the name of the variable to the storage location.
Assignment to a named variable then affects what value is stored at the
location, but leaves the bindings unchanged. Aliasing can now be understood
simply as the simultaneous binding of different names to the same location.

The funcons for imperative variables involve a mutable
${\color[rgb]{.545,0,0}\textsf{store}}(\sigma)$ entity, mapping locations to
their current values. The store supports allocation (and recycling) of
locations for values of any type, and their initialisation, assignment, and
inspection. It is completely independent of the
${\color[rgb]{.545,0,0}\textsf{environment}}(\rho)$ entity used for name
bindings.

In mathematical logic, a ‘variable’ corresponds to a name, and ‘assignment’ to
binding. Imperative variables in programming languages are often called
‘L-values’, with ‘R-values’ being those that can be assigned to variables.777
‘L’ and ‘R’ refer to the left and right sides of typical assignment commands
[29]. With funcons, all values can be assigned to variables, including
variables themselves.

  * •

_Can funcons represent structured variables with mixtures of constant and
mutable fields?_

A simple variable consists of a location together with the type of values that
it can store; assignment checks that the value to be assigned to the variable
is in its type.888Funcons for using un-typed locations as variables would be
slightly simpler. Simple variables may store primitive values (e.g., numbers)
or composite values (e.g., tuples), but assignment to a simple variable is
always monolithic: the current value is replaced entirely by the new value.

Structured variables are composite values where some components are simple
variables. These include hybrids having both mutable and immutable components.
Assignment to a selected component variable corresponds to an in-place update;
assignment of a composite value to an entire structured variable updates all
the component simple variables with the matching values, and checks that the
immutable components are the same.

Appendix 0.A.5 summarises the funcons for representing imperative variables.

  * •

_How about abrupt termination?_

Various language constructs may cause abrupt termination when executed:
throwing/raising an exception, returning the value of a function, breaking out
of a loop, etc. Enclosing constructs can detect particular kinds of abrupt
termination, and handle them appropriately. For example, a language construct
may inspect an exception value, and conditionally handle it; a function
application handles an abruptly returned value by giving it as the result; and
a loop handles a break by terminating normally.

Funcons express abrupt termination and handlers uniformly. Abrupt termination
leads to a stuck term, emitting an
${\color[rgb]{.545,0,0}\textsf{abrupted}}(V)$ signal that carries a value $V$.
The closest enclosing funcon that notices the emission of such a signal can
inspect its value, and determine whether to handle it or not.

Appendix 0.A.6 summarises the funcons for representing data flow.

  * •

_Is it possible to express delimited control operators as funcons?_

Somewhat surprisingly, yes: see [27]. Funcons for expressing delimited control
operators are defined at [23, Funcons-beta/Computations/Abnormal/Controlling].

  * •

_Can non-terminating funcons have observable behaviour?_

In many languages, programs correspond to commands, rather than declarations
or expressions. Their behaviour may depend on, and affect, data stored in
files. Conceptually, files can be regarded as (complicated) structured
variables: input from a file inspects the value at its current position, and
advances the position; output to a file appends a value to it. Changes to a
file system during program execution correspond to updating values stored in
locations; they can be observed, but they may also be overwritten. Programming
languages typically relegate effects on files to library functions, and
corresponding funcons would not be directly relevant to analysis of language
constructs.

Interactive input and output, in contrast, cannot be regarded as effects on
mutable storage. Acceptance of input data from a stream during program
execution is irrevocable, as is output of data to a stream. Interaction may
also involve inter-dependence between input and output. And a program that
never terminates can have infinitely long streams of input and output.

Thus funcons for expressing communication involve kinds of entities that
differ fundamentally from those we previously introduced. The
${\color[rgb]{.545,0,0}\textsf{standard-in}}(V^{*})$ entity represents the
(finite) sequence of values input at each step of a computation, where the
empty sequence $(\ )$ represents that no values are input. The value null-
value indicates the end of the input. The
${\color[rgb]{.545,0,0}\textsf{standard-out}}(V^{*})$ entity represents the
(finite) sequence of values output at a particular step, where the empty
sequence $(\ )$ represents the lack of output. Computations concatenate the
input sequences of each step, and similarly for output, potentially resulting
in infinite sequences for non-terminating computations. To support multiple
streams, further entities and funcons would need to be added.

Appendix 0.A.7 summarises the funcons for representing interaction.

  * •

_Do funcons currently support specification of any other language features?_

Tentative funcons for multithreading have been developed. They have not yet
been rigorously unit-tested, nor used much in language definitions. These
funcons are not included in Funcons-beta, but in an unstable collection that
extends Funcons-beta [23, Unstable-Funcons-beta].

The multithreading funcons involve multiple mutable entities, representing the
collection of threads, the set of active threads, the thread being executed,
the values computed by terminated threads, and (abstract) scheduling
information. Funcons that combine effects on multiple entities are
undesirable, and their definitions are quite verbose. It is currently unclear
whether simpler funcons for multithreading can be developed.

Multithreading also involves synchronisation. The funcons for synchronising
involve only the store entity. To inhibit preemption during synchronisation,
multiple assignments need to be executed atomically, in a single transition.

Funcons for distributed processes have not yet been developed. They are
expected to be based on asynchronous execution and message passing.

Funcons for specifying meta-programming constructs have been defined [1]; they
also enable a straightforward specification of call-by-need parameter-passing.

##  5 Translation of Language Constructs to Funcons

In this section, we illustrate how a simple programming language construct can
be analysed by translation to funcons. Specifying such a translation for all
constructs of a language defines a semantics for the language, based on the
semantics of the funcons used in the translation. The PLanCompS project has
developed some examples [23, Languages-beta] and made them available for
browsing on a website. We conclude this section with an overview of the
examples, and indicate how they have been developed and tested.

  * •

_How is call-by-value translated to funcons?_

The following language specification fragments illustrate how call-by-value
parameter passing in an imperative programming language can be analysed by
translation to funcons. The fragments originate from the complete
specification of the SIMPLE language [23, Languages-beta/SIMPLE]; for brevity,
we restrict functions here to a single parameter.

The translation specification in Fig. 1 declares exp as a phrase sort, with
the meta-variable Exp (possibly with subscripts and/or primes) ranging over
phrases of that sort. The BNF-like production shows two language constructs of
sort exp: an identifier of sort id (lexical tokens, here assumed to be
specified elsewhere with meta-variable Id) and a function application written
‘${\color[rgb]{0,0,0}\textit{Exp}}_{1}\texttt{(}{\color[rgb]{0,0,0}\textit{Exp}}_{2}\texttt{)}$’.

$\displaystyle\textsf{{{\color[rgb]{.752,.752,.752}Syntax}}}\quad{\color[rgb]{0,0,0}\textit{Exp}}:{\color[rgb]{.18,.545,.34}\textsf{exp}}::=\cdots\mid{\color[rgb]{.18,.545,.34}\textsf{id}}\mid{\color[rgb]{.18,.545,.34}\textsf{exp}}\
\textsf{{\color[rgb]{.752,.752,.752}`}{(}{\color[rgb]{.752,.752,.752}'}}\
{\color[rgb]{.18,.545,.34}\textsf{exp}}\
\textsf{{\color[rgb]{.752,.752,.752}`}{)}{\color[rgb]{.752,.752,.752}'}}\mid\cdots$

Semantics $\displaystyle{\color[rgb]{0,0,.545}\textsf{rval}}\llbracket\
\\_:{\color[rgb]{.18,.545,.34}\textsf{exp}}\
\rrbracket:\mathop{\Rightarrow}{\color[rgb]{.545,0,0}\textsf{values}}$ Rule
$\displaystyle{\color[rgb]{0,0,.545}\textsf{rval}}\llbracket\
{\color[rgb]{0,0,0}\textit{Id}}\
\rrbracket={\color[rgb]{.545,0,0}\textsf{assigned-
value}}({\color[rgb]{.545,0,0}\textsf{bound-
value}}({\color[rgb]{0,0,.545}\textsf{id}}\llbracket\
{\color[rgb]{0,0,0}\textit{Id}}\ \rrbracket))$ Rule
$\displaystyle{\color[rgb]{0,0,.545}\textsf{rval}}\llbracket\
{\color[rgb]{0,0,0}\textit{Exp}}_{1}\
\textsf{{\color[rgb]{.752,.752,.752}`}{(}{\color[rgb]{.752,.752,.752}'}}\
{\color[rgb]{0,0,0}\textit{Exp}}_{2}\
\textsf{{\color[rgb]{.752,.752,.752}`}{)}{\color[rgb]{.752,.752,.752}'}}\
\rrbracket={\color[rgb]{.545,0,0}\textsf{apply}}({\color[rgb]{0,0,.545}\textsf{rval}}\llbracket\
{\color[rgb]{0,0,0}\textit{Exp}}_{1}\
\rrbracket,{\color[rgb]{0,0,.545}\textsf{rval}}\llbracket\
{\color[rgb]{0,0,0}\textit{Exp}}_{2}\ \rrbracket)$

Figure 1: Translation of identifiers and function applications in SIMPLE to
funcons

The translation function rval maps exp phrases to funcon terms that compute
elements of type values. Translation is compositional: the funcon term for a
phrase combines the translations of its sub-phrases. We assume the translation
function id maps lexical tokens of sort id to funcon values of type
identifiers.

In this illustrative language, the only values that can be bound to
identifiers are simple imperative variables. For languages where identifiers
can be bound directly to other values, we would use current-value instead of
assigned-value.

For call-by-value parameters in an imperative language, the argument value can
be passed to the called function, which then has to allocate a variable to
store the value. For call-by-reference, the argument would have to evaluate to
a variable; for call-by-name, the evaluation of the argument would be
deferred, which can be expressed constructing a thunk abstraction value from
it. When the mode of parameter-passing in function applications depends on the
function, argument evaluation needs to be incorporated in the value that
represents the function.

The translation specification for function declarations in Fig. 2 assumes a
translation function exec for phrases Block of sort block. A block is a
command, which normally computes a null value; but, as in many languages, a
block can return an expression value by executing a return statement, which
terminates the execution of the block abruptly.

$\displaystyle\textsf{{{\color[rgb]{.752,.752,.752}Syntax}}}\quad{\color[rgb]{0,0,0}\textit{Decl}}:{\color[rgb]{.18,.545,.34}\textsf{decl}}::=\cdots\mid\textsf{{\color[rgb]{.752,.752,.752}`}{function}{\color[rgb]{.752,.752,.752}'}}\
{\color[rgb]{.18,.545,.34}\textsf{id}}\
\textsf{{\color[rgb]{.752,.752,.752}`}{(}{\color[rgb]{.752,.752,.752}'}}\
{\color[rgb]{.18,.545,.34}\textsf{id}}\
\textsf{{\color[rgb]{.752,.752,.752}`}{)}{\color[rgb]{.752,.752,.752}'}}\
{\color[rgb]{.18,.545,.34}\textsf{block}}$

Semantics $\displaystyle{\color[rgb]{0,0,.545}\textsf{declare}}\llbracket\
\\_:{\color[rgb]{.18,.545,.34}\textsf{decl}}\
\rrbracket:\mathop{\Rightarrow}{\color[rgb]{.545,0,0}\textsf{environments}}$
Rule $\displaystyle{\color[rgb]{0,0,.545}\textsf{declare}}\llbracket\
\textsf{{\color[rgb]{.752,.752,.752}`}{function}{\color[rgb]{.752,.752,.752}'}}\
{\color[rgb]{0,0,0}\textit{Id}}_{1}\
\textsf{{\color[rgb]{.752,.752,.752}`}{(}{\color[rgb]{.752,.752,.752}'}}\
{\color[rgb]{0,0,0}\textit{Id}}_{2}\
\textsf{{\color[rgb]{.752,.752,.752}`}{)}{\color[rgb]{.752,.752,.752}'}}\
{\color[rgb]{0,0,0}\textit{Block}}\ \rrbracket=$
$\displaystyle\quad{\color[rgb]{.545,0,0}\textsf{bind-
value}}({\color[rgb]{0,0,.545}\textsf{id}}\llbracket\
{\color[rgb]{0,0,0}\textit{Id}}_{1}\ \rrbracket,$
$\displaystyle\quad\quad{\color[rgb]{.545,0,0}\textsf{allocate-initialised-
variable}}({\color[rgb]{.545,0,0}\textsf{functions}}({\color[rgb]{.545,0,0}\textsf{values}},{\color[rgb]{.545,0,0}\textsf{values}}),$
$\displaystyle\quad\quad\quad{\color[rgb]{.545,0,0}\textsf{function}}({\color[rgb]{.545,0,0}\textsf{closure}}($
$\displaystyle\quad\quad\quad\quad{\color[rgb]{.545,0,0}\textsf{scope}}($
$\displaystyle\quad\quad\quad\quad\quad{\color[rgb]{.545,0,0}\textsf{bind-
value}}({\color[rgb]{0,0,.545}\textsf{id}}\llbracket\
{\color[rgb]{0,0,0}\textit{Id}}_{2}\ \rrbracket,$
$\displaystyle\quad\quad\quad\quad\quad\quad{\color[rgb]{.545,0,0}\textsf{allocate-
initialised-
variable}}({\color[rgb]{.545,0,0}\textsf{values}},{\color[rgb]{.545,0,0}\textsf{given}})),$
$\displaystyle\quad\quad\quad\quad\quad{\color[rgb]{.545,0,0}\textsf{handle-
return}}({\color[rgb]{0,0,.545}\textsf{exec}}\llbracket\
{\color[rgb]{0,0,0}\textit{Block}}\ \rrbracket))))))$

Figure 2: Translation of function declarations in SIMPLE to funcons

The use of closure ensures static (lexical) bindings for references to names
in the function body. To change to dynamic bindings, we would replace closure
by abstraction. The construction of a function value from the closure is
needed so that apply can be used to give the argument value to the body of the
abstraction.

The scope funcon adds the bindings computed by its first argument to the
current bindings for the execution of its second argument. In this simplified
illustration, functions have only one formal parameter, which is bound to a
freshly allocated variable containing the given argument value; for multiple
parameters, the given value would be a tuple of the same length, matched by a
pattern tuple.

The handle-return funcon concisely handles abrupt termination of the function
body arising from execution of the return funcon. It has no effect on normal
termination, nor on abrupt termination for other reasons.

In languages where function identifiers can be bound directly to function
closures, the first allocate-initialised-variable in the translation rule
could be eliminated. However, the possibility of recursive function calls
would then need to be expressed directly, using the recursive funcon.

The call-by-value example illustrates how directly the behaviour of a language
construct can be specified by translation to funcons.

  * •

_Which other language constructs have been translated to funcons?_

The PLanCompS project has developed the following funcon-based language
specifications and made them available for browsing online [23, Languages-
beta].

IMP:

a very small imperative language. Its funcon-based specification illustrates
only the basic features of the framework.

SIMPLE:

a somewhat larger imperative language than IMP. Its funcon-based specification
illustrates many features of the framework, but omits language constructs for
process spawning, synchronisation, and locks.

MiniJava:

a very simple subset of Java. Its specification illustrates the use of funcons
for classes and objects.

SL:

a dynamic language. Its specification illustrates how dynamic bindings can be
translated to funcons.

OCaml Light:

a core sublanguage of OCaml, corresponding closely to Caml Light. Its
specification illustrates scaling up to a medium-sized language.

Further examples of funcon-based language specifications have been developed,
but not sufficiently tested [23, Unstable-Languages-beta]:

IMP++:

extends IMP with multithreading and other features.

SIMPLE-Threads:

adds the previously-omitted concurrency constructs.

LangDev-2019:

demonstrates extensibility of language specifications.

A funcon-based specification of C$\sharp$ has yet to be completed.

  * •

_How can we check translations of language constructs to funcons?_

Consider our translation of function declarations with call-by-value
parameters. Potential mistakes include spelling errors in names (primarily
funcons, but also syntax sorts, translation functions, and meta-variables) and
misplaced parentheses. The syntax of the language construct in the translation
rule might not be consistent with the specified grammar. A less obvious
mistake is when the arguments of a funcon could compute values that are not in
the types required by the funcon signature. We might also have used a funcon
that does not have the intended behaviour (e.g., using abstraction instead of
closure).

Clearly, tool support for checking is essential. A workbench for specifying
translations of languages to funcons is being developed [18]. Tools for
executing funcon terms [3] allow us to check whether they have the expected
behaviour.

The workbench checks references to names, term formation, and the syntax in
translation rules. It checks that funcons have the right number of arguments,
but not that the arguments compute values of the required types; we rely on
testing to check for that.

The workbench also supports parsing complete programs and translating them to
funcon terms, using parsers and translators generated from the specified
grammar and translation rules. It is based on the Spoofax language workbench
[9], and implemented using the declarative domain-specific meta-languages
SDF3, NaBL2, and Stratego. See [18] for further details. The tools for
executing funcon terms [3] are implemented in Haskell, and can be called
directly from the workbench.

##  6 Defining and Implementing Funcons

In this section, we illustrate how to define the behaviour of a funcon, once
and for all, using a modular variant [16, 20] of structural operational
semantics [24].

  * •

_How are funcons defined?_

The funcon signature in Fig. 3 specifies that scope takes two arguments. The
first argument is required to be pre-evaluated to a value of type
environments; the second argument should be unevaluated. Values computed by
${\color[rgb]{.545,0,0}\textsf{scope}}(\rho_{1},X)$ are to have the same type
($T$) as the values computed by $X$.

Funcon
$\displaystyle{\color[rgb]{.545,0,0}\textsf{scope}}(\\_:{\color[rgb]{.545,0,0}\textsf{environments}},\\_:\mathop{\Rightarrow}T):\mathop{\Rightarrow}T$
Rule $\displaystyle\frac{\begin{aligned}
{\color[rgb]{.545,0,0}\textsf{environment}}({\color[rgb]{.545,0,0}\textsf{map-
override}}(\rho_{1},\rho_{0}))\vdash X\longrightarrow
X^{\prime}\end{aligned}}{\begin{aligned}
{\color[rgb]{.545,0,0}\textsf{environment}}(\rho_{0})\vdash{\color[rgb]{.545,0,0}\textsf{scope}}(\rho_{1}:{\color[rgb]{.545,0,0}\textsf{environments}},X)\longrightarrow{\color[rgb]{.545,0,0}\textsf{scope}}(\rho_{1},X^{\prime})\end{aligned}}$
Rule
$\displaystyle{\color[rgb]{.545,0,0}\textsf{scope}}(\\_:{\color[rgb]{.545,0,0}\textsf{environments}},V:T)\leadsto
V$ Figure 3: Definition of the funcon for expressing scopes of local
declrations

The rules define how execution of
${\color[rgb]{.545,0,0}\textsf{scope}}(\rho_{1},X)$ can proceed when the
current bindings are represented by $\rho_{0}$. The premise of the first rule
holds if $X$ can make a transition to $X^{\prime}$ when $\rho_{1}$ overrides
the current bindings $\rho_{0}$. Whether $X^{\prime}$ is a computed value or
an intermediate term is irrelevant. When the premise holds, the conclusion is
that ${\color[rgb]{.545,0,0}\textsf{scope}}(\rho_{1},X)$ can make a transition
to ${\color[rgb]{.545,0,0}\textsf{scope}}(\rho_{1},X^{\prime})$.

If $X$ can terminate abruptly, or continue making transitions forever, then
${\color[rgb]{.545,0,0}\textsf{scope}}(\rho_{1},X)$ can do the same. The last
rule allows execution of ${\color[rgb]{.545,0,0}\textsf{scope}}(\rho_{1},V)$
to terminate when $V$ is a value. Transitions written with ‘$\leadsto$’
correspond to term rewriting [5], and never depend on entities such as the
current environment.

  * •

_How can funcon definitions remain fixed when new funcons are added?_

The use of the entity ${\color[rgb]{.545,0,0}\textsf{environment}}(\rho_{0})$
in the definition of scope restricts transitions to states that include it,
but states might still include other entities, such as
${\color[rgb]{.545,0,0}\textsf{store}}(\sigma)$ or
${\color[rgb]{.545,0,0}\textsf{given-value}}(V)$. If a transition
$X\longrightarrow X^{\prime}$ updates $\sigma$ to $\sigma^{\prime}$, so does
the transition
${\color[rgb]{.545,0,0}\textsf{scope}}(\rho_{1},X)\longrightarrow{\color[rgb]{.545,0,0}\textsf{scope}}(\rho_{1},X^{\prime})$;
the transitions in the premise and conclusion are given the same value $V$;
and if $X\longrightarrow X^{\prime}$ emits a signal on abrupt termination, so
does the corresponding transition for
${\color[rgb]{.545,0,0}\textsf{scope}}(\rho_{1},X)$.

Entities used in transitions are classified according to how they flow during
program execution:

Contextual:

A contextual entity remains fixed for successive steps in the computation of a
term, but can be different for the computations of sub-terms.

Mutable:

Changes to a mutable entity are threaded sequentially through the computation
of a term and its sub-terms.

Input:

An input entity is a sequence of values, and the sequences input by successive
steps are independent.

Output:

An output entity is a sequence of values, and the sequences output by
successive steps are independent.

Control:

A control entity is a value that can optionally be signalled by a step. The
corresponding step of an enclosing term may inspect the value, and signal the
same value, signal a different value, or not signal.

The notation used for entities in transitions determines their classification.

  * •

_Can static semantics for funcons be defined in the same way as dynamic
semantics?_

The modular structural operational semantics rules for funcon execution are in
the small-step style, where each rule has at most one transition premise. A
static semantics for funcons would naturally use big-step rules, with a
premise for each sub-term. It is currently unclear whether the same
classification of entities can be used for static and dynamic semantics; the
static semantics of abstractions generally requires making latent effects
explicit, in contrast to dynamic semantics.

  * •

_How have funcons been implemented?_

The initial implementation of funcons was in Prolog. Funcon definitions were
translated to Prolog clauses defining
transitions,999https://pdmosses.github.io/prolog-msos-tool based on the
original implementation of MSOS in
Prolog.101010https://pdmosses.github.io/msos-in-prolog Funcons have also been
implemented in Maude.111111https://github.com/fcbr/mmt The Prolog
implementation of MSOS was subsequently enhanced to support the rewriting
relation used in value-computation transition systems [5]. The Funcon Tools
package [3] supports parsing funcon definitions and generating a funcon
interpreter in Haskell, as described in [2].

  * •

_Could funcons be used for language specification in other frameworks?_

The K-framework [25] has a high degree of modularity. For an experiment with
using the K-framework to define funcons, see [21]. The distinction between
pre-evaluated and unevaluated arguments in funcon signatures is represented by
strictness annotations in K. However, rules in K are unconditional, so funcons
such as scope cannot be defined straightforwardly. The specification of the
structure of states is monolithic, and may need updating when adding new
funcons.

Redex [10] is a popular domain-specific metalanguage for operational
semantics, embedded in the Racket programming language. It is based on
reduction rules and evaluation contexts. The reduction rules are highly
modular, and grammars for language constructs and evaluation contexts can be
specified incrementally. However, evaluation context grammars associated with
control operators appear to be inherently global. It should be possible to
define a particular collection of funcons in Redex, but not independently:
adding a new funcon would generally require updating the evaluation contexts
for existing funcons.

##  7 Related Work

Many funcons are closely related to notation used in several previously
developed language specification frameworks: denotational semantics, monads,
abstract semantic algebras, and action semantics.

##### Denotational Semantics.

The funcons for flowing, binding, and storing are directly based on
Christopher Strachey’s original conceptual analysis of imperative programming
languages. Strachey initiated the development of denotational semantics at the
IFIP Working Conference on Formal Language Description Languages in 1964 [28].
At the time, he was working on the design and implementation of the high-level
CPL programming language, and aiming to specify its semantics formally. In the
paper, he focuses on representing imperative features of programming languages
as pure mathematical functions, avoiding the introduction of abstract
machines. For assignment commands, he distinguishes between L-values and
R-values of expressions, with locations in stores $\sigma$ being a special
case of L-values. He defines the operation $C$ to get the current content of a
location, and $U$ to update the content. For flow of control, he uses
composition of functions from stores to stores, and the fixed-point operation
$Y$. In his widely-circulated 1967 lecture notes [29], he also introduces
environments that map names to values, and represents procedures as closures.

Strachey’s original operation $C$ on stores is renamed Contents in [26], and
$U$ is renamed Assign. Many subsequent denotational specifications define a
large number of such auxiliary operations (e.g., [13] defines about 80).
However, the definitions are ad hoc, and they are based on the domains defined
for the specified language. Even the way lambda-expressions are written, and
the notation used for modifying environments and stores, vary between
denotational specifications. The VDM metalanguage for denotational semantics,
developed from 1974 [8], introduced fixed notation for operations expressing
basic mathematical and computational concepts. The notation for data flow,
control flow, storing, and exception handling looks rather like a programming
language, but it is intepreted as pure mathematical functions (the
interpretation depends on whether exceptions are used).

##### Monads.

The types of the mathematical functions used in denotational semantics can be
quite complicated. In 1989, Eugenio Moggi suggested that each feature should
be seen as a monad, where the elements represent computations of values in
arbitrary domains [12]; moreover, the required domains could be defined
modularly, by applying a series of monad constructors. Monads have a binary
operation for composing a computation with a function that takes its computed
value,121212See [17] for discussion of earlier uses of similar operations in
denotational semantics. corresponding to the funcon
${\color[rgb]{.545,0,0}\textsf{give}}(X,Y)$, and a unary operation for giving
a value as the result of a computation (not needed with funcons). Each monad
constructor adds further structure to the domain of computations, together
with associated operations. For example, the monad constructor for stores in a
domain $S$ makes computations of values in $T$ take an argument in $S$ and
return both a value in $T$ and a store in $S$. The associated operations are
$\textit{lookup}(l)$, to return the value at location $l$ in the argument
store and the unchanged store, and $\textit{update}(l,v)$, to return a null
value and a store where the value at $l$ is $v$. The funcons
${\color[rgb]{.545,0,0}\textsf{assigned}}({\color[rgb]{0,0,0}\textit{Var}})$
and
${\color[rgb]{.545,0,0}\textsf{assign}}({\color[rgb]{0,0,0}\textit{Var}},V)$
correspond to (a typed variant of) the operations defined by the store monad
constructor. Other funcons correspond closely to the operations associated
with monad constructors for a wide range of notions of computation. Monad
constructors also need to lift definitions of operations to the resulting
domains, which is non-trivial. Notation for monad constructors and operations
varies (also between the various functional programming languages and proof
assistants that support monads).

##### Abstract Semantic Algebras and Action Semantics.

In a series of papers in the 1980s, the present author proposed various sets
of combinators, together with algebraic laws that they were supposed to obey,
giving so-called _abstract semantic algebras_. The elements of abstract
semantic algebras were intended to have a clear operational interpretation;
they were referred to as ‘actions’ from 1985.

The action notation used in the action semantics framework [14, 15] was
developed in collaboration with David Watt [22]. It was defined [14, App. C]
using a novel (but non-modular) variant of structural operational semantics,
and use of action semantics was supported by tools implemented in the ASF+SDF
Meta-Environment [4, 7].

Action notation involves actions, data, and yielders. The performance of an
action represents information processing behaviour. Yielders used in actions
may access, but not change, the current information. The evaluation of a
yielder always results in a data entity. Many funcons correspond closely to
the combinators of action notation. The crucial difference is that action
notation could not be extended with new features, due to the non-modularity of
its operational definition. The development of modular structural operational
semantics [16] was directly motivated by the aim of making the definition of
action notation extensible, and avoiding reduction of the many facets of
action behaviour to pure functions in monads [31].

##  8 Conclusion

The PLanCompS project has defined the behaviour of a substantial collection of
funcons, and illustrated translation of functional and imperative language
constructs to funcons [23]. It has also developed their theoretical
foundations [5] Specifying language semantics by translation to funcons
appears to be significantly less effort than with other frameworks. Funcon
definitions and translations have been validated by testing using generated
interpreters; web pages and PDFs are generated from the same source files,
with hyperlinks from names to definitions to support browsing and navigation.

Much remains to be done. Current and future work includes: completion and
release of the CBS IDE and the initial collection of funcons; demonstration of
scaling up to translation of a major language such as C$\sharp$; improvement
of the definitions of funcons for multithreading; defining the static
semantics of funcons; defining funcons for expressing static semantics of
language constructs; proving algebraic laws for funcons; and investigating
whether funcons can be used also for specifying the semantics of declarative
and domain-specific programming languages The PLanCompS project welcomes new
participants!

####  8.0.1 Acknowledgements

The author is grateful to colleagues for helpful comments and suggestions for
improvement on a previous draft. The initial development of funcons was
supported by EPSRC grant (EP/I032495/1) to Swansea University for the
PLanCompS project. The author is currently a visitor at TU Delft.

## References

  * [1] van Binsbergen, L.T.: Funcons for HGMP: the fundamental constructs of homogeneous generative meta-programming (short paper). In: Wyk, E.V., Rompf, T. (eds.) GPCE 2018. pp. 168–174. ACM (2018). https://doi.org/10.1145/3278122.3278132
  * [2] van Binsbergen, L.T., Mosses, P.D., Sculthorpe, N.: Executable component-based semantics. J. Log. Algebr. Meth. Program. 103, 184–212 (2019). https://doi.org/10.1016/j.jlamp.2018.12.004
  * [3] van Binsbergen, L.T., Sculthorpe, N.: funcons-tools: A modular interpreter for executing funcons, https://hackage.haskell.org/package/funcons-tools, Hackage package, accessed 2021-06-02
  * [4] van den Brand, M., Iversen, J., Mosses, P.D.: An action environment. Sci. Comput. Program. 61(3), 245–264 (2006). https://doi.org/10.1016/j.scico.2006.04.005
  * [5] Churchill, M., Mosses, P.D.: Modular bisimulation theory for computations and values. In: Pfenning, F. (ed.) FOSSACS 2013. LNCS, vol. 7794, pp. 97–112. Springer (2013). https://doi.org/10.1007/978-3-642-37075-5
  * [6] Churchill, M., Mosses, P.D., Sculthorpe, N., Torrini, P.: Reusable components of semantic specifications. LNCS Trans. Aspect Oriented Softw. Dev. 12, 132–179 (2015). https://doi.org/10.1007/978-3-662-46734-3_4
  * [7] van Deursen, A., Mosses, P.D.: ASD: the action semantic description tools. In: Wirsing, M., Nivat, M. (eds.) AMAST ’96. LNCS, vol. 1101, pp. 579–582. Springer (1996). https://doi.org/10.1007/BFb0014346
  * [8] Jones, C.B.: The transition from VDL to VDM. J. Univers. Comput. Sci. 7(8), 631–640 (2001). https://doi.org/10.3217/jucs-007-08-0631
  * [9] Kats, L.C.L., Visser, E.: The Spoofax language workbench: Rules for declarative specification of languages and IDEs. In: Cook, W.R., Clarke, S., Rinard, M.C. (eds.) OOPSLA 2010. p. 444–463. ACM (2010). https://doi.org/10.1145/1869459.1869497
  * [10] Klein, C., Clements, J., Dimoulas, C., Eastlund, C., Felleisen, M., Flatt, M., McCarthy, J.A., Rafkind, J., Tobin-Hochstadt, S., Findler, R.B.: Run your research: on the effectiveness of lightweight mechanization. In: Field, J., Hicks, M. (eds.) POPL 2012. pp. 285–296. ACM (2012). https://doi.org/10.1145/2103656.2103691
  * [11] Madlener, K., Smetsers, S., van Eekelen, M.C.J.D.: Formal component-based semantics. In: Reniers, M.A., Sobocinski, P. (eds.) SOS 2011. EPTCS, vol. 62, pp. 17–29 (2011). https://doi.org/10.4204/EPTCS.62.2
  * [12] Moggi, E.: An abstract view of programming languages. Tech. Rep. ECS-LFCS-90-113, Edinburgh Univ. (1989)
  * [13] Mosses, P.D.: The mathematical semantics of Algol 60. Tech. Mono. PRG-12, Oxford Univ. Comp. Lab. (1974)
  * [14] Mosses, P.D.: Action semantics, Cambridge Tracts in TCS, vol. 26. Cambridge Univ. Press (1992). https://doi.org/10.1017/CBO9780511569869
  * [15] Mosses, P.D.: Theory and practice of action semantics. In: Penczek, W., Szalas, A. (eds.) MFCS’96. LNCS, vol. 1113, pp. 37–61. Springer (1996). https://doi.org/10.1007/3-540-61550-4_139
  * [16] Mosses, P.D.: Modular structural operational semantics. J. Log. Algebr. Program. 60-61, 195–228 (2004). https://doi.org/10.1016/j.jlap.2004.03.008
  * [17] Mosses, P.D.: VDM semantics of programming languages: combinators and monads. Formal Aspects Comput. 23(2), 221–238 (2011). https://doi.org/10.1007/s00165-009-0145-4
  * [18] Mosses, P.D.: A component-based formal language workbench. In: Monahan, R., Prevosto, V., Proença, J. (eds.) F-IDE@FM. EPTCS, vol. 310, pp. 29–34 (2019). https://doi.org/10.4204/EPTCS.310.4
  * [19] Mosses, P.D.: Software meta-language engineering and CBS. J. Comput. Lang. 50, 39–48 (2019). https://doi.org/10.1016/j.jvlc.2018.11.003
  * [20] Mosses, P.D., New, M.J.: Implicit propagation in structural operational semantics. ENTCS 229(4), 49–66 (2009). https://doi.org/10.1016/j.entcs.2009.07.073
  * [21] Mosses, P.D., Vesely, F.: FunKons: Component-based semantics in K. In: Escobar, S. (ed.) WRLA 2014. LNCS, vol. 8663, pp. 213–229. Springer (2014). https://doi.org/10.1007/978-3-319-12904-4_12
  * [22] Mosses, P.D., Watt, D.A.: The use of action semantics. In: Wirsing, M. (ed.) Formal Description of Programming Concepts III. pp. 135–166. North-Holland (1987)
  * [23] PLanCompS Project: CBS: A framework for component-based specification of programming languages, https://plancomps.github.io/CBS-beta, accessed 2021-06-02
  * [24] Plotkin, G.D.: A structural approach to operational semantics. J. Log. Algebr. Program. 60-61, 17–139 (2004). https://doi.org/10.1016/j.jlap.2004.05.001
  * [25] Rosu, G.: K: A semantic framework for programming languages and formal analysis tools. In: Pretschner, A., Peled, D., Hutzelmann, T. (eds.) Dependable Software Systems Engineering, pp. 186–206. IOS Press (2017). https://doi.org/10.3233/978-1-61499-810-5-186
  * [26] Scott, D.S., Strachey, C.: Toward a mathematical semantics for computer languages. In: Fox, J. (ed.) Proc. Symp. on Computers and Automata. Microwave Research Inst. Symposia, vol. 21, pp. 19–46. Polytechnic Inst. of Brooklyn (1971), also Tech. Mono. PRG-6, Oxford Univ. Comput. Lab
  * [27] Sculthorpe, N., Torrini, P., Mosses, P.D.: A modular structural operational semantics for delimited continuations. In: Danvy, O., de’Liguoro, U. (eds.) WoC 2016. EPTCS, vol. 212, pp. 63–80 (2015). https://doi.org/10.4204/EPTCS.212.5
  * [28] Strachey, C.: Towards a formal semantics. In: Formal Language Description Languages for Computer Programming. p. 198–216. North-Holland (1966)
  * [29] Strachey, C.S.: Fundamental concepts in programming languages. High. Order Symb. Comput. 13(1/2), 11–49 (2000). https://doi.org/10.1023/A:1010000313106, lecture notes, Int. Summer School in Comput. Prog., Copenhagen, 1967
  * [30] Torrini, P., Schrijvers, T.: Reasoning about modular datatypes with Mendler induction. In: Matthes, R., Mio, M. (eds.) FICS 2015. EPTCS, vol. 191, pp. 143–157 (2015). https://doi.org/10.4204/EPTCS.191.13
  * [31] Wansbrough, K., Hamer, J.: A modular monadic action semantics. In: Ramming, C. (ed.) DSL’97. USENIX (1997), http://www.usenix.org/publications/library/proceedings/dsl97/wansbrough.html

##  Appendix 0.A Funcons-beta Summary

This appendix is intended for inclusion only in the extended version of the
paper.

###  0.A.1 Data

####  0.A.1.1 Datatypes.

##### Primitive values.

Conceptually, primitive values are atomic, and not formed from other values.
For large (or infinite) types of primitive values, however, it is infeasible
to declare a separate constant for each value. So in practice, funcons used to
construct primitive values usually take other values as arguments.

  * •

booleans are the values true, false, and funcons corresponding to the usual
Boolean operations are defined.

  * •

integers is the built-in type of unbounded integers, with funcons for the
usual mathematical operations. Funcons corresponding to associative binary
operations are extended to arbitrary numbers of arguments. Subtypes include
naturals and ${\color[rgb]{.545,0,0}\textsf{bounded}}(M,N)$; compositions with
casts to such subtypes correspond to partial operations representing computer
arithmetic.

  * •

floats is the built-in type of IEEE floating point numbers.

  * •

characters is the built-in type of all Unicode characters. Its subtypes
include ascii-characters and iso-latin-1-characters. The UTF-8, UTF-16, and
UTF-32 encodings of characters as byte sequences are provided.

  * •

null-type has the single value null-value, alias null.

##### Composite values.

Conceptually, composite values are constructed from finite sequences of
argument values. The types of composite values include parametrised algebraic
data types, with a generic representation. Various algebraic datatypes are
defined, and new ones can be introduced. Composite values include also built-
in parametrised types of sets, maps, multi-sets, and graphs.

Algebraic datatypes:

  * •

datatype-values are generic representations for all algebraic datatype values.

  * •

${\color[rgb]{.545,0,0}\textsf{tuples}}(T_{1},\cdots,T_{n})$ are grouped
sequences of values with the specified types.

  * •

${\color[rgb]{.545,0,0}\textsf{lists}}(T)$ are grouped sequences of values
with the same type, with the usual operations; strings are lists of
characters.

  * •

${\color[rgb]{.545,0,0}\textsf{vectors}}(T)$ are grouped sequences of values
with the same type.

  * •

${\color[rgb]{.545,0,0}\textsf{trees}}(T)$ are finitely branching, with values
of type $T$ at nodes and leaves.

  * •

${\color[rgb]{.545,0,0}\textsf{references}}(T)$ are values that represent
values of type $T$. ${\color[rgb]{.545,0,0}\textsf{pointers}}(T)$ are
references or a single null value.

  * •

${\color[rgb]{.545,0,0}\textsf{records}}(T)$ are unordered aggregate values,
indexed by identifiers.

  * •

${\color[rgb]{.545,0,0}\textsf{variants}}(T)$, are pairs of identifiers and
values of type $T$.

  * •

classes are collections of features, allowing multiple superclasses, used to
create objects.

  * •

objects are classified collections of features.

  * •

${\color[rgb]{.545,0,0}\textsf{bit-vectors}}(N)$ has instantiations for bits
and bytes.

Built-in datatypes:

  * •

${\color[rgb]{.545,0,0}\textsf{sets}}(GT)$ are finite sets of ground values.

  * •

${\color[rgb]{.545,0,0}\textsf{maps}}(GT,T^{?})$ are finite maps from values
of type GT to values of type $T^{?}$.

  * •

${\color[rgb]{.545,0,0}\textsf{multisets}}(GT)$ are finite multisets of ground
values.

  * •

${\color[rgb]{.545,0,0}\textsf{directed-graphs}}(GT)$ have ground values as
vertices.

See [23, Funcons-beta/Values] for funcons on the above types.

####  0.A.1.2 Abstractions.

##### Generic Abstractions.

These values are used in thunks, functions, and patterns.

  * •

${\color[rgb]{.545,0,0}\textsf{abstractions}}(CT)$ are procedural abstractions
of computation type $CT$.

  * •

${\color[rgb]{.545,0,0}\textsf{abstraction}}(X)$ constructs values from terms
with dynamic bindings.

  * •

${\color[rgb]{.545,0,0}\textsf{closure}}(X)$ computes closed abstractions from
terms with static bindings.

  * •

${\color[rgb]{.545,0,0}\textsf{enact}}(A)$ evaluates the terms of abstractions
$A$.

##### Thunks.

The abstractions of thunks do not reference a given value.

  * •

${\color[rgb]{.545,0,0}\textsf{thunks}}(T)$ are constructed from abstractions
with bodies of type $(\ )\mathop{\Rightarrow}T^{\prime}$.

  * •

${\color[rgb]{.545,0,0}\textsf{force}}(V)$ enacts the abstraction of the thunk
$V$.

##### Functions.

The abstractions of functions reference a given value.

  * •

${\color[rgb]{.545,0,0}\textsf{functions}}(T,T^{\prime})$ are constructed from
abstractions with bodies of type $T\mathop{\Rightarrow}T^{\prime}$.

  * •

${\color[rgb]{.545,0,0}\textsf{function}}({\color[rgb]{.545,0,0}\textsf{abstraction}}(X))$
constructs a function with dynamic bindings.

  * •

${\color[rgb]{.545,0,0}\textsf{function}}({\color[rgb]{.545,0,0}\textsf{closure}}(X))$
computes a function with static bindings.

  * •

${\color[rgb]{.545,0,0}\textsf{apply}}(F,V)$ applies the function $F$ to the
argument value $V$.

  * •

${\color[rgb]{.545,0,0}\textsf{supply}}(F,V)$ determines the argument value of
a function application, but returns a thunk that defers executing the body of
the function.

  * •

${\color[rgb]{.545,0,0}\textsf{compose}}(F_{2},F_{1})$ returns the function
that applies $F_{1}$ then $F_{2}$.

  * •

${\color[rgb]{.545,0,0}\textsf{curry}}(F)$ takes a function $F$ that takes a
pair of arguments, and returns the corresponding ‘curried’ function.

  * •

${\color[rgb]{.545,0,0}\textsf{uncurry}}(F)$ takes a curried function $F$ and
returns a function that takes a pair of arguments.

  * •

${\color[rgb]{.545,0,0}\textsf{partial-apply}}(F,V)$ takes a function $F$ that
takes a pair of arguments, and determines the first argument, returning a
function of the second argument.

##### Patterns.

The abstractions of patterns match a given value.

  * •

${\color[rgb]{.545,0,0}\textsf{pattern}}(A)$ constructs values of type
patterns from abstractions $A$.

  * •

${\color[rgb]{.545,0,0}\textsf{match}}(X,{\color[rgb]{.545,0,0}\textsf{pattern}}(A))$
enacts the abstraction $A$, giving it the value of the argument $X$.

A pattern abstraction either computes an environment or fails. Various funcons
express common primitive and composite patterns. The arguments of the funcon
${\color[rgb]{.545,0,0}\textsf{match}}(\\_,\\_)$ can also be structured
values: then the match computes the union of the environments computed by
matching the corresponding components, provided that the structures themselves
match.

###  0.A.2 Flow of Control

  * •

${\color[rgb]{.545,0,0}\textsf{left-to-right}}(\cdots)$ executes its arguments
sequentially, and concatenates the computed value sequences. Composing it with
a funcon having pre-computed arguments prevents interleaving; e.g.,
${\color[rgb]{.545,0,0}\textsf{integer-
add}}({\color[rgb]{.545,0,0}\textsf{left-to-right}}(X,Y))$ always executes $X$
before $Y$. ${\color[rgb]{.545,0,0}\textsf{right-to-left}}(\cdots)$ is
analogous.

  * •

${\color[rgb]{.545,0,0}\textsf{sequential}}(X,\cdots)$ executes the command
$X$, then any remaining arguments, giving the same value(s) as the last
argument.

  * •

${\color[rgb]{.545,0,0}\textsf{effect}}(\cdots)$ interleaves the executions of
its arguments, discarding their computed values, and giving null-value.

  * •

${\color[rgb]{.545,0,0}\textsf{choice}}(Y,\cdots)$ selects one of its
arguments, then executes it.

  * •

${\color[rgb]{.545,0,0}\textsf{if-true-else}}(B,X,Y)$ evaluates $B$ to a
Boolean value, then executes either $X$ or $Y$ (which may correspond to
commands or expressions).

  * •

${\color[rgb]{.545,0,0}\textsf{while-true}}(B,X)$ evaluates $B$ to a Boolean
value, then either executes $X$ (which has to correspond to a command) and
iterates, or terminates.

  * •

${\color[rgb]{.545,0,0}\textsf{interleave}}(\cdots)$ executes its arguments in
any order, possibly with interleaving, and concatenates the computed value
sequences.

###  0.A.3 Flow of Data

  * •

given evaluates to the current value of the given-value entity.

  * •

${\color[rgb]{.545,0,0}\textsf{give}}(X,Y)$ executes $X$ to compute a value.
It then executes $Y$ with that value as the given-value.

  * •

${\color[rgb]{.545,0,0}\textsf{left-to-right-map}}(F,V^{*})$ computes $F$
given each value in the sequence $V^{*}$, returning the sequence of resulting
values.

  * •

${\color[rgb]{.545,0,0}\textsf{interleave-map}}(F,V^{*})$ is similar.

  * •

${\color[rgb]{.545,0,0}\textsf{left-to-right-repeat}}(F,M,N)$ computes $F$
given each integer from $M$ to $N$ sequentially, returning the sequence of
resulting values.

  * •

${\color[rgb]{.545,0,0}\textsf{interleave-repeat}}(F,M,N)$ is similar.

  * •

${\color[rgb]{.545,0,0}\textsf{left-to-right-filter}}(P,V^{*})$ computes $P$
for each value in $V^{*}$, returning the sequence of argument values for which
the computed value is true.

  * •

${\color[rgb]{.545,0,0}\textsf{interleave-filter}}(P,V^{*})$ is similar.

  * •

${\color[rgb]{.545,0,0}\textsf{fold-left}}(F,A,V^{*})$ reduces a sequence
$V^{*}$ to a single value by folding it from the left, using $A$ as the
initial accumulator value, and iteratively updating the accumulator by giving
$F$ the pair of the accumulator value and the first of the remaining
arguments.

  * •

${\color[rgb]{.545,0,0}\textsf{fold-right}}(F,A,V^{*})$ is similar.

For any list $L$, the funcon term ${\color[rgb]{.545,0,0}\textsf{list-
elements}}(L)$ evaluates to the sequence $V^{*}$ of elements in $L$, and
${\color[rgb]{.545,0,0}\textsf{list}}(V^{*})$ reconstructs $L$. Composition
with these funcons allows the above funcons on sequences to be used with
lists; similarly for vectors, sets, multisets, and the datatype of maps.

###  0.A.4 Name Binding

  * •

${\color[rgb]{.545,0,0}\textsf{bind-value}}(I,X)$ computes the singleton
environment mapping $I$ to the value computed by $X$.

  * •

${\color[rgb]{.545,0,0}\textsf{unbind}}(I)$ computes an environment that hides
the binding of $I$.

  * •

${\color[rgb]{.545,0,0}\textsf{bound-value}}(I)$ computes the value to which
$I$ is currently bound (possibly recursively, via a link), if any, and
otherwise fails.

  * •

${\color[rgb]{.545,0,0}\textsf{scope}}(D,X)$ first executes $D$ to compute an
environment $\rho$. It then extends the current environment entity with $\rho$
for the execution of $X$.

  * •

${\color[rgb]{.545,0,0}\textsf{closed}}(X)$ prevents references to non-local
bindings while executing $X$.

  * •

${\color[rgb]{.545,0,0}\textsf{accumulate}}(D_{1},D_{2})$ first executes
$D_{1}$, to compute an environment $\rho_{1}$. It then extends the current
environment entity by $\rho_{1}$ for the execution of $D_{2}$, to compute an
environment $\rho_{2}$. The result is $\rho_{1}$ extended by $\rho_{2}$.

  * •

${\color[rgb]{.545,0,0}\textsf{collateral}}(D_{1},\cdots)$ executes its
arguments to compute environments. It gives their union as result, failing if
their domains are not pairwise disjoint.

  * •

${\color[rgb]{.545,0,0}\textsf{bind-recursively}}(I,X)$ makes
${\color[rgb]{.545,0,0}\textsf{bind-value}}(I,X)$ recursive. It first computes
a singleton environment $\rho$ mapping $I$ to a fresh link $L$. It then
extends the current environment entity by $\rho$ for the execution of $X$, to
compute a value $V$. Finally, it sets $L$ to refer to $V$, and gives $\rho$ as
the computed result.

  * •

${\color[rgb]{.545,0,0}\textsf{recursive}}({\color[rgb]{0,0,0}\textit{SI}},D)$
makes $D$ recursive on the identifiers in the set SI. It first computes an
environment $\rho$ mapping all $I$ in SI to fresh links. It then extends the
current environment entity by $\rho$ for the execution of $D$, to compute an
environment $\rho^{\prime}$. Finally, it sets the link for each $I$ to refer
to the value of $I$ in $\rho^{\prime}$, and gives $\rho^{\prime}$ as the
computed result.

References to recursively-bound names generally need to be inside procedural
abstractions, to avoid inspection of links before they have been set.

###  0.A.5 Imperative Variables

  * •

${\color[rgb]{.545,0,0}\textsf{allocate-variable}}(T)$ constructs a simple
variable for storing values of type $T$ from a location not in the current
store.

  * •

${\color[rgb]{.545,0,0}\textsf{recycle-
variables}}({\color[rgb]{0,0,0}\textit{Var}},\cdots)$ removes locations
allocated to variables from the current store.

  * •

${\color[rgb]{.545,0,0}\textsf{initialise-
variable}}({\color[rgb]{0,0,0}\textit{Var}},V)$ assigns $V$ as the initial
value of Var.

  * •

${\color[rgb]{.545,0,0}\textsf{allocate-initialised-variable}}(T,V)$ is a
composition of ${\color[rgb]{.545,0,0}\textsf{allocate-variable}}(T)$ and
${\color[rgb]{.545,0,0}\textsf{initialise-variable}}(\\_,V)$.

  * •

${\color[rgb]{.545,0,0}\textsf{assign}}({\color[rgb]{0,0,0}\textit{Var}},V)$
stores $V$ at the location of Var when the type contains $V$.

  * •

${\color[rgb]{.545,0,0}\textsf{assigned}}({\color[rgb]{0,0,0}\textit{Var}})$
gives the value last assigned to Var.

  * •

${\color[rgb]{.545,0,0}\textsf{current-value}}(V)$ gives the same result as
${\color[rgb]{.545,0,0}\textsf{assigned}}(V)$ when $V$ is a simple variable,
otherwise $V$.

  * •

${\color[rgb]{.545,0,0}\textsf{un-assign}}({\color[rgb]{0,0,0}\textit{Var}})$
makes Var uninitialised.

  * •

${\color[rgb]{.545,0,0}\textsf{structural-assign}}(V_{1},V_{2})$ assigns to
all the simple variables in $V_{1}$ the corresponding values in $V_{2}$,
provided that the structure and all non-variable values in $V_{1}$ match the
structure and corresponding values of $V_{2}$.

  * •

${\color[rgb]{.545,0,0}\textsf{structural-assigned}}(V)$ computes $V$ with all
simple variables replaced by their assigned values. When $V$ is a simple
variable or a value with no component variables,
${\color[rgb]{.545,0,0}\textsf{structural-assigned}}(V)$ gives the same result
as ${\color[rgb]{.545,0,0}\textsf{current-value}}(V)$.

###  0.A.6 Abrupt Termination

  * •

${\color[rgb]{.545,0,0}\textsf{abrupt}}(V)$ terminates abruptly for reason
$V$.

  * •

${\color[rgb]{.545,0,0}\textsf{handle-abrupt}}(X,Y)$ first executes $X$. If
$X$ terminates normally, $Y$ is ignored. If $X$ terminates abruptly for any
reason, $Y$ is executed, with the reason as the given value.

  * •

${\color[rgb]{.545,0,0}\textsf{finally}}(X,Y)$ first executes $X$. On normal
or abrupt termination of $X$, it executes $Y$. If $Y$ terminates normally, its
computed value is ignored, and the funcon terminates in the same way as $X$;
otherwise it terminates in the same way as $Y$.

  * •

fail abruptly terminates for reason failed.

  * •

${\color[rgb]{.545,0,0}\textsf{else}}(X_{1},X_{2},\cdots)$ executes the
arguments in turn until either some Xi does _not_ fail, or all arguments Xi
have been executed. The last argument executed determines the result.

  * •

${\color[rgb]{.545,0,0}\textsf{else-choice}}(X_{1},X_{2},\cdots)$ is similar,
but executes the arguments sequentially in any order.

  * •

${\color[rgb]{.545,0,0}\textsf{check-true}}(X)$ terminates normally if the
value computed by $X$ is true, and fails if it is false.

  * •

${\color[rgb]{.545,0,0}\textsf{checked}}(X)$ fails when $X$ computes the empty
sequence of values $(\ )$, representing that a value has not been computed. It
otherwise computes the same as $X$.

  * •

${\color[rgb]{.545,0,0}\textsf{throw}}(V)$ abruptly terminates for reason
${\color[rgb]{.545,0,0}\textsf{thrown}}(V)$.

  * •

${\color[rgb]{.545,0,0}\textsf{handle-thrown}}(X,Y)$ handles abrupt
termination of $X$ for reason ${\color[rgb]{.545,0,0}\textsf{thrown}}(V)$ with
$Y$.

  * •

${\color[rgb]{.545,0,0}\textsf{handle-recursively}}(X,Y)$ is similar to
${\color[rgb]{.545,0,0}\textsf{handle-thrown}}(X,Y)$, except that another copy
of the handler attempts to handle any values thrown by $Y$.

  * •

${\color[rgb]{.545,0,0}\textsf{return}}(V)$ abruptly terminates for reason
${\color[rgb]{.545,0,0}\textsf{returned}}(V)$.

  * •

${\color[rgb]{.545,0,0}\textsf{handle-return}}(X)$ evaluates $X$. If $X$
either terminates abruptly for reason
${\color[rgb]{.545,0,0}\textsf{returned}}(V)$, or terminates normally with
value $V$, it terminates normally giving $V$.

  * •

break abruptly terminates for reason broken.

  * •

${\color[rgb]{.545,0,0}\textsf{handle-break}}(X)$ terminates normally when $X$
terminates abruptly for reason broken.

  * •

continue abruptly terminates for reason continued.

  * •

${\color[rgb]{.545,0,0}\textsf{handle-continue}}(X)$ terminates normally when
$X$ terminates abruptly for reason continued.

Further funcons are provided for expressing delimited continuations [23,
Funcons-beta/Computations/Abnormal/Controlling], see also [27].

###  0.A.7 Communication

  * •

read inputs a single non-null value from the standard-in entity, and gives it
as the result.

  * •

${\color[rgb]{.545,0,0}\textsf{print}}(V^{*})$ outputs the sequence of values
$V^{*}$ to the standard-out entity.