User:Pengo/comp

Computer science and related topics

Haskell

Codata

from the paper Codata and Comonads in Haskell [1] (pdf)

• cowords: codata, comonad, coalgebra, co-variety, cofree, codomain, co-extension (coextend may be called preserve)
• cofunctions: co-eval or coeval (function or combinator), co-ext (function), coOpenFile, coGetChar, coPutChar, coClose
• cophrases: codata object, structure coalgebras, codomain type, comonadic type, comonadic function,
• almost cowords: coercion, coexist
• examples of comonads: I/O, component interfaces, parallel evaluation, concurrent communication processes, exceptions, explicit continuations

Computer theory

Automata theory

• Kleene closure, Kleene's theorem
• Recursive definition
• Regular expression
• Finite language
• Finite automata (FA)
• Transition graph (TG)
• Generalized transition graph
• Nondeterminism
• Nondeterministic finite automata (NFA),
• Moore machine
• Mealy machine
• Transducer
• Sequential circuit
• regular language
• Closure
• Pumping Lemma, Pumping lemma, Lemma
• Myhill
• Nerode Theorem, Nerode theorem
• Quotient language, Quotient
• Decidability
• Finiteness

Pushdown automata theory

• Context-free grammar (CFG)
• Symbolism
• Generative grammar
• Łukasiewicz notation, Polish notation (Jan Łukasiewicz)
• Ambiguity
• Total language tree
• Grammatical format
• Regular grammar
• Chomsky normal form / Chomsky Normal Form
• Leftmost derivation
• Pushdown automata (PDA)
• Pushdown stack
• Non-Context-Free language, Non-context-free language, Non-context-free
• Self-embeddedness
• Context-free language (CFL)
• Decidability
• Emptiness and Uselessness

Turing theory

• Turing machine (TM)
• Subprogram
• Post machine (PM)
• Minsky's theorem
• Two stack pushdown automata, Two stack PDA
• Move-in-State machine, Move-in-state machine, Move-in-state, Move in state
• Stay-Option machine, Stay-option machine
• k-Track, k-track, k-track turing machine
• two-way infinite tape model, two-way infinite tape
• nondeterministic turing machine
• read-only turing machine
• turing machine language, turing machine languages
• recursively enumerable language
• non-recursively enumerable language
• universal turing machine
• decidability
• Chomsky hierarchy
• Phrase-structure grammar, Phrase-structure
• Type 0
• Context-sensitive grammar
• Computable function
• Church's thesis
• Language generator

Types and Programming Languages

Not covered

• Denotational and axiomatic approaches to semantics, denotation, axiom, semantics
• The rich connections between type systems and logic
• dependent types (mentioned in passing)
• intersection type (mentioned in passing)
• Curry-Howard correspondence (mentioned in passing)

Introduction

• formal methods, lightweight formal methods
• Hoare logic
• algebraic specification language
• modal logic
• denotational semantics
• model checker
• type system
• type theory
• dimension analysis
• language safety, safe language
• region inference
• typechecking
• categorial grammar

Untyped arithmetic expressions

• expression vs term
• abstract syntax
• inference rule
• natural deduction style
• closure properties
• one step evaluation, reduction, evaluation relation vs big step style (big step)
• evaluation strategy
• conditional, guard
• computation rule
• congruence rule
• derivation tree
• induction on derivations (a proof technique)
• value means normal form
• Structural induction
• inductive definition
• systems of inference rules (inference rule)
• proof by induction

Definition styles

• BNF grammar (metalanguage)
• inductive definition
  • by inference rules: axioms and "proper rules"
  • creating a set of concrete rules
  • better called a rule schema (because metavariables are used)
• Concrete definition (to generate all expressions/terms)

Symantics styles

• operational semantics (used exclusively in the book)
  • abstract machine
• denotational semantics
  • semantic domain
  • interpretation function
  • domain theory
• axiomatic semantics

ML example (ch4)

• Objective Caml
• Arithmetic expression
• Automatic storage management (garbage collection)
• other recommendations: Standard ML, Haskell, Scheme (with some pattern-matching extension)
• Java, pure Scheme are somewhat heavy
• Code: [2]

The Untyped Lambda-calculus

Alternatives:

• pi-calculus (Milner, Parrow, Walker)
• object calculus (Abadi, Cardelli)

Free variables and bound variables:

• free variable
• bound variable

Evaluation strategies:

• full beta-reduction, beta-reduction (any redex at any time)
• normal order strategy (normal order), leftmost, outermost redex is always reduced first
• call-by-name, no reductions inside abstractions. non-strict (lazy)
• call by need (Haskell). non-strict (lazy)
• call-by-value (most languages). strict (arguments always evaluated)

Lambda calculus grammmar:

