Unstable-Languages-beta : LD-Start.cbs | PLAIN | PDF
OUTLINE
\[\KEY{Language} \quad \STRING{LD}\] \[\begin{align*} [ \ \textsf{\SECTREF{1}} \ & \textsf{Lexical constructs} \\ \textsf{\SECTREF{2}} \ & \textsf{Call-by-value lambda-calculus} \\ \textsf{\SECTREF{3}} \ & \textsf{Arithmetic and Boolean expressions} \\ \textsf{\SECTREF{4}} \ & \textsf{References and imperatives} \\ \textsf{\SECTREF{5}} \ & \textsf{Multithreading} \\ \textsf{\SECTREF{6}} \ & \textsf{Programs} \\ \textsf{\SECTHYPER{../.}{LD-Disambiguation}{A}} \ & \textsf{Disambiguation} \ ] \end{align*}\]
Lexical syntax:
\[\begin{align*} \KEY{Lexis} \quad \VARDECL{X} : \SYNDECL{id} \ ::= \ & \ \LEFTGROUP \LEX{a} {-} \LEX{z} \RIGHTGROUP \ \LEFTGROUP \LEX{a} {-} \LEX{z} \mid \LEX{0} {-} \LEX{9} \RIGHTGROUP\STAR \\ \VARDECL{N} : \SYNDECL{int} \ ::= \ & \ \LEFTGROUP \LEX{0} {-} \LEX{9} \RIGHTGROUP\PLUS \\ \SYNDECL{keyword} \ ::= \ & \ \LEX{do} \mid \LEX{else} \mid \LEX{fork} \mid \LEX{if} \\ \ \mid \ & \ \LEX{in} \mid \LEX{join} \mid \LEX{lambda} \mid \LEX{let} \\ \ \mid \ & \ \LEX{ref} \mid \LEX{spawn} \mid \LEX{then} \mid \LEX{while} \end{align*}\]Context-free syntax:
\[\begin{align*} \KEY{Syntax} \quad \VARDECL{E} : \SYNDECL{exp} \ ::= \ & \ \SYNREF{int} \\ \ \mid \ & \ \SYNREF{id} \\ \ \mid \ & \ \LEX{lambda} \ \SYNREF{id} \ \LEX{{.}} \ \SYNREF{exp} \\ \ \mid \ & \ \SYNREF{exp} \ \SYNREF{exp} \\ \ \mid \ & \ \LEX{let} \ \SYNREF{id} \ \LEX{{=}} \ \SYNREF{exp} \ \LEX{in} \ \SYNREF{exp} \\ \ \mid \ & \ \LEX{{(}} \ \SYNREF{exp} \ \LEX{{)}} \\ \ \mid \ & \ \SYNREF{exp} \ \LEX{{+}} \ \SYNREF{exp} \\ \ \mid \ & \ \SYNREF{exp} \ \LEX{{*}} \ \SYNREF{exp} \\ \ \mid \ & \ \SYNREF{exp} \ \LEX{{/}} \ \SYNREF{exp} \\ \ \mid \ & \ \SYNREF{exp} \ \LEX{{<}{=}} \ \SYNREF{exp} \\ \ \mid \ & \ \SYNREF{exp} \ \LEX{{\AMPERSAND}{\AMPERSAND}} \ \SYNREF{exp} \\ \ \mid \ & \ \LEX{if} \ \SYNREF{exp} \ \LEX{then} \ \SYNREF{exp} \ \LEX{else} \ \SYNREF{exp} \\ \ \mid \ & \ \LEX{ref} \ \SYNREF{exp} \\ \ \mid \ & \ \SYNREF{exp} \ \LEX{{:}{=}} \ \SYNREF{exp} \\ \ \mid \ & \ \LEX{{!}} \ \SYNREF{exp} \\ \ \mid \ & \ \SYNREF{exp} \ \LEX{{;}} \ \SYNREF{exp} \\ \ \mid \ & \ \LEX{{(}} \ \LEX{{)}} \\ \ \mid \ & \ \LEX{while} \ \SYNREF{exp} \ \LEX{do} \ \SYNREF{exp} \\ \ \mid \ & \ \LEX{spawn} \ \SYNREF{exp} \\ \ \mid \ & \ \LEX{join} \ \SYNREF{exp} \end{align*}\]Expression evaluation:
\[\begin{align*} \KEY{Type} \quad & \NAMEDECL{ld-values} \\&\quad \leadsto \NAMEHYPER{../../../../../Funcons-beta/Values/Abstraction}{Functions}{functions} ( \NAMEHYPER{../../../../../Funcons-beta/Values}{Value-Types}{values}, \NAMEHYPER{../../../../../Funcons-beta/Values}{Value-Types}{values} ) \\&\quad\quad\quad \mid \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Integers}{integers} \\&\quad\quad\quad \mid \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Booleans}{booleans} \\&\quad\quad\quad \mid \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Storing}{variables} \\&\quad\quad\quad \mid \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Null}{null-type} \\&\quad\quad\quad \mid \NAMEHYPER{../../../../../Unstable-Funcons-beta/Computations/Threads}{Multithreading}{thread-ids} \end{align*}\] \[\begin{align*} \KEY{Semantics} \quad & \SEMDECL{eval} \LEFTPHRASE \ \_ : \SYNREF{exp} \ \RIGHTPHRASE : \TO \NAMEREF{ld-values} \end{align*}\]\(\SECT{1}\) Lexical constructs
\[\begin{align*} \KEY{Rule} \quad & \SEMREF{eval} \LEFTPHRASE \ \VARREF{N} \ \RIGHTPHRASE = \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Integers}{decimal} \ \textsf{\textquotedblleft}\VAR{N}\textsf{\textquotedblright} \\ \KEY{Rule} \quad & \SEMREF{eval} \LEFTPHRASE \ \VARREF{X} \ \RIGHTPHRASE = \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Binding}{bound} \ \textsf{\textquotedblleft}\VAR{X}\textsf{\textquotedblright} \end{align*}\]\(\SECT{2}\) Call-by-value lambda-calculus
\[\begin{align*} \KEY{Rule} \quad & \SEMREF{eval} \LEFTPHRASE \ \LEX{lambda} \ \VARREF{X} \ \LEX{{.}} \ \VARREF{E} \ \RIGHTPHRASE = \\&\quad \NAMEHYPER{../../../../../Funcons-beta/Values/Abstraction}{Functions}{function} \ \NAMEHYPER{../../../../../Funcons-beta/Values/Abstraction}{Generic}{closure} \\&\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Binding}{scope} ( \\&\quad\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Binding}{bind} ( \textsf{\textquotedblleft}\VAR{X}\textsf{\textquotedblright}, \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Giving}{given} ), \\&\quad\quad\quad \SEMREF{eval} \LEFTPHRASE \ \VAR{E} \ \RIGHTPHRASE ) \\ \KEY{Rule} \quad & \SEMREF{eval} \LEFTPHRASE \ \VARREF{E}\SUB{1} \ \VARREF{E}\SUB{2} \ \RIGHTPHRASE = \\&\quad \NAMEHYPER{../../../../../Funcons-beta/Values/Abstraction}{Functions}{apply} ( \SEMREF{eval} \LEFTPHRASE \ \VAR{E}\SUB{1} \ \RIGHTPHRASE , \SEMREF{eval} \LEFTPHRASE \ \VAR{E}\SUB{2} \ \RIGHTPHRASE ) \\ \KEY{Rule} \quad & \SEMREF{eval} \LEFTPHRASE \ \LEX{let} \ \VARREF{X} \ \LEX{{=}} \ \VARREF{E}\SUB{1} \ \LEX{in} \ \VARREF{E}\SUB{2} \ \RIGHTPHRASE = \\&\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Binding}{scope} ( \\&\quad\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Binding}{bind} ( \textsf{\textquotedblleft}\VAR{X}\textsf{\textquotedblright}, \SEMREF{eval} \LEFTPHRASE \ \VAR{E}\SUB{1} \ \RIGHTPHRASE ), \\&\quad\quad \SEMREF{eval} \LEFTPHRASE \ \VAR{E}\SUB{2} \ \RIGHTPHRASE ) \end{align*}\]Desugaring (alternative to the above rule):
\[\begin{align*} \KEY{Rule} \quad & \LEFTPHRASE \ \LEX{let} \ \VARREF{X} \ \LEX{{=}} \ \VARREF{E}\SUB{1} \ \LEX{in} \ \VARREF{E}\SUB{2} \ \RIGHTPHRASE : \SYNREF{exp} = \\& \LEFTPHRASE \ \LEX{{(}} \ \LEX{lambda} \ \VAR{X} \ \LEX{{.}} \ \VAR{E}\SUB{2} \ \LEX{{)}} \ \LEX{{(}} \ \VAR{E}\SUB{1} \ \LEX{{)}} \ \RIGHTPHRASE \end{align*}\] \[\begin{align*} \KEY{Rule} \quad & \SEMREF{eval} \LEFTPHRASE \ \LEX{{(}} \ \VARREF{E} \ \LEX{{)}} \ \RIGHTPHRASE = \SEMREF{eval} \LEFTPHRASE \ \VAR{E} \ \RIGHTPHRASE \end{align*}\]\(\SECT{3}\) Arithmetic and Boolean expressions
\[\begin{align*} \KEY{Rule} \quad & \SEMREF{eval} \LEFTPHRASE \ \VARREF{E}\SUB{1} \ \LEX{{+}} \ \VARREF{E}\SUB{2} \ \RIGHTPHRASE = \\&\quad \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Integers}{int-add} ( \SEMREF{eval} \LEFTPHRASE \ \VAR{E}\SUB{1} \ \RIGHTPHRASE , \SEMREF{eval} \LEFTPHRASE \ \VAR{E}\SUB{2} \ \RIGHTPHRASE ) \\ \KEY{Rule} \quad & \SEMREF{eval} \LEFTPHRASE \ \VARREF{E}\SUB{1} \ \LEX{{*}} \ \VARREF{E}\SUB{2} \ \RIGHTPHRASE = \\&\quad \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Integers}{int-mul} ( \SEMREF{eval} \LEFTPHRASE \ \VAR{E}\SUB{1} \ \RIGHTPHRASE , \SEMREF{eval} \LEFTPHRASE \ \VAR{E}\SUB{2} \ \RIGHTPHRASE ) \\ \KEY{Rule} \quad & \SEMREF{eval} \LEFTPHRASE \ \VARREF{E}\SUB{1} \ \LEX{{/}} \ \VARREF{E}\SUB{2} \ \RIGHTPHRASE = \\&\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Abnormal}{Failing}{checked} \ \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Integers}{int-div} ( \SEMREF{eval} \LEFTPHRASE \ \VAR{E}\SUB{1} \ \RIGHTPHRASE , \SEMREF{eval} \LEFTPHRASE \ \VAR{E}\SUB{2} \ \RIGHTPHRASE ) \\ \KEY{Rule} \quad & \SEMREF{eval} \LEFTPHRASE \ \VARREF{E}\SUB{1} \ \LEX{{<}{=}} \ \VARREF{E}\SUB{2} \ \RIGHTPHRASE = \\&\quad \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Integers}{is-less-or-equal} \ \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Flowing}{l-to-r} ( \SEMREF{eval} \LEFTPHRASE \ \VAR{E}\SUB{1} \ \RIGHTPHRASE , \SEMREF{eval} \LEFTPHRASE \ \VAR{E}\SUB{2} \ \RIGHTPHRASE ) \\ \KEY{Rule} \quad & \SEMREF{eval} \LEFTPHRASE \ \VARREF{E}\SUB{1} \ \LEX{{\AMPERSAND}{\AMPERSAND}} \ \VARREF{E}\SUB{2} \ \RIGHTPHRASE = \\&\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Flowing}{if-true-else} ( \SEMREF{eval} \LEFTPHRASE \ \VAR{E}\SUB{1} \ \RIGHTPHRASE , \SEMREF{eval} \LEFTPHRASE \ \VAR{E}\SUB{2} \ \RIGHTPHRASE , \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Booleans}{false} ) \\ \KEY{Rule} \quad & \SEMREF{eval} \LEFTPHRASE \ \LEX{if} \ \VARREF{E}\SUB{1} \ \LEX{then} \ \VARREF{E}\SUB{2} \ \LEX{else} \ \VARREF{E}\SUB{3} \ \RIGHTPHRASE = \\&\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Flowing}{if-true-else} ( \SEMREF{eval} \LEFTPHRASE \ \VAR{E}\SUB{1} \ \RIGHTPHRASE , \SEMREF{eval} \LEFTPHRASE \ \VAR{E}\SUB{2} \ \RIGHTPHRASE , \SEMREF{eval} \LEFTPHRASE \ \VAR{E}\SUB{3} \ \RIGHTPHRASE ) \end{align*}\]\(\SECT{4}\) References and imperatives
\[\begin{align*} \KEY{Rule} \quad & \SEMREF{eval} \LEFTPHRASE \ \LEX{ref} \ \VARREF{E} \ \RIGHTPHRASE = \\&\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Storing}{allocate-initialised-variable} ( \NAMEREF{ld-values}, \SEMREF{eval} \LEFTPHRASE \ \VAR{E} \ \RIGHTPHRASE ) \\ \KEY{Rule} \quad & \SEMREF{eval} \LEFTPHRASE \ \VARREF{E}\SUB{1} \ \LEX{{:}{=}} \ \VARREF{E}\SUB{2} \ \RIGHTPHRASE = \\&\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Storing}{assign} ( \SEMREF{eval} \LEFTPHRASE \ \VAR{E}\SUB{1} \ \RIGHTPHRASE , \SEMREF{eval} \LEFTPHRASE \ \VAR{E}\SUB{2} \ \RIGHTPHRASE ) \\ \KEY{Rule} \quad & \SEMREF{eval} \LEFTPHRASE \ \LEX{{!}} \ \VARREF{E} \ \RIGHTPHRASE = \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Storing}{assigned} ( \SEMREF{eval} \LEFTPHRASE \ \VAR{E} \ \RIGHTPHRASE ) \\ \KEY{Rule} \quad & \SEMREF{eval} \LEFTPHRASE \ \VARREF{E}\SUB{1} \ \LEX{{;}} \ \VARREF{E}\SUB{2} \ \RIGHTPHRASE = \\&\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Flowing}{sequential} ( \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Flowing}{effect} ( \SEMREF{eval} \LEFTPHRASE \ \VAR{E}\SUB{1} \ \RIGHTPHRASE ), \SEMREF{eval} \LEFTPHRASE \ \VAR{E}\SUB{2} \ \RIGHTPHRASE ) \\ \KEY{Rule} \quad & \SEMREF{eval} \LEFTPHRASE \ \LEX{{(}} \ \LEX{{)}} \ \RIGHTPHRASE = \NAMEHYPER{../../../../../Funcons-beta/Values/Primitive}{Null}{null-value} \\ \KEY{Rule} \quad & \SEMREF{eval} \LEFTPHRASE \ \LEX{while} \ \VARREF{E}\SUB{1} \ \LEX{do} \ \VARREF{E}\SUB{2} \ \RIGHTPHRASE = \\&\quad \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Flowing}{while-true} ( \SEMREF{eval} \LEFTPHRASE \ \VAR{E}\SUB{1} \ \RIGHTPHRASE , \NAMEHYPER{../../../../../Funcons-beta/Computations/Normal}{Flowing}{effect} ( \SEMREF{eval} \LEFTPHRASE \ \VAR{E}\SUB{2} \ \RIGHTPHRASE ) ) \end{align*}\]\(\SECT{5}\) Multithreading
N.B. The funcons for multithreading have not yet been fully validated, so they are defined in Unstable-Funcons-beta instead of Funcons-beta.
\[\begin{align*} \KEY{Rule} \quad & \SEMREF{eval} \LEFTPHRASE \ \LEX{spawn} \ \VARREF{E} \ \RIGHTPHRASE = \\&\quad \NAMEHYPER{../../../../../Unstable-Funcons-beta/Computations/Threads}{Multithreading}{thread-activate} \ \NAMEHYPER{../../../../../Unstable-Funcons-beta/Computations/Threads}{Multithreading}{thread-joinable} \ \NAMEHYPER{../../../../../Funcons-beta/Values/Abstraction}{Thunks}{thunk} \ \NAMEHYPER{../../../../../Funcons-beta/Values/Abstraction}{Generic}{closure} \ \SEMREF{eval} \LEFTPHRASE \ \VAR{E} \ \RIGHTPHRASE \\ \KEY{Rule} \quad & \SEMREF{eval} \LEFTPHRASE \ \LEX{join} \ \VARREF{E} \ \RIGHTPHRASE = \NAMEHYPER{../../../../../Unstable-Funcons-beta/Computations/Threads}{Multithreading}{thread-join} ( \SEMREF{eval} \LEFTPHRASE \ \VAR{E} \ \RIGHTPHRASE ) \end{align*}\]