Logic

• ∃ was introduced by Peano
• ∀ was introduced by Gentzen (after ∃)
• natural deduction, rules come in pairs (introduction,elimination)
• Sentential logic: another name for Boolean logic ⁵
• Subjunction: Something like 'implies' or 'if-then'

• Contrapositive: a rule by which the antecedent and consequent of an implication are inverted and switched.
  • Eg: (p → q) → (~q → ~p)

• Transposition: a rule by which we can switch the antecedent and consequent of an implication.
  • Eg: (p → q) ↔︎ (~q → ~p)

Propositions as types

From one of Philip Wadler's talks:

STLC: Curry style and Church style

UTLC functions have no fixed domain and range.

Both Curry and Church came up with typed versions of their lambda calculus systems:

• Curry style
• Church style

https://ncatlab.org/nlab/show/intrinsic+and+extrinsic+views+of+typing

CoC (and hence CIC) is in Church style.

type := Type
      | type → type

(→ associates to the right.)

Values of Type are type variables.

where all τᵢ are of values of type type.

Heyting algebra

• ∪, ∩ are commutative and associative

• ∪ distributes over ∩, ∩ distributes over ∪

• a ∪ 0 = a, a ∩ 1 = a

• 0 is like False / fallacy.

• 1 is like True / tautology.

BHK: Classical interpretation

• Brouwer-Heyting-Kolmogorov interpration: assign a set of proofs to the formula
  • formula is true iff it has a proof
• Tarski-an interpretation: interpretation of a formula is either 'true' or 'false'.
• Classical vs intuitionistic logic:
  • Classical: Existence is proof
  • Construction: Construction is proof??
• Constructive programming: Programming is replaced by proving.

Ref: Classical Brouwer-Heyting-Kolmogorov interpretation - Sata, Masahiko: https://repository.kulib.kyoto-u.ac.jp/dspace/bitstream/2433/61685/1/1021-3.pdf

Peirce's law

Named after the logician Charles Peirce.

((p -> q) -> p) -> p

Truth table:

| p | q | p -> q | (p->q) -> p | ((p -> q) -> p) -> p |
|---+---+--------+-------------+----------------------|
| 0 | 0 |      1 |           0 |                    1 |
| 0 | 1 |      1 |           0 |                    1 |
| 1 | 0 |      0 |           1 |                    1 |
| 1 | 1 |      1 |           1 |                    1 |

Peirce's law is equivalent to law of excluded middle when q is made ¬p:

| ((p -> ¬p) -> p) -> p      |                          |
| ((¬p ∨ p) -> p) -> p       | (p->q) ≡ (¬p ∨ q)        |
| (¬(¬p ∨ p) ∨ p) -> p       | (p->q) ≡ (¬p ∨ q)        |
| ((p ∧ ¬p) ∨ p) -> p        | ∨ distr, double negation |
| ¬((p ∧ ¬p) ∨ p) ∨ p        | (p->q) ≡ (¬p ∨ q)        |
| (¬(p ∧ ¬p) ∧ ¬p) ∨ p       | double negation          |
| ((¬p ∨ p) ∧ ¬p) ∨ p        | double negation          |
| ((¬p ∧ ¬p) ∨ (p ∧ ¬p)) ∨ p | ∧ distr                  |
| ¬p ∨ p                     | double negation          |
| p ∨ ¬p                     | ∨ comm                   |

Assumes double negation rule (ie, ¬¬p ≡ p). But it's classical logic anyway, since we are deriving law of excluded middle.

Minimal logic

https://en.wikipedia.org/wiki/Minimal_logic

Doesn't have:

• law of excluded middle (p ∨ ¬p)
• principle of explosion (∀x, ⊥ → x)
  • Anything can be proven from a contradiction.

'Systems'

• System LK (Gentzen)
• System LJ (A modification of LK)
• System F (Polymorphism)
• System T (Gödel?)

Order of quantifier matters

• In ∀x, ∃y, means x is fixed first, and y is chosen later.
• In ∃y, ∀x, means y is fixed first, and x is chosen later.

For example,

∀x:country, ∃y:city,
  y = capital(x)

