3b =E2=80=93 Two Language Kernels (The Kernels)

3b =E2=80=93 Two Langua= ge Kernels (The Kernels)

`while` and `sa-decl`

Mark Armstrong, PhD Candidate, McMaster University

Fall, 2019

1 The imperat= ive =E2=80=9Ccore=E2=80=9D =E2=80=93 `While`

The basic operation in imperative languages is the assignment. To make a Turing-complete language, we additionally need sequencing and some control structures.

For Turing completeness, a conditional statement and a potentially infinite loop statement are sufficient.
- A conditional and a jump (goto) are simpler (and less restrictive), but jumps are hard to reason about.
- We instead prefer a conditional and a while loop.

1.1 Adding re= ference types

As mentioned, most imperative languages include some ability to work with references to memory.

Even if explicit referencing and dereferencing is rare, we often need to reason about references to implement parts of the language, such as with
- pass by reference parameter passing, or
- non-copying assignment.

To introduce reference types to our language, we extend Expr=E2=82=80 to Expr=E2=82=80=E2=80=B2, adding

expressions for referencing and dereferencing variables, = and

variables of reference type.

=E2=9F=A8expr=E2=9F=A9 =E2=88= =B7=3D =E2=9F=A8rexpr=E2=9F=A9 =E2=9F=A8rexpr=E2=9F=A9 =E2=88=B7=3D & var | var =E2=9F=A8expr=E2=9F=A9 =E2=88=B7=3D ! var

The & operation obtains the reference to a variable.
The ! operation dereferences a reference variable, returning the value stored at the reference.

If the given var is not of reference type, this results in= a type error.

For the moment, we do not handle type errors.

In many languages, the dereferencing operator is *.

1.2 A first l= anguage based on while

So let us define a kernel for imperative languages based on the while loop and an if-then-else. We'll call this language While=E2=82=80.

=E2=9F=A8stmt=E2=9F=A9 =E2=88= =B7=3D skip | var =E2=89=94 =E2=9F=A8expr=E2=9F=A9 | =E2=9F=A8stmt=E2=9F=A9 =E2=9F=A8stmt=E2=9F=A9 | if =E2=9F=A8bexpr=E2=9F=A9 then =E2=9F=A8stmt=E2=9F=A9 else =E2=9F=A8stmt= =E2=9F=A9 | while =E2=9F=A8bexpr=E2=9F=A9 do =E2=9F=A8stmt=E2=9F=A9

Note that:

Sometimes ; is used to sequence instructions, but this is abstract syntax, so we omit it.

Similarly, we do not require an end marker for the body of if's and while loops.

We could omit the then, else and do keywords, but choose to keep them for clarity.
To emphasise that assignment is not equality, we will write it using the symbol =E2=89=94 rather than =3D.

1.2.1 The sho= rtcomings of While=E2=82=80

While=E2=82=80 is a sufficient language in many ways, but it is missing (at least) two key abstractions.

Subroutines

Whether they take the form of functions, procedures or a hybrid of the two, subroutines are a highly valuable abstraction.

But we can encode them in While=E2=82=80 by =E2=80=9Cinlining=E2= =80=9D.

Scope and lifetime

While=E2=82=80 provides no means to declare variables.

Every variable's lifetime is the whole of the runtime.

Every variable's scope is the whole of the program.

Since we can encode subroutines as a linguistic abstraction, we do not address the first shortcoming, at least for the moment.

However, to make the kernel language useful, we must address the second shortcoming.

1.3 The Wh= ile language

Most [imperative] programming languages have, among others, five constructs: assignment, variable declaration, sequence, test and loop. These constructs form the imperative core of the language.

=E2=80=94 Principles of Programming Languages (Dowek)

We add the =E2=80=9Cdo nothing=E2=80=9D command skip to this l= ist of constructs to obtain our language While.

=E2=9F=A8stmt=E2=9F=A9 =E2=88= =B7=3D skip | local var in =E2=9F=A8stmt=E2=9F=A9 | var =E2=89=94 =E2=9F=A8expr=E2=9F=A9 | =E2=9F=A8stmt=E2=9F=A9 =E2=9F=A8stmt=E2=9F=A9 | if =E2=9F=A8bexpr=E2=9F=A9 then =E2=9F=A8stmt=E2=9F=A9 else =E2=9F=A8stmt= =E2=9F=A9 | while =E2=9F=A8bexpr=E2=9F=A9 do =E2=9F=A8stmt=E2=9F=A9

