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

Z Lem
Skocz do: nawigacji, wyszukiwania
(→‎Language \mathcal{L}_{0,1})
(→‎\mathcal{L}_{4} Iteration instructions)
 
(Nie pokazano 36 pośrednich wersji utworzonych przez tego samego użytkownika)
Linia 71: Linia 71:
 
| style="background-color:palegreen" | ''program''
 
| style="background-color:palegreen" | ''program''
 
| style="background-color:GoldenRod" | '''program''' <''name''>;<br />
 
| style="background-color:GoldenRod" | '''program''' <''name''>;<br />
−
 
 
:<''declarations of variables''><br />
 
:<''declarations of variables''><br />
−
 
 
'''begin'''<br />
 
'''begin'''<br />
−
 
+
:<''instructions''> i.e.<br />
−
:<''assignment instructions''><br />
+
:: sequence of <br />
−
 
+
::<''output instructions'' or ''assignment instructions'' >
 
'''end'''
 
'''end'''
−
 
 
|}
 
|}
  
Linia 85: Linia 82:
  
 
The ''declarations'' and ''instructions'' are  finite sequences of declarations and instructions respectively, empty squence included.
 
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<br />
  
 +
{| class="wikitable"
 +
|+ Axiom of assignment instruction
 +
|-
 +
| style="color:Blue" | <math> \qquad\qquad \{x:=\tau\}( \alpha ) \equiv \alpha(x/\tau) \qquad \qquad </math>
 +
|}
 +
 +
 +
{| class="wikitable"
 +
|+ Axiom of composed instruction
 +
|-
 +
| 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>.<br />
 +
{| class="wikitable"
 +
|-
 +
| style="background-color:palegreen" |
 +
|'''Lemma''' <br />
 +
Let <math> T </math> be a type. Let <math>x, y, z</math> be variables of type <math>T</math>. The following algorithmic formula is tautology
 +
<math> (x=a \land y=b)\implies \{z:=x;\,x:=y;\,y:=z \}(x=b \land y=a) </math> <br />
 +
'''Proof'''. By the axiom of composed instruction and propositional calculus our formula<br />
 +
<math> (x=a \land y=b) \implies \{\underbrace{z:=x;\, x:=y;}_{K}\,
 +
  \underbrace{y:=z}_{M}\}\underbrace{(x=b \land y=a)}_{\alpha} </math> <br />
 +
is equivalent to <br />
 +
<math> (x=a \land y=b) \implies \overbrace{\{z:=x;\, x:=y\}}^{K} \overbrace{\underbrace{\{
 +
  y:=z\}}_{y:=z}}^{M}\underbrace{(x=b \land y=a)}_{\alpha(y)} </math> <br />
 +
Using the axiom of assignment instruction we get an equivalent formula <br />
 +
<math> (x=a \land y=b)\implies \{z:=x;\,x:=y;\}\underbrace{(x=b \land z=a)}_{\alpha(y/z)} </math> <br />
 +
Again the axiom of composed instruction <br />
 +
<math> (x=a \land y=b)\implies \{z:=x\} \{x:=y;\}(x=b \land z=a) </math> <br />
 +
Now, by applying twice the axiom of assignment instruction we get<br />
 +
<math> (x=a \land y=b)\implies \{z:=x\} (y=b \land z=a) </math> <br />
 +
and <br />
 +
<math> (x=a \land y=b)\implies (y=b \land x=a) </math> <br />
 +
The last formula is tautology. All formulas are equivalent. Hence, our first formula is proved.
 +
|}
 +
-----
 +
Note, the meaning of the lemma is ''if initially the value of x is a and the value of y is b, then after execution of these three instructions the variables swapped their values x=b and y=a ''
 
=== 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.
 
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 =.
 
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.
+
Consequently the only characters expressions are character constants and character variables.
 
   
 
   
 
'''Example'''<br />
 
'''Example'''<br />
 +
{| class="wikitable"
 +
|- 
 +
|style="background-color:#FFCC99" |
 +
'''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.
  
−
program Characters;
+
Axioms of data structure (type) '''char'''.
−
  var x,y: char;
+
{| class="wikitable"
−
begin
+
|+ Axiom enumerating the type char
−
  x := 'a';
+
|-
−
  y := x
+
| style="color:Blue" | <math>  \forall_{x \in char}(x=’a’\lor \dots \lor x=’z’ \lor x='A' \lor \dots x='Z' \lor \dots) </math>
−
end
+
|}
 +
The reader is kindly requested to complete the above line.
 +
 
 +
{| class="wikitable"
 +
|+ Axioms of identitities of char constants
 +
|-
 +
| style="color:Blue" | <math>  (('a'\neq\, 'b') \land ('a'\neq\, 'c')\land \dots )  </math>
 +
|}
 +
Also this line can be completed without problems.
 
-----
 
-----
 +
 
=== Language <math>\mathcal{L}_{1,s}</math> ===
 
=== Language <math>\mathcal{L}_{1,s}</math> ===
 
Declarations are declarations of variables of type string.
 
Declarations are declarations of variables of type string.
Linia 163: Linia 228:
 
== <math>\mathcal{L}_{2}</math> Conditional instructions ==
 
== <math>\mathcal{L}_{2}</math> Conditional instructions ==
 
== <math>\mathcal{L}_{3}</math> Arrays and '''for''' instructions ==
 
== <math>\mathcal{L}_{3}</math> Arrays and '''for''' instructions ==
 +
== <math>\mathcal{L}_{4}</math> Iteration instructions ==
 +
We extend the language by admitting the instruction while and its cousins
 +
== <math>\mathcal{L}_{5}</math> Definitions ==
 +
This language allows to use subprograms - non-recursive ones
 +
== <math>\mathcal{L}_{6}</math> Primitive recursion ==
 +
Theorem of Julia Robinson, Stephen Kleene on reducing primitive recursion to while programs
 +
== <math>\mathcal{L}_{7}</math> Functions and procdures ==
 +
The general case of modules that define algorithms for multiple use
 +
== <math>\mathcal{L}_{8}</math> Functionals ==
 +
Functions that allow other functions as parameters
 +
== <math>\mathcal{L}_{9}</math> Classes and objects ==
 +
obvious
 +
== <math>\mathcal{L}_{10}</math> Inheritance ==
 +
bbb
 +
== <math>\mathcal{L}_{11}</math> Coroutines ==
 +
== <math>\mathcal{L}_{12}</math> Signals and Exceptions ==
 +
== <math>\mathcal{L}_{13}</math> Processes and active objects of processes ==
 +
== <math>\mathcal{L}_{14}</math> Software engineering ==
 +
A case study of bank simulation
 +
== <math>\mathcal{L}_{4}</math> Iteration instructions ==
 +
== <math>\mathcal{L}_{4}</math> Iteration instructions ==
 
== <math>\mathcal{L}_{4}</math> Iteration instructions ==
 
== <math>\mathcal{L}_{4}</math> Iteration instructions ==

Aktualna wersja na dzień 22:29, 25 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.

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,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

write("hallo world!"); writeln;
write("Today is: May"); write(22); write(2014); writeln

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:

Program
definiendum definiens
program program <name>;
<declarations of variables>

begin

<instructions> i.e.
sequence of
<output instructions or assignment 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. 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

Axiom of assignment instruction
[math] \qquad\qquad \{x:=\tau\}( \alpha ) \equiv \alpha(x/\tau) \qquad \qquad [/math]


Axiom of composed instruction
[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].

Lemma

Let [math] T [/math] be a type. Let [math]x, y, z[/math] be variables of type [math]T[/math]. The following algorithmic formula is tautology [math] (x=a \land y=b)\implies \{z:=x;\,x:=y;\,y:=z \}(x=b \land y=a) [/math]
Proof. By the axiom of composed instruction and propositional calculus our formula
[math] (x=a \land y=b) \implies \{\underbrace{z:=x;\, x:=y;}_{K}\, \underbrace{y:=z}_{M}\}\underbrace{(x=b \land y=a)}_{\alpha} [/math]
is equivalent to
[math] (x=a \land y=b) \implies \overbrace{\{z:=x;\, x:=y\}}^{K} \overbrace{\underbrace{\{ y:=z\}}_{y:=z}}^{M}\underbrace{(x=b \land y=a)}_{\alpha(y)} [/math]
Using the axiom of assignment instruction we get an equivalent formula
[math] (x=a \land y=b)\implies \{z:=x;\,x:=y;\}\underbrace{(x=b \land z=a)}_{\alpha(y/z)} [/math]
Again the axiom of composed instruction
[math] (x=a \land y=b)\implies \{z:=x\} \{x:=y;\}(x=b \land z=a) [/math]
Now, by applying twice the axiom of assignment instruction we get
[math] (x=a \land y=b)\implies \{z:=x\} (y=b \land z=a) [/math]
and
[math] (x=a \land y=b)\implies (y=b \land x=a) [/math]
The last formula is tautology. All formulas are equivalent. Hence, our first formula is proved.

Note, the meaning of the lemma is if initially the value of x is a and the value of y is b, then after execution of these three instructions the variables swapped their values x=b and y=a

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 character constants and character variables.

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.

Axioms of data structure (type) char.

Axiom enumerating the type char
[math] \forall_{x \in char}(x=’a’\lor \dots \lor x=’z’ \lor x='A' \lor \dots x='Z' \lor \dots) [/math]

The reader is kindly requested to complete the above line.

Axioms of identitities of char constants
[math] (('a'\neq\, 'b') \land ('a'\neq\, 'c')\land \dots ) [/math]

Also this line can be completed without problems.

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]

[math]\mathcal{L}_{2}[/math] Conditional instructions

[math]\mathcal{L}_{3}[/math] Arrays and for instructions

[math]\mathcal{L}_{4}[/math] Iteration instructions

We extend the language by admitting the instruction while and its cousins

[math]\mathcal{L}_{5}[/math] Definitions

This language allows to use subprograms - non-recursive ones

[math]\mathcal{L}_{6}[/math] Primitive recursion

Theorem of Julia Robinson, Stephen Kleene on reducing primitive recursion to while programs

[math]\mathcal{L}_{7}[/math] Functions and procdures

The general case of modules that define algorithms for multiple use

[math]\mathcal{L}_{8}[/math] Functionals

Functions that allow other functions as parameters

[math]\mathcal{L}_{9}[/math] Classes and objects

obvious

[math]\mathcal{L}_{10}[/math] Inheritance

bbb

[math]\mathcal{L}_{11}[/math] Coroutines

[math]\mathcal{L}_{12}[/math] Signals and Exceptions

[math]\mathcal{L}_{13}[/math] Processes and active objects of processes

[math]\mathcal{L}_{14}[/math] Software engineering

A case study of bank simulation

[math]\mathcal{L}_{4}[/math] Iteration instructions

[math]\mathcal{L}_{4}[/math] Iteration instructions

[math]\mathcal{L}_{4}[/math] Iteration instructions

Źródło „http://lem12.uksw.edu.pl/index.php?title=Axiomatic_definition_of_Loglan%2782&oldid=2015”