means 'every country has a city as its capital'

∃y:city, ∀x:country,
  y = capital(x)

means 'there is some city which is the capital of all countries'.

Sequent calculus

A style of formal logical argumentation in which every line of proof is a conditional tautology (known as sequent).

• More suited for theoretical analysis.
  • Natural deduction more suited for practical theorem proving.
• Sequent calculus is a Gentzen style system, like natural deduction.
  • But unlike natural deduction, which can have only one conclusion per line, sequent calculus can have one or more conclusions per line.

Inference rules

Left ∧ rule (L ∧):

Γ,A∧B ⊢ Δ
=========
Γ,A,B ⊢ Δ


Left ∨ rule (L ∨):

    Γ,A∨B ⊢ Δ
=================  
Γ,A ⊢ Δ   Γ,B ⊢ Δ


Left → rule: (DOUBT: How does this one come about??)

Γ,A→B ⊢ Δ
=========


Left ¬ rule: (DOUBT: How does this one come about??)

Γ,¬A ⊢ Δ
========
Γ ⊢ Δ,A

Cut rule in sequent calculus

• An inference rule in sequent calculus.
• Something like a broader/generalized form of modus ponens rule.

If a formula A appears as a conclusion of one proof and appears as a hypothesis of another proof, a third proof can be deduced in which the formula A does not even appear (ie, A is eliminated).

  Γ ⊢ A,Δ   Γ',A ⊢ Δ'
======================
     Γ,Γ' ⊢ Δ,Δ'

Hilbert style proof systems

• Every line of the proof is an unconditional tautology (ie, a theorem).
• Has small number of inference rules, more number of axioms.
  • Unlike Gentzen style systems, which have few axioms and more inference rules.

Continuation Passing Style (CPS)

• Used by smlnj internally.

Reference: Compiling with continuations - Andrew Appel

Proposition

Informally speaking,

A proposition is a 'sentence' for which 'it makes sense' to ask if it is true or false.

Reference: Applied abstract algebra (2e) - Rudolf Lidl, Günter Pilz

Skolemization

• A process of removing existential quantifiers from a first order formula.
  • By introducing new function symbols if needed.
• The result would be in Skolem normal form.
• Needn't be equivalent to the original formula, but result is SAT only if the original formula is SAT.
  • ie, result of skolemization is equisatisfiable with the original formula.
• Dual of skolemization is Herbrandization.

An example ¹⁶:

Formula: Every philosopher has written at least one book.
ie, for each philosopher, there exists a book that is written by that philosopher.

∀p, Philo(p) -> (∃b [book(b) ∧ write(p, b)])

Rewriting the implication,

∀p, ¬ Philo(p) ∨ (∃b [book(b) ∧ write(p, b)])

There exists a b for a given p means we can have a function g that maps any given p to its b. 
This part is the skolemization.

∀p, ¬ Philo(p) ∨ [book(g(p)) ∧ write(p, g(p))]

Another example ¹⁶:

∀p ∀s, philo(p) ∧ studentOf(p, s) -> ∃b, book(b) ∧ write(p, b) ∧ read(s, b)

Rewriting the implication,

∀p ∀s, ¬ [philo(p) ∧ studentOf(p, s)] ∨ [∃b, book(b) ∧ write(p, b) ∧ read(s, b)]

From de-Morgan's law,

∀p ∀s, [¬philo(p) ∨ ¬studentOf(p, s)] ∨ [∃b, book(b) ∧ write(p, b) ∧ read(s, b)]

There exists a book for a given philosopher p that one of his students s read. We can have a function g mapping a given p and s to a b.
Skolemizing,

∀p ∀s, [¬philo(p) ∨ ¬studentOf(p, s)] ∨ [book(g(p,s)) ∧ write(p, g(p,s)) ∧ read(s, g(p,s))]

Linear logic

Proposed by Jean-Yves Girard.

tm := p        | ¬p
    | p ⊕ p    | p ⊗ p
    | p & p    | p ⅋ p
    | 0        | 1
    | ⊤        | ⊥
    | !p       | ?p

Nature of connectives:

• Exponentials: !, ?
• Multiplicative: ⨂, ⅋, 1
• Additive: ⨁, &, 0

