User:Pengo/comp

From Wikipedia, the free encyclopedia

Flag of Earth Peter Halasz (talk) ?

Subpages: /dia | /missing | /org | /pages | /photo | /quotes

Ideas: /rants | /ite | /R | /teletaxo

Subjects: /bot | /comp | /ee | /eco | /fringe | /micro | /sd | /zoo

Incubator: /ownimg | /teletaxotest | /self

Computer science and related topics

Contents

[edit] Haskell

[edit] 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

[edit] Computer theory

[edit] Automata theory

[edit] Pushdown automata theory

[edit] Turing theory

[edit] Types and Programming Languages

[edit] Not covered

[edit] Introduction

[edit] Untyped arithmetic expressions

[edit] Definition styles

[edit] Symantics styles

[edit] ML example (ch4)

[edit] The Untyped Lambda-calculus

Alternatives:

Free variables and bound variables:

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:

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.t1) = FV(t1)\{x}
  • FV(t1 t2) = FV(t1) ∪ FV(t2)

[edit] Nameless representation of types

Capture (cont):

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:

[edit] 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

[edit] 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:

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)

[edit] Simple extensions

e.g.

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

also for null-able types:

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

e.g.

EuroAmount = <euros:Float>;

[edit] Normalization

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