thodg/slides

Diff from 955b11036a9990385e5b43118fd7b1bc247bdd9e to master


diff --git a/Makefile b/Makefile
index 69bbbe2..b4a994e 100644
--- a/Makefile
+++ b/Makefile
@@ -3,6 +3,7 @@ FONTSIZE = 8pt
 
 MD = \
 	bsd \
+	language \
 	modal-logic \
 	pandoc \
 	railsonlisp \
@@ -12,6 +13,7 @@ TEX =
 
 PDF = \
 	bsd.pdf \
+	language.pdf \
 	pandoc.pdf \
 	railsonlisp.pdf \
 	test.pdf
diff --git a/README.md b/README.md
index 3f76c39..0d337c0 100644
--- a/README.md
+++ b/README.md
@@ -11,17 +11,17 @@ with
 
 ### Pandoc
 A few examples of Pandoc usage to generate Beamer presentations from Markdown syntax.
-[Markdown](https://github.com/thodg/slides/blob/master/pandoc/index.md)
-[PDF](https://github.com/thodg/slides/blob/master/pandoc.pdf)
+[Markdown](https://git.kmx.io/thodg/slides/_tree/master/pandoc/index.md)
+[PDF](https://git.kmx.io/thodg/slides/_blob/master/pandoc.pdf)
 
 ## 2019
 
 ### BSD
 About *BSD and UNIX history.
-[Markdown](https://github.com/thodg/slides/blob/master/bsd/index.md)
-[PDF](https://github.com/thodg/slides/blob/master/bsd.pdf)
+[Markdown](https://git.kmx.io/thodg/slides/_tree/master/bsd/index.md)
+[PDF](https://git.kmx.io/thodg/slides/_blob/master/bsd.pdf)
 
 ### RailsOnLisp
 An introduction to Common Lisp and RailsOnLisp.
-[Markdown](https://github.com/thodg/slides/blob/master/railsonlisp/index.md)
-[PDF](https://github.com/thodg/slides/blob/master/railsonlisp.pdf)
+[Markdown](https://git.kmx.io/thodg/slides/_tree/master/railsonlisp/index.md)
+[PDF](https://git.kmx.io/thodg/slides/_blob/master/railsonlisp.pdf)
diff --git a/bsd/index.md b/bsd/index.md
index 133e6d3..cb7c103 100644
--- a/bsd/index.md
+++ b/bsd/index.md
@@ -12,42 +12,42 @@ https://kmx.io/
 
 ### Diagram
 
-![UNIX](unix-history.png)
+![UNIX](https://git.kmx.io/thodg/slides/_blob/master/bsd/unix-history.png)
 
 ### Multics
 
-1960  
+1960
 
 Companies
 
   - MIT
-  
+
   - AT\&T Bell labs
-  
+
   - General Electric
 
 ### UNIX
 
-AT\&T Bell Labs 1970  
+AT\&T Bell Labs 1970
 
 Developers
 
   - Ken Thompson
-  
+
   - Dennis Ritchie
 
 ### Berkeley Unix
 
-1974  
+1974
 
 Licensed by AT\&T
 
 ### Berkeley Software Distribution
 
-1979  
+1979
 
   - `vi`
-  
+
   - `csh`
 
 Licensed by AT\&T
@@ -56,7 +56,7 @@ Licensed by AT\&T
 
     Copyright (c) <year> <copyright holder>.
     All rights reserved.
-    
+
     Redistribution and use in source and binary forms are permitted
     provided that the above copyright notice and this paragraph are
     duplicated in all such forms and that any documentation,
@@ -71,12 +71,12 @@ Licensed by AT\&T
 
 ### Net/1
 
-June 1989  
+June 1989
 
 Basis for
 
   - NetBSD
-  
+
   - FreeBSD
 
 Under BSD License
diff --git a/language.pdf b/language.pdf
new file mode 100644
index 0000000..0629d74
Binary files /dev/null and b/language.pdf differ
diff --git a/language/index.md b/language/index.md
new file mode 100644
index 0000000..b06c5f8
--- /dev/null
+++ b/language/index.md
@@ -0,0 +1,70 @@
+Language
+
+Thomas de Grivel <thoxdg@gmail.com>
+
+https://kmx.io/
+
+2020-05-17
+
+# Language
+
+## Structure
+
+### Three components
+
+Any formal language usable with a model is composed of three things :
+
+ - A schema (or grammar)
+ - Semantics
+ - Data
+
+### Schema
+
+In model theory a schema allows you to define an ontology,
+that is a definition of what can and cannot be expressed in your
+language.
+
+It is a set of rules which make any pattern part of the language or not.
+
+The most used schemas for formal language definition are grammars.
+
+The schema is a generalistic view of all the data that can be
+expressed in the language.
+
+It can be a relative process where parts of the structure of the
+language are combined to form a more complex schema, e.g. a
+grammar made of simpler rules.
+
+### Semantics
+
+Semantics tell you the meaning of the language. They describe
+how to translate your language into another one.
+
+This is a relative process : a semantic is from a language to another,
+even if it is the same language acting as source and destination
+language.
+
+Semantics give meaning to your language which otherwise is just another
+data model.
+
+A number of programming languages also export the semantics of
+lower-level constructs such as mathematical operations from the processor
+or disk access from the kernel.
+
+Semantics tells you how your language relates to other languages.
+It is a connection to other languages.
+
+### Data
+
+Data is valid use of the language for reasons pertaining to its
+semantics.
+
+It is a direct application of the language schema.
+
+Semantics are appliable to all data.
+
+Data is a choice from the possibilities of the language schema
+driven by the semantics of the language.
+
+Each datum represents a single valid use of the language and can
+be uniquely identified.
diff --git a/modal-logic/index.md b/modal-logic/index.md
index 75f2f81..ecabc5a 100644
--- a/modal-logic/index.md
+++ b/modal-logic/index.md
@@ -1,13 +1,31 @@
 # Modal logic
 
 ## 1. Notation
-¬A   "Not A"
 
-□A    "It is necessary that A"
+### 1.1 ¬A
+"Not A"
 
-◊A    "It is possible that A"
+### 1.2 □A
+"It is necessary that A"
+
+### 1.3 ◊A
+"It is possible that A"
+
+### 1.4 A → B
+"If A then B"
+
+### 1.5 A ∧ B
+"A and B"
+
+### 1.6 A ∨ B
+"A or B"
+
+### 1.7 A ⊕ B
+"A xor B"
+
+### 1.8 A ↔ B
+"If A then B and if B then A"
 
-A → B "If A then B"
 
 ## 2. Contruction
 K is a weak logic (Saul Kripke)
@@ -18,7 +36,18 @@ A is a theorem of K → □A is a theorem of K
 ### 2.2 Distribution axiom
 □(A → B) → (□A → □B)
 
-## 3. T
+### 2.3 Operator ◊
+◊A = ¬□¬A
+
+## 3. Lemmas
+
+### 3.1 Necessary conjunction
+□(A ∧ B) ↔ □A ∧ □B
+
+### 3.2 Disjonction of necessities
+◻A ∨ ◻B → □(A ∨ B)
+
+## 4. T
 T is K plus the following axiom :
 
 □A → A