Names:

• &: with
• ⅋: par
• !: bang
• ?: quest

Lollipop is a derived connective: p ⊸ q ≡ ¬p ⅋ q

Affine logic

• Like a 'weakened' linear logic.
• Each resource can be used atmost once.
  • Ie, can also be left unused.
  • Or to put it in other words, resource can be discarded instead of being used.
• Unlike linear logic, where each resource has to be used exactly once ʷ

Leibniz's equality

x = y iff P(x) = P(y) for all predicates. ʷ

Type theory

• Types are 'specs' for values. ¹
• Compilers ensure that these specs are adhered to.
• Π-calculus: a popular core language for defining semnatics of message-based concurrent languages.
• type reconstruction: another name for 'type inference'.
  • Compiler fills in type information that has been left out by the programmer.

Type variable example

From 22.2 of TAPL book (page 319):

λf:X→X.
  λa:X.
    f (f a)

where X is a type variable.

Two abstractions. So, two arguments:

1. f : X → X
2. a : X

Final value type: X

As in

f (f a)
|  |  |
|  +--+
|    |
|    X
|    |
+----+
   |
   X

So the type of the initial term is:

(X → X) → X -> X
|     |   |    |
+-----+   |    |
   |      |    |
   f      a  return value

Holding type variable abstract like this allows for parametric polymorphism.

Most general instance

Makes smallest commitment about the values of type variables that yields a well-typed term.

Example

Consider a term:

λf:Y.
λa:X.
f (f a)

This by itself can't be said to be well typed. Because f is of type Y when it has got to accept a : X as argument.

But if we change Y to be X → X, to make it

λf:X → X.
λa:X.
f (f a)

we could say that the term is well-typed, but without yet giving a concrete value for the type variable X. Its type is: (X → X) → X → X.

So, the latter is the 'most general instance' of the former. Smallest commitment regarding values of type variables that yields a well-typed term.

We could say that type inference (aka type reconstruction) is the search for a valid instantiation of type variables.

λf:Y .
λa:X .
f (f a)

Fixed point of functions

x is a fixed point of a function f if:

f(x) = x

Example:

Any function definable in lambda calculus has a fixed point, which itself is definable in labmda calculus. ⁸

Computer Science

Church-Turing thesis

• Entscheidungsproblem is undecidable.
  • German for 'decision problem'
• Church's lambda calculus and Turing machines are equivalent.
  • Both formalize the meaning of computation.
• Some decision problems are undecidable.
  • There's no general algorithm that works every time.
  • https://en.wikipedia.org/wiki/Turing%27s_proof
• Alan Turing worked on Turing machines.
• Alonzo Church worked on lambda calculus.

Informally speaking, Church-Turing thesis says:that both Turing machines and lambda calculus represent computations.

Reference: https://www.cs.cornell.edu/courses/cs3110/2021sp/textbook/adv/curry-howard.html

Entscheidungsproblem

• Accept a statement as input and find an algorithm that check if the statement holds in the given axiom system.
  • ie, whether the statement is valid in every structure satisfying the axioms.
  • An algorithm that can give a yes/no answer.

Church-Rosser theorem

Related to lambda calculus.

If two different β-reductions upon a term terminate, then they terminate in the same term.

   e1
 ↗   ↘
e     e'
 ↘   ↗
   e2 

References:

• https://www.cse.iitk.ac.in/users/karkare/Talks/FPIntro.pdf
• https://en.wikipedia.org/wiki/Church%E2%80%93Rosser_theorem

Logic

Red-black trees

• A balanced binary search tree (that means elements are sorted).
• Better performance than AVL trees.

From here:

• Root is black
• Leaves are black
• Children of a red node are black
• Path from any node to a leaf has same number of black nodes

             B        
             |
     +-------+------+
     |              |
     R              B
     |              |
+----+----+         +-----+
|         |               |
B         B               R

Compilers

Kripke structures

Basically the state diagrams used in model checking books.

Pronounced /ˈkrɪpki/.

Finite automata vs Finite state machine

Apparently the same?? Not sure…

