thodg/slides

Diff from 32e2b29ceb428d01b211b966e638e18a71ecfb59 to master


diff --git a/Makefile b/Makefile
index f2ec9a6..b4a994e 100644
--- a/Makefile
+++ b/Makefile
@@ -3,12 +3,21 @@ FONTSIZE = 8pt
 
 MD = \
 	bsd \
+	language \
+	modal-logic \
 	pandoc \
 	railsonlisp \
 	test
 
 TEX =
 
+PDF = \
+	bsd.pdf \
+	language.pdf \
+	pandoc.pdf \
+	railsonlisp.pdf \
+	test.pdf
+
 all: pdf
 
 clean:
@@ -18,10 +27,6 @@ clean:
 %.pdf: %/index.md
 	cd "${@:%.pdf=%}" && pandoc -st beamer -V theme:${THEME} -V fontsize:${FONTSIZE} -o ../$@ -f gfm index.md
 
-PDF = \
-	${MD:%=%.pdf} \
-	${TEX:%=%.tex.pdf}
-
 pdf: ${PDF}
 
 .PHONY: all clean 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
new file mode 100644
index 0000000..ecabc5a
--- /dev/null
+++ b/modal-logic/index.md
@@ -0,0 +1,53 @@
+# Modal logic
+
+## 1. Notation
+
+### 1.1 ¬A
+"Not 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"
+
+
+## 2. Contruction
+K is a weak logic (Saul Kripke)
+
+### 2.1 Necessitation rule
+A is a theorem of K → □A is a theorem of K
+
+### 2.2 Distribution axiom
+□(A → B) → (□A → □B)
+
+### 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