Axiomatic definition of Loglan'82: Różnice pomiędzy wersjami
(→Language \mathcal{L}_{1,c}) |
(→\mathcal{L}_{1} Declarations of variables. Assignment instructions) |
||
| Linia 103: | Linia 103: | ||
| style="color:Blue" | <math> \textbf{begin }\, K: M \textbf{ end}\, \alpha \equiv K M\, \alpha </math> | | style="color:Blue" | <math> \textbf{begin }\, K: M \textbf{ end}\, \alpha \equiv K M\, \alpha </math> | ||
|} | |} | ||
| − | + | How to use these axioms?<br /> | |
| + | We present a lemma that is universally true for all the sublanguages of the language <math>\mathcal{L}_{1}</math>. | ||
| + | <math>\begin{lemma} | ||
| + | Let T be a type. Let x, y, z be variables of type T. The following algorithmic logic is tautology | ||
| + | (x=a \land y=b)\implies \{z:=x;\,x:=y;\,y:=z \}(x=b \land y=a) | ||
| + | \end{lemma} | ||
| + | </math> | ||
=== Language <math>\mathcal{L}_{1,c}</math> === | === Language <math>\mathcal{L}_{1,c}</math> === | ||
Declarations are declarations of variables of type char. | Declarations are declarations of variables of type char. | ||
Wersja z 15:14, 23 paź 2015
On these pages we are sketching, in an incremental way, an axiomatic semantics of Loglan'82.
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.
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,0}[/math] of Loglan'82.
Language [math]\mathcal{L}_{0,0}[/math]
[math]\mathcal{L}_{0,0} \stackrel{df}{=}\{p\in \mathcal{A}^*: p=\textbf{program}\ \textit{id}; \textbf{begin end} \}[/math]
Programs of the language [math]\mathcal{L}_{0,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.
Language [math]\mathcal{L}_{0,1}[/math]
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]
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.
Example 0.1
| program print; begin
end |
Semantics
Each output instruction appends a string of characters to the standard output.
[math]\mathcal{L}_{1}[/math] Declarations of variables. Assignment instructions
Now we shall introduce the linear programs. Each program of this group contains declarations of variable and the instructions of a program are the assignment instructions only.
The language [math]\mathcal{L}_{1}[/math] is the closure of languages [math]\mathcal{L}_{1,c} \cup \mathcal{L}_{1,s}\cup \mathcal{L}_{1,b}\cup \mathcal{L}_{1,i}\cup \mathcal{L}_{1,r}[/math]
The structure of a program is as follow:
| 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. The structure of assignment instruction is [math] variable := expression [/math] An assignment instruction is well formed if the types of the variable and of expression are equal and if all variables are declared in the program.
Axioms
| [math] \qquad\qquad \{x:=\tau\}( \alpha ) \equiv \alpha(x/\tau) \qquad \qquad [/math] |
| [math] \textbf{begin }\, K: M \textbf{ end}\, \alpha \equiv K M\, \alpha [/math] |
How to use these axioms?
We present a lemma that is universally true for all the sublanguages of the language [math]\mathcal{L}_{1}[/math].
[math]\begin{lemma}
Let T be a type. Let x, y, z be variables of type T. The following algorithmic logic is tautology
(x=a \land y=b)\implies \{z:=x;\,x:=y;\,y:=z \}(x=b \land y=a)
\end{lemma}
[/math]
Language [math]\mathcal{L}_{1,c}[/math]
Declarations are declarations of variables of type char. Type char is a finite set of characters. Obviously it contains all letters, digits and delimiters.There are no operations on characters and the only relation in this set is the identity relation =.
Consequently the only characters expressions are charcter constants and character variables.
Example
program print;
begin
end |
Axioms of data structure (type) char.
| [math] \forall_{x \in char}(x='a' \lor x='z') \qquad \qquad [/math] |
| [math] ('a'\neq\, 'b' \land 'a'\neq\, 'b') [/math] |
Language [math]\mathcal{L}_{1,s}[/math]
Declarations are declarations of variables of type string. Type string is an infinite set of finite words over the alfabet of characters. There are no operations on strings and the only relation ...
Consequently the only string expressions are string constants and string variables.
Example
program Strings;
var x,y: string;
begin
x := 'ba'; y := x
end
Language [math]\mathcal{L}_{1,b}[/math]
Declarations are declarations of variables of type boolean. Type char is a finite set of characters. Obviously it contains all letters, digits and delimiters.There are no operations on characters and the only relation in this set is the identity relation =.
Consequently the only characters expressions are charcter constants and character variables.
Example
program Booleans;
var x,y: boolean;
begin
x := 'false'; y := x OR
end
Example
program P2 ;
- var x,y: integer;
begin
- y:=74;
- x:= y+ 8;
end
Grammar
program <name>;
- var id: char; var id1: char;
begin
- id1 := character expression;
- id :=character expression
end
Context free grammar character expression ::= character constant | character variable character constant ::= 'a'| ... |'z'|'A'| ... |'Z'|'+'|'&'| ... character variable :: Well formed expressions
- A character expression <mat>\tau</math> occurring in a program [math]P[/math], is well formed iff either it is a character constant or it is a variable declared in the program.
Axiom
[math]\{x:=\tau\}( \alpha ) \Leftrightarrow \alpha(x/\tau)[/math]