https://stackoverflow.com/questions/22354706/can-anyone-please-explain-difference-between-finite-state-machine-and-finite-aut

Primitive recursive functions

Functions which are known to terminate.

As in a loop whose maximum possible number of iterations is known before entering the loop.

(Gödel called this just 'recursive functions'. Kleene kind of renamed it.)

Petrinet

• Can model distributed systems.

  • Advantage: Can be given a formal semantics of system execution.
  • Can have multiple concurrent activities, unlike a finite automaton where at a time there is only one 'activity'. ʳ

• Named after German computer scientist Carl Adam Petri. ʷ

• A directed bipartite graph

• Two kinds of nodes

  • Places (white circle)
  • Transitions (rectangles)

• Arcs connect places and transitions.

  • There can be no arcs between nodes of the same type (ie, between two places or two transitions).

• A place can contain tokens (black small circles within place).

• A transition is enable if all places connected as input to it has at least one token each.

• Non-deterministic behaviour.

  • If multiple transitions are enabled, the order in which they fire is not predetermined.

• See some example petrinets here.

Definition:

(P, T, F)

where:

• P: set of places
• T: set of transitions
• F: set of arcs
  • F = (P⨯T) ∪ (T⨯P)

Variants of Petrinet:

• Timed/untimed
• Coloured

Electronics

Register retiming

Move registers to decrease the time for the critical path so that frequency may be increased.

Retiming is possible only when there is sufficient slack.

+--+   /-----\   /-----\   +--+   +--+
|R1|---| OP1 |->-| OP2 |->-|R2|->-|R3|
+--+   \-----/   \-----/   +--+   +--+
         10ns      20ns               

where the 'R's are registers.

In the above case, R1-R2 takes 10ns + 20ns = 30ns whereas R2-R3 takes 0ns (ie, we have a positive slack of 20ns in R2-R3??).

So one clock should be of at least 30ns.

That means ν = 1/(30 * 10⁻⁹) = 33.33MHz

Yet, if OP2 were moved to R2-R3,

+--+   /-----\   +--+   /-----\   +--+
|R1|---| OP1 |->-|R2|->-| OP2 |->-|R3|
+--+   \-----/   +--+   \-----/   +--+
         10ns             20ns        

one clock need be only at least 20ns.

∴ ν = 1/(20 * 10⁻⁹) = 50MHz.

ie, we can get higher frequency of operation.

Distances

Euclidean distance

• aka Pythagorean distance

  |   |   |   |   |   |   |
5-|---|---|---|---|---|---|
  |   |   |   |   |   |   |
4-|---|---|---|---|---|---|
  |   |   |   |   |   |   |
3-|---|---|---|---▄---|---|
  |   |   |   | ▄▀|   |   |
2-|---|---|---▄▀--|---|---|
  |   |   | ▄▀|   |   |   |
1-|---|---▄▀--|---|---|---|
  |   | ▄▀|   |   |   |   |
0-|---|▀--|---|---|---|---|
  0   1   2   3   4   5   6

(1,0) to  (4,3)

Manhattan distance

• aka Taxicab distance
• Often used in intergrated circuits where the wires can run only parallel to the X and Y axes (ie, rectilinear).
  • https://xlinux.nist.gov/dads/HTML/manhattanDistance.html
  • https://xlinux.nist.gov/dads/HTML/rectilinear.html

  |   |   |   |   |   |   |             |   |   |   |   |   |   |
5-|---|---|---|---|---|---|           5-|---|---|---|---|---|---|
  |   |   |   |   |   |   |             |   |   |   |   |   |   |
4-|---|---|---|---|---|---|           4-|---|---|---|---|---|---|
  |   |   |   |   |   |   |             |   |   |   |   |   |   |
3-|---┏━━━━━━━━━━━━---|---|           3-|---|---|---┏━━━━---|---|
  |   ┃   |   |   |   |   |             |   |   |   ┃   |   |   |
2-|---┃---|---|---|---|---|           2-|---|---┏━━━┛---|---|---|
  |   ┃   |   |   |   |   |             |   |   ┃   |   |   |   |
