Axiomatic definition of Loglan'82 - Historia wersji

AndrzejSalwicki: /* \mathcal{L}_{4} Iteration instructions */

2015-10-25T21:29:51Z

‎\mathcal{L}_{4} Iteration instructions

2015-10-25T21:01:37Z

‎Language \mathcal{L}_{1,c}

2015-10-25T17:55:19Z

‎\mathcal{L}_{1} Declarations of variables. Assignment instructions

2015-10-25T05:27:06Z

‎\mathcal{L}_{1} Declarations of variables. Assignment instructions

2015-10-24T12:11:27Z

‎\mathcal{L}_{1} Declarations of variables. Assignment instructions

2015-10-24T12:08:58Z

‎\mathcal{L}_{1} Declarations of variables. Assignment instructions

2015-10-24T12:06:49Z

‎\mathcal{L}_{1} Declarations of variables. Assignment instructions

2015-10-24T12:02:06Z

‎Language \mathcal{L}_{1,c}

2015-10-24T11:58:34Z

‎Language \mathcal{L}_{1,c}

2015-10-24T11:52:29Z

‎Language \mathcal{L}_{1,c}

@@ Linia 228: / Linia 228: @@
 == <math>\mathcal{L}_{2}</math> Conditional instructions ==
 == <math>\mathcal{L}_{3}</math> Arrays and '''for''' instructions ==
 == <math>\mathcal{L}_{4}</math> Iteration instructions ==

@@ Linia 135: / Linia 135: @@
 {| class="wikitable"
 |-
-|style="background-color:#FFCC99" | '''program''' print; <br />
+|style="background-color:#FFCC99" |
-:'''var''' x: char;<br />
+'''program''' characters;<br />
-:'''var''' y,z: char
+: '''var''' c1,c2,c3:char<br />
-'''begin''' <br />
+'''begin'''<br />
-:x := 'a'; <br />
+:c1:='p';<br />
-:y := x;<br />
+:c2:='d';<br />
-:write("Today is: May"); write(22); write(x,'d'); writeln <br />
+:writeln(c1,c2); <br />
-'''end''' <br/>
+:c3:=c1; <br />
 |}
 Axioms of data structure (type) '''char'''.
 {| class="wikitable"

@@ Linia 98: / Linia 98: @@
 |+ Axiom of composed instruction
 |-
-| 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 />

@@ Linia 71: / Linia 71: @@
 | style="background-color:palegreen" | ''program''
 | style="background-color:GoldenRod" | '''program''' <''name''>;<br />
 :<''declarations of variables''><br />
 '''begin'''<br />
+:<''instructions''> i.e.<br />
-:<''assignment instructions''><br />
+:: sequence of <br />
+::<''output instructions'' or ''assignment instructions'' >
 '''end'''
 |}

@@ Linia 118: / Linia 118: @@
    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;\}(x=b \land z=a) </math> <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 />

@@ Linia 112: / Linia 112: @@
 <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) \cond \{\underbrace{z:=x;\, x:=y;}_{K}\,
+<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) \cond \overbrace{\{z:=x;\, x:=y\}}^{K} \overbrace{\underbrace{\{
+<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 />

@@ Linia 129: / Linia 129: @@
 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 />
 {| class="wikitable"
 |-
-|style="background-color:#FFCC99" | program print; <br />
+|style="background-color:#FFCC99" | '''program''' print; <br />
-:var x: char;<br />
+:'''var''' x: char;<br />
-:var y,z: char
+:'''var''' y,z: char
-begin <br />
+'''begin''' <br />
-:x := 'a' <br />
+:x := 'a'; <br />
-:y := x
+:y := x;<br />
 :write("Today is: May"); write(22); write(x,'d'); writeln <br />
-end <br/>
+'''end''' <br/>
 |}
 Axioms of data structure (type) '''char'''.
@@ Linia 154: / Linia 154: @@
 |+ Axioms of identitities of char constants
 |-
-| style="color:Blue" | <math>  (('a'\neq\, 'b') \land ('a'\neq\, 'b')\land \dots )  </math>
+| style="color:Blue" | <math>  (('a'\neq\, 'b') \land ('a'\neq\, 'c')\land \dots )  </math>
 |}
 Also this line can be completed without problems.

@@ Linia 147: / Linia 147: @@
 |+ Axiom enumerating the type char
 |-
-| style="color:Blue" | <math>  \forall_{x \in char}(x=’a’ \lor x=’z’) \qquad \qquad </math>
+| 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>
 |}
+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\, 'b')  </math>
+| style="color:Blue" | <math>  (('a'\neq\, 'b') \land ('a'\neq\, 'b')\land \dots )  </math>
 |}
 -----