User:Pengo/comp

	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

Haskell

Codata

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

• cowords:
  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:
  coexist
• examples of comonads:
  I/O, component interfaces, parallel evaluation, concurrent communication processes, exceptions, explicit continuations

Automata theory

• 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
• Leftmost derivation
• Pushdown automata
  (PDA)
• Pushdown stack
• 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
• guard
• computation rule
• congruence rule
• derivation tree
• induction on derivations (a proof technique)
• value means normal form
• Structural induction
• inductive definition
• 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:
  Scheme
  (with some pattern-matching extension)
• Java, pure Scheme
  are somewhat heavy
• Code: [2]

The Untyped Lambda-calculus

Alternatives:

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

Free variables and bound variables:

• free variable
• bound variable

Evaluation strategies:

• 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
• parser
• internal language
  (IL), sublanguages of core features
• external language (EL), full language of derived forms

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
• 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)

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

• 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 Γ ..."
• 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'
• Γ in the permutation lemma
• weakening lemma

Curry-Howard Correspondence:

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

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

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

EuroAmount = <euros:Float>;