Axiomatic definition of Loglan'82: Różnice pomiędzy wersjami
(→\mathcal{L}_{1} Declarations of variables. Assignment instructions) |
|||
| Linia 1: | Linia 1: | ||
| − | On these pages we are sketching, in an incremental way, an axiomatic semantics of Loglan'82. | + | On these pages we are sketching, in an incremental way, an axiomatic semantics of Loglan'82.<br /> |
| − | + | ''' | |
| + | Axiomatic definitions of sublanguages of Loglan'82''' <br /> | ||
| + | |||
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. | 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 /> | Program in Loglan'82 has the following structure<br /> | ||
| Linia 27: | Linia 29: | ||
This allow us to define the first sublanguage <math>\mathcal{L}_{0,0}</math> of Loglan'82. | 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> | <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''. | 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:<br /> | 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 /> | writeln; <br /> | ||
| Linia 53: | Linia 55: | ||
Each output instruction appends a string of characters to the standard output. | 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.<br /> | 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.<br /> | ||
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 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> | ||
| − | + | === Language <math>\mathcal{L}_{1,c}</math> === | |
Declarations are declarations of variables of type char. | Declarations are declarations of variables of type char. | ||
'''Example'''<br /> | '''Example'''<br /> | ||
| Linia 79: | Linia 81: | ||
<math>\{x:=\tau\}( \alpha ) \Leftrightarrow \alpha(x/\tau)</math> | <math>\{x:=\tau\}( \alpha ) \Leftrightarrow \alpha(x/\tau)</math> | ||
| − | + | == <math>\mathcal{L}_{2}</math> Conditional instructions == | |
| − | + | == <math>\mathcal{L}_{3}</math> Arrays and '''for''' instructions == | |
| − | + | == <math>\mathcal{L}_{4}</math> Iteration instructions == | |
Wersja z 16:11, 16 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]
| 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]
Language [math]\mathcal{L}_{1,c}[/math]
Declarations are declarations of variables of type char.
Example
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]
