Confluence (rewriting system)

Multiple paths between a source and target term via rewrite rules.

As in the Church-Rosser theorem (ie, ordering in which reduction rules are applied doesn't matter in lambda calculus).

Weak vs strong normalization (rewriting system)

Following is weak normalizing:

1) S -> S S
2) S -> A

because there exists at least one path by which normal form is reached:

S -> S S 
  -> A A         (by 2)

But this is not strong normalizing because, the rewriting can potentially go on infinitely. For example:

S -> S S 
  -> (S S) S     (by 1)
  -> ...

— Strong normalization => no matter what order of rewrite rules we use, it will eventually lead to a normal form within a finite number of rewrites.

Untyped lambda calculus is not normalizing. Due to the famous divergent terms. It is not even weakly normalizing since given (λx. x x) (λx. x x), the only applicable rewrite rule is that of application and it would simply diverge further.

On the other hand, simply typed lambda calculus is strongly normalizing.

—

• Strong normalization implies weak normalization, but not the other way.
• Normal form => no more applicable rewrite rules. Irreducible.

Ref:

• https://cs.stackexchange.com/questions/68080/what-is-the-difference-between-strong-normalization-and-weak-normalization-in-th
• https://en.wikipedia.org/wiki/Normal_form_(abstract_rewriting)
• https://www.cse.chalmers.se/~abela/talkMcGill2012Normalization.pdf

Point-free functions

• aka tacit programming
• A style of writing functions where the function arguments are never explicitly mentioned.
• The function is made as a combinator.
  • via function composition operations.

Eg: A function to find factorial of a number

A 'normal' style function:

-- Haskell
fact :: Int -> Int
fact 0 = 1
fact n = n * fact (n-1)

λ> fact 5
120

A point-free style function: ¹⁰

fact :: Int -> Int
fact = foldl (*) 1 . enumFromTo 1

λ> fact 5
120

Weak head normal form

From here:

Weak-head normal form means: evaluate it until you reach the outermost constructor.

Eg:

Also see this.

Bifunctor

• Short for 'binary functor'¹.
• Functors of two arguments.
• A functor whose domain is a product of two categories.

Haskell got it in Data.Bifunctor:

class BiFunctor f where
  bimap :: (a -> b) -> (c -> d) -> f a b -> f c d

Incompleteness of subtyping in Java

Array types should be invariant, but java compiler enforces only the covariant part during its type checking phase. Java has got

   S <: T 
------------
 [S] <: [T]

The contravariance check is done at run-time.

So programs like this:³:

public class Foo {
  public static void main(String[] args) {
    Object[] oarr = "hi,hello".split(",");
    oarr[0] = 42;
  }
}

will compile fine, but would result in runtime error:

Exception in thread "main" java.lang.ArrayStoreException: java.lang.Integer
        at Foo.main(Foo.java:5)

This is a design choice that some people consider to have been not so cool.

See this and this.

Type inference

• aka type reconstruction

Principal type

Most general instance of a type: 'makes the smallest commitment about the values of type variables tha yields a well-typed term' Eg:

a = λf:Y. λx.X. f x

a by itself is not well-typed.

But if we have a map like:
σ = {Y↦X→X, X↦X}

σ a = λf:X→X. λx.X. f x

which is well-typed.

This is the most general instance of a.

Notation:

• σ ⊑ β: unifier σ is less specific (ie, more general) than unifier β.

Principal unifier: Most general unifier

• σ such that ∀α, σ ⊑ α

First-class values

With first-class values in a programming language, both the following are possible:

• Can be passed as arguments to functions
• Can be stored in data structures

Logical relations

Refs: link link

Strong normalization (??) of STLC is not provable with induction (??) but is with logical relations.

W-types and M-types

• Looks like W-types are just inductive types as in Coq

• And M-types seem to be coinductive types

• 'M-types can be derived from W-types': https://en.wikipedia.org/wiki/Inductive_type

See:

• https://ncatlab.org/nlab/show/W-type#WTypesInTypeTheory
• https://ncatlab.org/nlab/show/well-founded+relation