1-|---┃---|---|---|---|---|           1-|---┏━━━┛---|---|---|---|
  |   ┃   |   |   |   |   |             |   ┃   |   |   |   |   |
0-|---┃---|---|---|---|---|           0-|---┃---|---|---|---|---|
  0   1   2   3   4   5   6             0   1   2   3   4   5   6



  |   |   |   |   |   |   |             |   |   |   |   |   |   |
5-|---|---|---|---|---|---|           5-|---|---|---|---|---|---|
  |   |   |   |   |   |   |             |   |   |   |   |   |   |
4-|---|---|---|---|---|---|           4-|---|---|---|---|---|---|
  |   |   |   |   |   |   |             |   |   |   |   |   |   |
3-|---|---|---┏━━━━---|---|           3-|---|---|---|---┃---|---|
  |   |   |   ┃   |   |   |             |   |   |   |   ┃   |   |
2-|---|---|---┃---|---|---|           2-|---|---|---|---┃---|---|
  |   |   |   ┃   |   |   |             |   |   |   |   ┃   |   |
1-|---┏━━━━━━━┛---|---|---|           1-|---|---|---|---┃---|---|
  |   ┃   |   |   |   |   |             |   |   |   |   ┃   |   |
0-|---┃---|---|---|---|---|           0-|---━━━━━━━━━━━━┛---|---|
  0   1   2   3   4   5   6             0   1   2   3   4   5   6

(1,0) to  (4,3)

The name comes from Manhattan, New York where the buildings were arranged in a grid layout and the shortest path a taxicab could take between two locations was precisely the 'Manhattan distance'. [¹][1]

It's like all the squares are buildings and the lines of the grid are roads.

To navigate between the different road junctions, a taxi would have to go around the 'buildings'.

Hence the nick name 'taxicab distance', I guess.

Chebyshev distance

• aka Chessboard distance.
• Named after the Russian mathematician Pafnuty Chebyshev.

+---+---+---+---+---+---+---+---+
| 3 | 3 | 3 | 3 | 3 | 3 | 3 | 4 |
|---+---+---+---+---+---+---+---+
| 3 | 2 | 2 | 2 | 2 | 2 | 3 | 4 |
|---+---+---+---+---+---+---+---+
| 3 | 2 | 1 | 1 | 1 | 2 | 3 | 4 |
|---+---+---+---+---+---+---+---+
| 3 | 2 | 1 | 𝐾 | 1 | 2 | 3 | 4 |
|---+---+---+---+---+---+---+---+
| 3 | 2 | 1 | 1 | 1 | 2 | 3 | 4 |
|---+---+---+---+---+---+---+---+
| 3 | 2 | 2 | 2 | 2 | 2 | 3 | 4 |
|---+---+---+---+---+---+---+---+
| 3 | 3 | 3 | 3 | 3 | 3 | 3 | 4 |
|---+---+---+---+---+---+---+---+
| 4 | 4 | 4 | 4 | 4 | 4 | 4 | 4 |
+---+---+---+---+---+---+---+---+

See:

• https://en.wikipedia.org/wiki/Chebyshev_distance
• https://en.wikipedia.org/wiki/Pafnuty_Chebyshev

Minkowski

• aka Lₘ distance.

https://xlinux.nist.gov/dads/HTML/lmdistance.html

SAT-SMT

https://cacm.acm.org/research/the-silent-revolution-of-sat/

–

From Handbook of Satisfiability by Armin Biere, Marijn Heule, Hans van Maaren, Toby Walsh:

In its broadest sense, a pseudo-Boolean function is a function that maps n Boolean values to a real number. … … Pseudo-Boolean constraints offer a more expressive and natural way to express constraints than clauses and yet, this formalism remains close enough to the SAT problem to benefit from the recent advances in SAT solving.

• Cook-Levine theorem: Boolean satisfiability problem is NP-complete.

Linear PB constaints

Σ aⱼlⱼ   operator   b
j

where
 - aⱼ,b ∈ ℤ
 - lⱼ are literals
 - operator ∈ {=, ≥, ≤, <, >}

RHS of the constraint (ie, b here) is known as the degree of the constraint.

Notations, abbreviations and some terms

• PB: Pseudo-boolean

