Skip to content

Latest commit

 

History

History
65 lines (35 loc) · 3.59 KB

big-ideas.md

File metadata and controls

65 lines (35 loc) · 3.59 KB
Raw

Big Ideas

(read bottom up ... out of date by now ... will come back to it ...)

...

(some big ideas that are still to come: variables, scope, binding, free algebras, higher-order functions, type inference, polymorphism, co-induction, bisimulation, non-deterministic computation, shared memory, message-passing, synchronous vs asynchronous, ... not all of this unfortunately ... )

(could be added now: terms as trees (parsing), formalising mathematical proofs in theorem provers, two dimensional syntax and string diagrams, ...)

Normalisation by Evaluation

see here

Invariants

see here

Compositionality

We will see many instances of this. For now, read again the lecture on synatx and semantics.

Termination by Measuring the Size of a Computation

see here and following

Propositions = Types, Proofs = Programs, Induction = Recursion

We have seen an example of a recursive program that is a proof by induction in the lecture on Idris.

Induction: The Smallest Set Closed Under a Set of Rules

We discussed in some detail that the set of natural numbers, the transitive closure of a relation, the set of programming languages given by a context-free grammar and the set of true equations derivable from given axioms are all examples of inductively defined sets.

  • The task to show that a given element e is in a given inductively defined set S amounts to finding a derivation that constructs the element e from the rules defining S.
  • From this point of view, parsing and theorem proving is essentially the same activity.

Confluent and Terminating Rewrite Systems have Unique Normal Forms

  • Computing with equations is circular, because equations are symmetric, that is, can be applied from left to right and from right to left. For example, 1/2=2/4=1/2=2/4=...

  • Therefore it is good to have conditions under which any computation results in a unique result. (Local) confluence and termination are often not too hard to establish, see the lectures on abstract reduction systems.

Normal Forms as Representatives of Equivalence Classes

  • Of course, we do not want to manipulate infinite sets of terms such as 1/2, 2/4, 3/6, ... directly. Therefore we set up rewrite rules that allow us to compute with normal forms such as 1/2 instead.
  • ...

Meaning as a Quotient by an Equivalence Relation

  • The meaning of a fraction such as 3/6 is the set of all fractions that are equivalent such as 1/2, 2/4, 3/6, ...
  • The meaning of arithmetic expressions has been discussed in detail in the second lecture on syntax and semantics.

Semantics as a Structure Preserving Function

  • I could explain the semantics (meaning) of German to you by translating German to English. This translation is a function that preserves the structure of the languages, for example, by mapping nouns to nouns and verbs to verbs, etc.
  • The meaning of arithmetic expressions has been discussed in detail in the lecture on syntax and semantics.

Computation as Rewriting to Normal Form

  • MWE: Cancelling fractions rewrites them to normal form.
  • Arithemtic expressions have been discussed in detail in Lecture 1.2 and following.
  • Programming languages will be discussed later.