More:

• https://www.cs.uoregon.edu/research/summerschool/summer13/lectures/ahmed_official1.pdf
• https://www.cs.uoregon.edu/research/summerschool/summer16/notes/AhmedLR.pdf
• https://cs.brown.edu/people/bgreenma/resources/notes/logical-relations-greatest-hits.pdf

Kind

A kind is a type of types.

From https://serokell.io/blog/kinds-and-hkts-in-haskell

they show the arity of a type (if we think of that type as a function).

Concrete types are like values and polymorphic types are like functions.

Higher-kinded types

Can be thought of as a 'function' taking a kind and returning another kind.

Subtyping

• aka subtype polymorphism
• Principle of safe substitution
• 'subset semantics': a way of interpreting subtype relation

—

S <: T:

• S is a sub-type of T
• T is a super-type of S
• Set of S-values is a subset of set of T-values (aka subset-semantics)
• S is more informative than T
• Values described by S are also described by T
• Eg: S=squares, T=rectangles
  • All squares are also rectangles

—

Subsumption rule:

   s: S
 S <: T
---------  (T-SUB)
   s: T

—

Subtyping relation:

• Must be reflexive and transitive
• Record type: Can make S by adding more fields to T => S <: T
  • Smaller type (ie, type with lesser number of values) is the subtype
  • Subtyping => we are kind of further restricting set of possible values
  • Width subtyping
• Subtyping for functions => variance comes to play
  • Says under what circumstances can a function of one type can be used in place of another.

—

Sense of relation reversed for arg type (contravariant) but remained same for result type (covariant).

 T1 <: S1        S2 <: T2 
──────────────────────────
      S1→S2 <: T1→T2