• QBF: Quantified boolean formula

• LPB: Linear pseudo-boolean

• Literal

  • Eg: x, x̅

• Clause

  • Eg: x ∨ y

Resolution

• A refutation system
  • ie, can say if a list of clauses is unsat.

 a ∨ x         b ∨ x̅
─────────────────────
        a ∨ b

where a ∨ b is the resolvent over x of a ∨ x and b ∨ x̅.

Because we need both a ∨ x and b ∨ x̅ to be true.

3 variables => 8 possibilities:

sage: import sage.logic.propcalc as propcalc
sage: f = propcalc.formula("((a|x) & (b|(~x))) -> (a|b)")
sage: f.truthtable()
a      x      b      value
False  False  False  True
False  False  True   True
False  True   False  True
False  True   True   True
True   False  False  True
True   False  True   True
True   True   False  True
True   True   True   True

—

Consider a CNF from Handbook of satisfiability (2e, Chapter 7):

(x ∨ y) ∧ (x ∨ y̅ ∨ z) ∧ (x̅ ∨ z) ∧ (y ∨ z̅) ∧ (y̅ ∨ z̅)

Each clause is something that must necessarily hold (ie, like an axiom).

Since ⊥ is derivable, this CNF is unsat.

More

• Davis-Putnam + LL
• Conflict-Driven Clause Learning

Tech

UTF-8

(From computerphile video on UTF-8)

ASCII

• 7 bits
• First 32 points are control codes.
• Made this possible: A: 0b1000001 (65)
• Look at the last number to get nth letter.
• Lowercase letters start 32 bits later, which makes this possible:
  • a: 0b1100001 (97)

8-bit codes

• more codepoints but still had disadvantages.
• not standardized.
• Extended ASCII is one of these.
• not compatible with each other.
• lot of extra work.
• still not enough code points for all the languages in the world
• Japan had multiple codes
  • mojibake: garbled nonsensical text when one code is interpreted as another
  • https://en.wikipedia.org/wiki/Mojibake

Unicode:

• to have a common standard
• UTF-8: one of unicode formats?
  • What's the difference between UTF-16 and UTF-32?

UTF-8:

• Latin letters is still like 7-bit ASCII
  • Put a leading zero to ASCII
• Avoids wastage when compared to naïve implementation
• NULL is 8 zeros in a row in legacy computers
• Encoding
  • 110: start of a new character which is 2 bytes long
  • 10: is a continuation of previous block
  • 1110: start of a new character which is 3 bytes long
  • Has upto 6 bytes long code points

IPv4 vs IPv6

• 0.0.0.0: local network
  • If a device has this address, it often means that it is not connected
  to a TCP/IP network
• 127.0.0.1: common loopback address
  • Looks like the whole 127.0.0.0 to 127.0.0.255 range is available for loopback addresses
  • ipv6: ::1/128

JSON vs YAML

• YAML: allows comments
• YAML can be thought of as a superset of JSON
• Prefer JSON for relatively simpler structures
• 'Yaml bomb' possible in YAML due to recursive definition
• Tab character not allowed in YAML ??
  • https://yaml.org/faq.html

https://stackoverflow.com/questions/1726802/what-is-the-difference-between-yaml-and-json

madoko

Super and subscript

• Subscript: H~2~O is H₂O
• Superscript: mc²^ is mc²
• Use backslash to escape whitespace

Strikeout: Enclose with a pair of ~~

Link:

• Direct link: <link>
• Named link: [Text](link)

@inl: make 'inl' bold

—

See:

• http://madoko.org/reference.html

Sample:

• Input: https://github.com/anfelor/pfenning-oplss/blob/main/lecture1.mdk
• Output: https://www.cs.uoregon.edu/research/summerschool/summer24/lectures/pfenning1.pdf

Stuff that I would like to know more about

• Monadic second order logic
• How did something as rational as logic evolve out of philosophy?
• What's the use of considering NFAs instead of DFAs?
  • Less number of states?
  • We can't have a physical implementation of NFA, although such concepts probably came in before computers were invented.
• Monad in category theory
  • Haskell, fine. Got it. But what about in math?
• Spectroscopy