Axiomatic definition of Loglan'82: Różnice pomiędzy wersjami

Wersja z 11:03, 16 paź 2015

On these pages we are sketching, in an incremental way, an axiomatic semantics of Loglan'82.

Part II Axiomatic definitions of sublanguages of Loglan'82

Here we shall present an increasing sequence of sublanguages [math]\mathcal{L}_0\subset\mathcal{L}_1\subset\mathcal{L}_2\subset \mathcal{L}_3\subset\mathcal{L}_4\subset \dots[/math]Loglan'82. For each language [math]\mathcal{L}_i[/math] we shall present its grammar and some axioms and inference rules that define its semantics.

Program

Program in Loglan'82 has the following structure

where name is any identifier, i.e. a finite sequence of letters and digits beginning with a letter.

The declarations and instructions are finite sequences of declarations and instructions respectively, empty squence included.

This allow us to define the first sublanguage [math]\mathcal{L}_0[/math] of Loglan'82.

[math]\mathcal{L}_0 \stackrel{df}{=}\{p\in \mathcal{A}^*: p=\textbf{program}\ \textit{id}; \textbf{begin end} \}[/math]

Programs of the language [math]\mathcal{L}_0[/math] are empty programs, they posses just a name. Their list of instructions as well as list of declarations are empty. The effect of execution of such program is do nothing.

Now we shall define a new language [math]\mathcal{L}_{0.1}[/math]. First, we say that any expression of the form:
writeln;
write(integer);
write("here your text");
is an output instruction.

[math]\mathcal{L}_{0.1} \stackrel{df}{=}\{p\in \mathcal{A}^*: p=\textbf{program} \textit{ id}; \textbf{begin} \lt\textit{output instructions}\gt \textbf{end} \}[/math]

Declarations of variables. Assignment instructions

Example

program P2 ;

var x,y: integer;

begin

y:=74;

x:= y+ 8;

end

Grammar
Context free grammar

Well formed expressions

Axiom

[math]\{x:=\tau\}( \alpha ) \Leftrightarrow \alpha(x/\tau)[/math]