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

Z Lem
Skocz do: nawigacji, wyszukiwania
(Characters)
(Characters)
Linia 79: Linia 79:
  
 
<big>Lemma</big><br />
 
<big>Lemma</big><br />
<math>(c1=a \land c2=b)\Leftarrow [c3:=c1; c1:=c2; c2:=c3](c1=b \land c2=a) </math>
+
<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>[x:=\tau]\alpha Leftrightarrow \alpha(x/\tau) </math>
 +
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.''
  
 
==== Boolean ====
 
==== Boolean ====

Wersja z 16:11, 26 lis 2014

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

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 [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]

Example 0.1
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 [math]\mathcal{L}_{1.1} [/math] 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.

Lemma
[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:
[math][x:=\tau]\alpha Leftrightarrow \alpha(x/\tau) [/math] 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.

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

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