Tekst źródłowy strony Axiomatic definitions of sublanguages of Loglan'82

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 <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<br />

{| class="wikitable"
|+ Program
!definiendum!! definiens
|-
| style="background-color:palegreen" | ''program''
| style="background-color:GoldenRod" | '''program''' <''name''>;<br />

:<''declarations''><br />

'''begin'''<br />

:<''instructions''><br />

'''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 <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:<br />
writeln;  <br /> 
write(''integer''); <br />
write("here your text"); <br />
is an output instruction.

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

{| class="wikitable"
|+ style="text-align:left" | '''Example 0.1''' <br />
|-
| program print; <br />
begin <br />
:write("hallo world!"); writeln; <br />
:write("Today is: May"); write(22); write(2014); writeln <br />
end <br/>
|}

=== 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'<br />

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

<big>Example</big><br />
'''program''' characters;<br />
: '''var''' c1,c2,c3:char<br />
'''begin'''<br />
:c1:='p';<br />
:c2:='d';<br />
:writeln(c1,c2); <br />
:c3:=c1; <br />
:c1:=c2; <br />
:c2:=c3; <br />
:writeln(c1,c2) <br />
'''end'''

<big>Exercise</big><br />
Guess what will print this program.

<big>Lemma</big><br />
<math>(c1=a \land c2=b)\Rightarrow [c3:=c1; c1:=c2; c2:=c3](c1=b \land c2=a) </math>

'''Proof''' uses two axioms of algorithmic logic: <br />
<math>\begin{equation}\tag{Ax:=}}[x:=\tau]\alpha \Leftrightarrow \alpha(x/\tau) \end{equation} </math> <br />
this axiom of assignment instruction reads: ''after execution of instruction  '' <math>x:=\tau</math> ''formula  ''<math>\alpha</math> '' holds iff the formula '' <math>\alpha(x/\tau)</math> ''holds before.''
<math>\begin{align*}
 & (c_1 =a \land c_2=b \land c_1=a) & \\
\Leftrightarrow & [c_3 :=c_1](c_3 =a \land c_2=b \land c_3=a) & by Assign axiom \\
\Leftrightarrow & [c_3 :=c_1][c_1:=c_2](c_3 =a \land c_1=b \land c_3=a) & by Assign axiom \\
\Leftrightarrow & [c_3 :=c_1; c_1:=c_2](c_3 =a \land c_1=b \land c_3=a) & by   axiom \\
\Leftrightarrow & [c_3 :=c_1; c_1:=c_2][c_2:=c_3](c_3 =a \land c_1=b \land c_3=a) & by   axiom \\
\Leftrightarrow & [c_3 :=c_1; c_1:=c_2;c_2:=c_3](c_3 =a \land c_1=b \land c_3=a) & by   axiom \\
\end{align*}  </math>

==== Boolean ====

Syntax

Axioms


<big>Example</big><br />
'''program''' Boole;<br />
: '''var''' a, b, c, b1, b2:Boolean<br />
'''begin'''<br />
:b1:=a or b;<br />
:b2:=b1 and c;<br />
:writeln(b1, b2)<br />
'''end'''

=== Declarations of variables. Assignment instructions ===
'''Example'''<br />

'''program'''  P2 ;<br />
:'''var''' x,y: integer;<br />
'''begin'''<br />
:y:=74;<br />
:x:= y+ 8;<br />
'''end'''<br />

'''Grammar'''<br />
Context free grammar

Well formed expressions

'''Axiom'''<br />

<math>\{x:=\tau\}( \alpha ) \Leftrightarrow \alpha(x/\tau)</math>