(Go from conclusion then it's easier to remember this rule)

Intuition behind this rule:

f: S1→S2 means f is a function that accepts values of type S1.

This means f would accept values of a subtype of S1 as well. If T1 <: S1, we have:

S1→S2 <: T1→?

Now, considering the result value. f gives a value of type S2. Any value of type S2 is also a value of a supertype of S2.

If S2 <: T2, we have:

S1→S2 <: T1→T2

• No arg should 'surprise' the function.
• No result should surprise the context (to which the value from f would be given).

—

• Top: Maximum element of subtyping relation
  • Supertype of all types

Variance

• Covariant: 'Ordering of component types preserved'
• Contravariant: Ordering of component type reversed
• Bivariant: Both covariant and contravariant
• Invariant: Neither covariant and contravariant

Consider a type operator T and types A and B.

• T is convariant if A ≤ B means T(A) ≤ T(B)
• T is contravariant if A ≤ B means T(B) ≤ T(A)
• Invariant => mutable?? As in anything can happen??

https://old.reddit.com/r/programming/comments/lkmhy/understanding_covariance_and_contravariance_in/

• 'Java array subtyping problem – which is resolved in Java by doing a runtime check at each array mutation operation.'

Axiom K

There is only one proof equality.

• Not valid in homotopy type theory

https://www.pls-lab.org/en/Axiom_K_(type_theory)

Misc

• catamorphism: fold (banana)
• anamorphism: unfold
• hylomorphism: function made with both fold and unfold operations
• Endofunctor: A functor mapping a category to the self-same category.

Types, Categories, Topologies, Knots, etc

From an article.

Types

• W type of Aczel
• well-foundedness
  • well founded inductive types are like trees
• M-types (ie, coinductive types) can be made from W-types (ie, inductive types)
  • TODO: How?
• univalent foundation of math
  • math structures represented by types
  • type correspond to spaces
  • equal types correspond to homotopy equivalent spaces
  • equal elements of a type correspond to points in the space between which there is a path
  • agda-unimath

Categories

• natural transformation: morphism of functors

• natural isomorphism: natural transformation that is an isomorphism?

• adjoint functors

• adjunction

• monoidal category: like category of product types

• intial algebras

• initial object in the category of F-algebras for a given endofunctor F

  • So it itself is an F-algebra
  • 'Provides framework for recursion and induction.'
    • TODO: How?

• initial object (I)

  • aka coterminal object
  • aka universal object
  • For every object X in the category, there is exactly one morphism (I→X) from I to the X
  • Strict initial object: if the I→X morphisms are isomorphisms.

• terminal object (T)

  • aka final object
  • For every object X in the category, there is exactly one morphism X→T

• Null object

  • aka zero object
  • An object which is both initial object and terminal object
  • I guess:
    • there can be multiple initial objects in a category?
    • there cannot be multiple zero objects?
  • Pointed category: A category with a null object
    • What's the etymology of this name? Why 'pointed'?

• F-algebra

  • A functor F is the signature

• T-algebra

  • Like F-algebra for monads

• coalgebra

• terminal coalgebra

• centre of contraction

• dual (category theory)

• Opposite category

  • aka dual category
  • The category that we get by reversing the direction of all morphisms within the original category
  • Needless to say, opposite (opposite C) is C itself.

• small types

• groupoid (category theory)

  • a (small) category where all morphisms are invertible

• invertible morphism of a category

  • inverse morphism
  • morphism in the other direction
  • an invertible morphism is an isomorphism

• Kleisli catgory

  • The monad: (T, μ, η)
    • η: unit
    • μ: multiplication

• Interval category

  • aka 2
  • Category with just 2 objects (0 and 1) with just one non-trivial morphism (0 → 1)

• k-morphism (or k-cells)

  • 0-morphisms: objects themselves
  • 1-morphisms: morphism
  • 2-morphisms: morphisms between 1-morphisms
    • 2-categories have them
  • 3-morphisms: morphisms between 2-morphisms
    • 3-categories have them

• ∞-category

  • There are k-morphisms forall k≥0

• 2-category

  • A higher category
  • Has 2-morphisms (in addition to the 1-morphisms of normal categories)

Topology

• open set
  • Generalization of open interval in real line
• Closed set
• Interior
• manifold
• cobordism
  • 'bord' is French for boundary
• fibration

• Standard topology

homotopy

• 2 continuous functions between two topological spaces
  • Is R a topological space?

Topological space

• Consists of a set and a topology on that set
  • Elements of this set are called points
• Eg: R² with standard topology

Topology

• Topological equivalence
  • Eg: homotopy equiv, homeomorphism
• Classic example: homeomorphism between doughnut and coffee mug

Homeomorphism:

• Mapping from a topological space that preserves all topological properties of that space
• aka topological isomorphism
• Two spaces with a homeomorphism between them are said to be homeomorphic.
• Not all homeomorphisms are continuous deformations.
  • Homeomorphism that is a continuous deformation is a homotopy.
• Deformation of a line into a point is not a homeomorphism. Why?

Neighbourhood of a point:

• Set of points, of which the point is a part, such that we can move 'some distance' in any direction from that point without leaving that set.

Knot

Tangles String diagrams

Misc

Spaces:

• metric space
  • Distance is well-defined between any pair of points.
• Vector space
• linear operator: map between two vector spaces
• Euclidean space
• affine space
  • A generalization of Euclidean spaces
• Hilbert space
  • A vector space equipped with an inner product which can give rise to a distance function by which the vector space is a (complete) metric space.
• Cauchy space: a complete metric space

Operational vs denotational semantics

• Synthetic guarded domain theory (SGDT)

Recursion vs corecursion

They are duals of each other.

Recursion:

• Kinda 'top-down': Go down till a base case and build up from there
• Folding

Co-recursion:

• Kinda 'bottom-up: Accumulator style. Start from a point and build from there
• Unfolding

—

More:

• Classical (co)recursion - Downen, Ariola @ JFP'2023
• https://blog.thomasheartman.com/posts/corecursion-and-anamorphisms
• https://softwareengineering.stackexchange.com/questions/144274/whats-the-difference-between-recursion-and-corecursion

ITP vs ATP

References

• https://www.pls-lab.org/