t ::=            terms:
       x         variable
       λx.t      abstraction or lambda-abstraction
       t t       application

Language levels:

• concrete syntax, or surface syntax, the source code
• abstract syntax, the internal representation, eg abstract syntax tree. via lexer and parser
• internal language (IL), sublanguages of core features
• external language (EL), full language of derived forms

Capture:

• variable capture, capture-avoiding substitution
• alpha-conversion

Free variables:

• FV(t) is the set of free variables of term t.
• FV(x) = {x}
• FV(λx.t₁) = FV(t₁)\{x}
• FV(t₁ t₂) = FV(t₁) ∪ FV(t₂)

Nameless representation of types

Capture (cont):

• Barendregt convention (Henk Barendregt)
• explicit substitution
• combinators to avoid variables: combinatory logic, FP (Backus' functional language)
• Canonical representation (used by this book). Well known technique due to de Bruijn.

Nicholas de Bruijn:

• de Bruijn
• de Bruijn presentation
• Canonical representation
• de Bruijn graph (not mentioned)
• nameless term, de Bruijn term
• de Bruijn indicies, de Bruijn index, static distance
• 0-term, 0 term, terms with no free variables
• 1-term, 1 term, terms with 1 free variable
• n-term, n term, (not used in book)

Explicit substitution:

• explicit substitution, Abadi, Cardelli, Curien, Lévy (1991a)

Typed Arithmetic Expressions

• Typed Arithmetic Expression, Typed arithmetic expression

• typing relation
• lemma
• generation lemma
• inversion lemma

Safety = Progress + Preservation

• "safety is progress plus preservation" (using a canonical forms lemma) —Harper. Also Wright and Felleisen (A synthactic approach to type soundness. Information and Computation, 115(1):38-94, 15 Nov 1994.
• stuck state
• canonical form
• safety == soundness
• subject expansion

Simply typed lambda-calculus

Type assignment system:

• explicitly typed vs implicitly typed
• explicitly typed: type checker
• implicitly typed: types inferred or reconstructed

symbols:

• Γ ⊢ t:T "the closed term t has type T under the empty set of assumptions."
• (not from book) ⊢ inference, reduces to. x ⊢ y means y is derived from x
• Table of mathematical symbols
• Γ ⊢ x : R, then x:R ∈ Γ (the type assumed for x in Γ is R)
• dom(Γ) gives the set of variables bound by Γ

context:

• Γ is context
• Γ is the set of assumptions about the types of the free variables in t.
• Γ ⊢ ... "using the context Γ ..."
• typing context or type environment

T ::=            types:
       T→T       type of functions

Γ ::=            contexts:
       ∅        empty context
       Γ,x:T     term variable binding

more lemmas:

• substituion lemma is important in safety proofs, so important that similiar lemmas get referred to as 'the substitution lemma'
• Δ is a permutation of Γ in the permutation lemma
• weakening lemma

Curry-Howard Correspondence:

• Curry-Howard correspondence aka Curry-Howard isomorphism
• introduction rule, elimination rule
• law of the excluded middle
• applies also to System F (quantification over type corresponds with second-order constructive logic)
• Girard's linear logic (1987) to linear type system(s)
• modal logic(s)
• partial evaluation
• run-time code generation

Logic	Programming languages
propositions	types
proposition P ⊃ Q	type P → Q
proposition P ∧ Q	type P × Q
proof of proposition P	term t of type P
proposition P is provable	type P is inhabited (by some term)

Thorough discussions of this correspondence:

• Girard, Lafont, and Laylot (1989)
• Gallier (1993)
• Sørensen and Urzyczyn (1998)
• Pfenning (2001)
• Goubault-Larrecq and Mackie (1997)
• Simmons (2000)

Erasure and Typability

• erasure
• typability
• Curry-style (terms, then symantics) used also for implicitly typed syntax
• Church-style (terms, then identify the well-types terms, then semantics to types)

Simple extensions

• Syntactic sugar
• Unit type (= void type)
• ascription (comments, and type abbreviations)
• Let binding, (Assignment (computer science))
• sum type (sum typing). Addr = PhysicalAddr + VirtualAddr. (=Dynamic supertyping)
• variant,

e.g.

Addr = <physical:PhysicalAddr, virtual:VirtualAddr>;
a = <physical:pa> as Addr;

also for null-able types:

OptionalNat = <none:Unit, some:Nat>;

• reference type
• single-field variant

e.g.

EuroAmount = <euros:Float>;

• Disjoint union(s), sum and variant types sometimes called disjoint unions.
• typecase, type dynamic, typecase construct (for unmarshalling of type info)
• full abstraction
• fix construct, fixed point of a function, fixed point operator, T-FIX,

Normalization

• Normalization, Normalizable, guaranteed to halt in a finite number of steps.
• logical relation(s)