Axiomatic definitions of sublanguages of Loglan'82: Różnice pomiędzy wersjami
(→Characters) |
(→Characters) |
||
(Nie pokazano 9 pośrednich wersji utworzonych przez tego samego użytkownika) | |||
Linia 78: | Linia 78: | ||
Guess what will print this program. | Guess what will print this program. | ||
− | One need not to guess. We have much better tool. | + | One need not to guess. We have much better tool. <br /> |
<big>Lemma</big><br /> | <big>Lemma</big><br /> | ||
− | <math>(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) </math> | + | <math>(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) </math><br /> |
− | I.e. ''the execution of three instructions causes swap of the values of variables'' <math> c_1, c_2 </math>. | + | I.e. ''the execution of three instructions causes swap of the values of variables'' <math> c_1, c_2 </math>.<br /> |
'''Proof''' uses two axioms of algorithmic logic: <br /> | '''Proof''' uses two axioms of algorithmic logic: <br /> | ||
<math>\begin{equation}\tag{Ax:=}[x:=\tau]\alpha \Leftrightarrow \alpha(x/\tau) \end{equation} </math> <br /> | <math>\begin{equation}\tag{Ax:=}[x:=\tau]\alpha \Leftrightarrow \alpha(x/\tau) \end{equation} </math> <br /> | ||
Linia 87: | Linia 87: | ||
<math>\begin{equation}\tag{Ax ;}[K; M]\alpha \Leftrightarrow [K][M]\alpha \end{equation} </math><br /> | <math>\begin{equation}\tag{Ax ;}[K; M]\alpha \Leftrightarrow [K][M]\alpha \end{equation} </math><br /> | ||
and the inference rule | and the inference rule | ||
− | <math>\begin{equation}\tag{R2}\dfrac{\alpha \Rightarrow \beta}{M\alpha \Rightarrow M\beta} | + | <math>\begin{equation}\tag{R2}\dfrac{\alpha \Rightarrow \beta}{M\alpha \Rightarrow M\beta} \end{equation} </math> |
Now observe that the following formulas are equivalent<br /> | Now observe that the following formulas are equivalent<br /> | ||
<math>\begin{align*}{} | <math>\begin{align*}{} | ||
&(c_1 =a \land c_2=b)& & \\ | &(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*} </math> | \end{align*} </math> | ||
Aktualna wersja na dzień 15:21, 27 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.
Spis treści
Program
Program in Loglan'82 has the following structure
definiendum | definiens |
---|---|
program | program <name>;
begin
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]
program print; begin
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.
One need not to guess. We have much better tool.
Lemma
[math](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) [/math]
I.e. the execution of three instructions causes swap of the values of variables [math] c_1, c_2 [/math].
Proof uses two axioms of algorithmic logic:
[math]\begin{equation}\tag{Ax:=}[x:=\tau]\alpha \Leftrightarrow \alpha(x/\tau) \end{equation} [/math]
this axiom of assignment instruction reads: formula [math]\alpha(x/\tau)[/math] holds iff after execution of instruction [math]x:=\tau[/math] formula [math]\alpha[/math] holds.
[math]\begin{equation}\tag{Ax ;}[K; M]\alpha \Leftrightarrow [K][M]\alpha \end{equation} [/math]
and the inference rule
[math]\begin{equation}\tag{R2}\dfrac{\alpha \Rightarrow \beta}{M\alpha \Rightarrow M\beta} \end{equation} [/math]
Now observe that the following formulas are equivalent
[math]\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*} [/math]
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]