\( % cbs-katex.sty % \newcommand{\STYLE}[2]{\htmlClass{cbs-#1}{#2}} \newcommand{\DECL}[3]{\htmlId{#1:#2}{#3}} \newcommand{\REF}[3]{\href{###1:#2}{#3}} \newcommand{\HYPER}[5]{\href{#1/#2/index.html###3:#4}{#5}} % \SHADE{MATH} can be defined to produce a shaded background to highlight % inline MATH in running text: \newcommand{\SHADE}[1]{#1} % \KEY{TEXT}, \STRING{TEXT}, \ATOM{TEXT}, \LEX{TEXT} can be used in math mode: \newcommand{\KEY}[1]{\textsf{\textit{\STYLE{Key}{#1}}}} \newcommand{\STRING}[1]{\textsf{``\texttt{#1}''}} \newcommand{\ATOM}[1]{\textsf{`\texttt{#1}'}} \newcommand{\LEX}[1]{\textsf{\STYLE{Key}{`}\texttt{#1}\STYLE{Key}{'}}} % The following commands produce ASCII characters that are treated specially by LaTeX: \newcommand{\HASH}{\char`\#} \newcommand{\DOLLAR}{\char`\$} \newcommand{\PERCENT}{\char`\%} \newcommand{\AMPERSAND}{\char`\&} \newcommand{\APOSTROPHE}{\char`\'} \newcommand{\BACKSLASH}{\char`\\} \newcommand{\CARET}{\char`\^} \newcommand{\UNDERSCORE}{\char`\_} \newcommand{\GRAVE}{\char`\`} \newcommand{\LEFTBRACE}{\char`\{} \newcommand{\RIGHTBRACE}{\char`\}} \newcommand{\TILDE}{\textasciitilde} % {\char`\~} % \NAME{name} highlights the name; % \NAMEDECL{name} declares Name.name as the target of links to name; % \NAMEREF{name} links name to the target Name.name in the current file; % \NAMEHYPER{url}{file}{name} links name to Name.name at url/file/file.pdf. % Similarly for \VAR{partvariable}, \SYN{syntaxname}, \SEM{semanticsName}, % and \SECT{sectionnumber} % The kerns in \SUB and \VAR avoid overlaps with primes: \newcommand{\SUB}[1]{_{\kern-2mu\STYLE{PartVariable}{\textsf{#1}}}} % PLAIN \newcommand{\VAR}[1]{\STYLE{PartVariable}{\textsf{\textit{#1}\kern2mu}}} \newcommand{\NAME}[1]{\STYLE{Name}{\textsf{#1}}} \newcommand{\SYN}[1]{\STYLE{SyntaxName}{\textsf{#1}}} \newcommand{\SEM}[1]{\STYLE{SemanticsName}{\textsf{#1}}} \newcommand{\SECT}[1]{\STYLE{SectionNumber}{\textsf{#1}}} % DECL \newcommand{\VARDECL}[1]{\DECL{PartVariable}{#1}{\VAR{#1}}} \newcommand{\NAMEDECL}[1]{\DECL{Name}{#1}{\NAME{#1}}} \newcommand{\SYNDECL}[1]{\DECL{SyntaxName}{#1}{\SYN{#1}}} \newcommand{\SEMDECL}[1]{\DECL{SemanticsName}{#1}{\SEM{#1}}} \newcommand{\SECTDECL}[1]{\DECL{SectionNumber}{#1}{\textsf{#1}}} % REF \newcommand{\VARREF}[1]{\REF{PartVariable}{#1}{\VAR{#1}}} \newcommand{\NAMEREF}[1]{\REF{Name}{#1}{\NAME{#1}}} \newcommand{\SYNREF}[1]{\REF{SyntaxName}{#1}{\SYN{#1}}} \newcommand{\SEMREF}[1]{\REF{SemanticsName}{#1}{\SEM{#1}}} \newcommand{\SECTREF}[1]{\REF{SectionNumber}{#1}{\SECT{#1}}} % HYPER \newcommand{\VARHYPER}[3]{\HYPER{#1}{#2}{PartVariable}{#3}{\VAR{#3}}} \newcommand{\NAMEHYPER}[3]{\HYPER{#1}{#2}{Name}{#3}{\NAME{#3}}} \newcommand{\SYNHYPER}[3]{\HYPER{#1}{#2}{SyntaxName}{#3}{\SYN{#3}}} \newcommand{\SEMHYPER}[3]{\HYPER{#1}{#2}{SemanticsName}{#3}{\SEM{#3}}} \newcommand{\SECTHYPER}[3]{\HYPER{#1}{#2}{SectionNumber}{#3}{\SECT{#3}}} % \LEFTPHRASE MATH \RIGHTPHRASE produces [[ MATH ]] with proper brackets: \newcommand{\LEFTPHRASE}{\llbracket} \newcommand{\RIGHTPHRASE}{\rrbracket} % \LEFTGROUP MATH \RIGHTGROUP produces ( MATH ) where the parentheses are % highlighted the same as keywords: \newcommand{\LEFTGROUP}{\STYLE{Key}{(}} \newcommand{\RIGHTGROUP}{\STYLE{Key}{)}} % MATH\PLUS produces a superscript + % MATH\STAR produces a superscript * % MATH\QUERY produces a superscript ? \newcommand{\PLUS}{{}^{\texttt{+}}} \newcommand{\STAR}{{}^{\texttt{*}}} \newcommand{\QUERY}{{}^{\texttt{?}}} % \RULE{& PREMISE \\ & ...}{& FORMULA ... \\ & ...} produces an inference rule % with separately aligned premises and conclusion % PREMISE % ... % ----------- % FORMULA ... % ... \newcommand{\RULE}[2] {\frac{\begin{aligned}#1\end{aligned}}{\begin{aligned}#2\end{aligned}}} % \AXIOM{& FORMULA ... \\ & ...} produces an aligned formula % % FORMULA ... % ... \newcommand{\AXIOM}[1]{\begin{aligned}#1\end{aligned}} % \TO TYPE produces => TYPE \newcommand{\TO}{\mathop{\Rightarrow}} % TERM \TRANS TERM produces TERM ---> TERM \newcommand{\TRANS}{\longrightarrow} % TERM \xrightarrow{LABEL} TERM puts the label above the long arrow % \)

Funcons-beta

This page introduces the beta-release of an initial collection of so-called ‘funcons’ (fundamental programming constructs). Other pages introduce and motivate the use of funcons in the CBS framework, and explain the purpose of the beta-release.

Funcons are reusable components of programming language specifications: the semantics of a language is specified by translating its syntax to funcons, reusing (by reference) the definitions of the required funcons.

Specifying a language by translation to funcons – and updating the specification as the language evolves – should be much less effort than defining its semantics in previous frameworks! See Languages-beta for some illustrative examples of language specifications in CBS, and LangDev-2019 for a demonstration of the ease of updating a language specification as the language evolves.

Funcon definitions

Funcons are defined using a variant of structural operational semantics (SOS, developed by Gordon Plotkin in the 1980s). Computations are sequences of labelled transitions between states, which generally consist of syntax, computed values, and auxiliary entities such as stores and environments. Computed values are final states, having no transitions.

However, SOS specifications lack modularity: when a new auxiliary entity is introduced for specifying an extended language, all the previous rules may need to be updated. And modularity is crucial for CBS, since adding new funcons to the collection must not require any changes at all to the definitions of previous funcons.

In the modular variant of SOS used in CBS for defining funcons, auxiliary entities are implicitly propagated when omitted in particular rules: adding a new auxiliary entity never affects existing rules. Such modular SOS rules also look a lot simpler than the corresponding conventional SOS rules, since each rule references only the entities that it actually requires.

Funcons have signatures, which specify the numbers and types of their arguments and results, and whether particular arguments are to be evaluated before using the specified rules or not (corresponding closely to strictness annotations in the K-framework).

Operational semantics

The operational semantics of a funcon term is the set of all its computations, where each computation consists of a (possibly-empty, possibly infinite) sequence of transitions according to the specified rules. The computations generally depend on the computations of any subterms; they may also depend on the initial values of auxiliary entities.

Computations

The computations page introduces funcons for specifying flow of control, and funcons whose execution generally involves auxiliary entities (environments, stores, etc.). These funcons are defined using a modular variant of structural operational semantics: entities that are not essential for a particular funcon are implicitly propagated between premises and conclusions of the rules used to define it, so the rules do not need updating when new entities are introduced.

Entities

The entities page lists the entities that are used in the definitions of funcons for computations. The execution of a term is unaffected by entities that are not involved in the funcons used in it.

There are no funcons for reifying auxiliary entities as values, nor for reflecting values as entities! This is because the way that particular entities flow during funcon execution is inherent and characteristic; reification and reflection would allow the flow to be circumvented.

For instance, stores that represent assignments to imperative variables are implicitly threaded through the individual steps of funcon executions, and cannot be (directly) copied or reset. There are funcons for allocating a variable, initialising its value, inspecting its value, and assigning a new value – but not for making a copy of the current store, nor for replacing the entire store.

Values

Value constructors are particularly simple funcons: they have no rules at all, and the values they compute are formed by replacing their arguments by computed values. Funcon terms formed entirely from value constructors are ground values; non-ground values include abstractions, formed from value constructors that have unevaluated arguments. The only computation starting from a value is trivial: the empty sequence of transitions.

The values page introduces funcons whose executions compute values from argument values without use of auxiliary entities. These funcons are defined using an embedding of conditional term rewriting in modular structural operational semantics, with all entities implicitly propagated between premises and conclusions of rules. Value constructors are not affected by rewriting, and can be matched in argument patterns in rules for funcon computation.

Funcons-Index

The Funcons-Index page lists the names of all the funcons defined in the CBS library (including aliases). The funcons are grouped together according to the types and entities involved in their definitions.

Sections of the Funcons-Index page correspond to the folders and files that contain the funcon definitions. However, no familiarity with the file system is required when browsing CBS specifications, since references to funcons are always hyperlinked to the corresponding definitions.

CBS does not have explicit packages: each language specification implicitly imports the entire library, and the list of the funcons that it uses is generated from the specification. This not only eliminates tedious lists of imported packages, but also reduces the effort of making changes.

→