# Axiomatic definitions of sublanguages of Loglan'82

Skocz do: nawigacji, wyszukiwania

On these pages we shall attempt to develop a sequence of algorithmic theories that correspond to a sequence of sublanguages of of Loglan'82 language.

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

## Program

Program in Loglan'82 has the following structure

Program
definiendum definiens
program program <name>;
<declarations>

begin

<instructions>

end

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 $\mathcal{L}_0$ of Loglan'82.

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

Programs of the language $\mathcal{L}_0$ 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 $\mathcal{L}_{0.1}$. First, we say that any expression of the form:
writeln;
write(integer);
is an output instruction.

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

 program print; begin write("hallo world!"); writeln; write("Today is: May"); write(22); write(2014); writeln end

### Primitive types

#### Characters

The type char is a finite set of characters. No operation is defined on charcters. However one can compare two characters.

'a' = 'a'

'a' =/= 'c'

The language $\mathcal{L}_{1.1}$ allows to declare variables of type char and to assign values to the variables. Assignments

Example
program characters;

var c1,c2,c3:char

begin

c1:='p';
c2:='d';
writeln(c1,c2);
c3:=c1;
c1:=c2;
c2:=c3;
writeln(c1,c2)

end

Exercise
Guess what will print this program.

One need not to guess. We have much better tool.
Lemma
$(c_1=a \land c_2=b)\Rightarrow [c_3:=c_1; c_1:=c_2; c_2:=c_3](c_1=b \land c_2=a)$
I.e. the execution of three instructions causes swap of the values of variables $c_1, c_2$.
Proof uses two axioms of algorithmic logic:
$\begin{equation}\tag{Ax:=}[x:=\tau]\alpha \Leftrightarrow \alpha(x/\tau) \end{equation}$
this axiom of assignment instruction reads: formula $\alpha(x/\tau)$ holds iff after execution of instruction $x:=\tau$ formula $\alpha$ holds.
$\begin{equation}\tag{Ax ;}[K; M]\alpha \Leftrightarrow [K][M]\alpha \end{equation}$
and the inference rule $\begin{equation}\tag{R2}\dfrac{\alpha \Rightarrow \beta}{M\alpha \Rightarrow M\beta} \end{equation}$ Now observe that the following formulas are equivalent
\begin{align*}{} &(c_1 =a \land c_2=b)& & \\ \Leftrightarrow &(c_1 =a \land c_2=b \land c1=a)& & \mbox{by propositional calculus} \\ \Leftrightarrow & [c_3:=c_1](c_3=a \land c_2 =b \land c_3=a) & & \mbox{by Ax :=} \\ \Leftrightarrow & [c_3:=c_1][c_1:=c_2](c_3=a \land c_1 =b \land c_3=a) & & \mbox{by Ax := and R2} \\ \Leftrightarrow & [c_3:=c_1; c_1:=c_2](c_3=a \land c_1 =b \land c_3=a) & & \mbox{by Ax ;} \\ \Leftrightarrow & [c_3:=c_1; c_1:=c_2][c_2 :=c_3](c_2=a \land c_1 =b \land c_3=a) & & \mbox{by Ax := and R2}\\ \Leftrightarrow & [c_3:=c_1; c_1:=c_2; c_2 :=c_3](c_2=a \land c_1 =b \land c_3=a) & & \mbox{by Ax ;} \\ \end{align*}

#### Boolean

Syntax

Axioms

Example
program Boole;

var a, b, c, b1, b2:Boolean

begin

b1:=a or b;
b2:=b1 and c;
writeln(b1, b2)

end

### 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

$\{x:=\tau\}( \alpha ) \Leftrightarrow \alpha(x/\tau)$