User:Pengo/comp

From Wikipedia, the free encyclopedia

	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

1 Haskell
- 1.1 Codata
2 Computer theory
3 Types and Programming Languages

[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

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

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

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

[edit] Types and Programming Languages

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

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

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

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

[edit] Symantics styles

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

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

[edit] The Untyped Lambda-calculus

Alternatives:

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

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:

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

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

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

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)

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