1.4 Embedding= While

In the kernel language approach,

there is an implicit assumption that the kernel language is a proper subset of the full programming language.

The syntax of While we have given

is not a proper subset of the syntax of any full programming language

(that I am aware of).

(To some extent, this is because we have given only abstract syntax).

But, it is close to several,

and we should be able to embed While programs into a any full imperative programming language.

This embedding may not always preserve meaning, though; sometimes the languages don't fully support the abstractions we have in While.

Functionally, this means that if we later show translations from practical languages to While, embedding and translation may not be inverses of each other.

For interest, let us investigate this embedding with a language we are familiar with:

Ruby

1.4.1 Embeddi= ng While into Ruby =E2=80=93 Expressions

Starting with expressions,

all integer and boolean expressions are easily translated into Ruby.
The refencing operation, &, we embed as the method object_id.

& x =E2=89=88 x.object_id

The referencing operation, !, we embed as the function ObjectSpace._id2ref.

! x =E2=89=88 ObjectSpace._id2ref(x)

1.4.2 Embeddi= ng While into Ruby =E2=80=93 Statements

Considering each type of statement of While:

skip

We simply remove all instances of skip.

local var in =E2=9F=A8stmt=E2=9F=A9

We embed local variable declaration as the statement var =3D nil; s where s is the embedding of th= e sub-statement.

var =3D expr

We embed assignment as is.

=E2=9F=A8stmt=E2=9F=A9 =E2=9F=A8stmt=E2=9F=A9

We place a semicolon between the embedding of the statements.

if =E2=9F=A8bexpr=E2=9F=A9 then =E2=9F=A8stmt=E2=9F=A9 else =E2= =9F=A8stmt=E2=9F=A9

We add the keyword end after the second statement.

while =E2=9F=A8bexpr=E2=9F=A9 do =E2=9F=A8stmt=E2=9F=A9

We add the keyword end after the statement.

1.4.3 Embeddi= ng While into Ruby =E2=80=93 Example

By our embedding, the While program

local x in local y in x =3D 5 y =3D ! & x while y > 0 do y =3D y - 1

is embedded as

x =3D nil ; y =3D nil ; x =3D 5 ; y =3D <= span style=3D"font-weight: bold; text-decoration: underline;">ObjectSpace._id2ref(x.object_id) ; while y > 0 do y =3D y - 1 e= nd

2 A declarati= ve model =E2=80=93 SA-Decl

The second kernel language we consider

is a proper subset of Oz, and

contains 8 kinds of statements.

=E2=9F=A8stmt=E2=9F=A9 =E2=88= =B7=3D skip // Empty statement | =E2=9F=A8stmt=E2=9F=A9 =E2=9F=A8stmt=E2=9F=A9 = // Sequence | local =E2=9F=A8var=E2=9F=A9 in =E2=9F=A8stmt=E2=9F=A9 end = // Variable creation | =E2=9F=A8var=E2=9F=A9 =3D =E2=9F=A8var=E2=9F=A9 = // Binding | =E2=9F=A8var=E2=9F=A9 =3D =E2=9F=A8value=E2=9F=A9 = // Value creation | if =E2=9F=A8var=E2=9F=A9 then =E2=9F=A8stmt=E2=9F=A9 else =E2=9F=A8stmt= =E2=9F=A9 end // Conditional | case =E2=9F=A8var=E2=9F=A9 of =E2=9F=A8pattern=E2=9F=A9 then =E2=9F=A8s= =E2=9F=A9 else =E2=9F=A8s=E2=9F=A9 end // Pattern match | `{` {=E2=9F=A8var=E2=9F=A9}=E2=81=BA `}` = // Procedure application

3 Where do we= go from here?

We will continue working with these kernel languages, beginning by

providing linguistic abstraction translations for common language features, and

extending the languages with types.

We will also

define operational semantics for these languages.