Semântica de Linguagens - Programa

  1. Introdução: Conceitos básicos de semântica de linguagens; semântica de linguagens versus semântica de programas; semântica formal; interpretadores definicionais; dificuldades com implementações definicionais; não determinismo.

  2. Lamba cálculo: motivação; noções básicas informalmente; funções como valores; currying.

  3. O Lambda cálculo puro.

    Expressões lambda:

    1. x (variável)

    2. e1 e2 (aplicação)

    3. \x. e (abstração)

    Variáveis livres:

    1. FV(x) = {x}

    2. FV(M N) = FV(M) ∪ FV(N)

    3. FV(\x. M) = FV(M) − {x}

    Uma variável que não é livre é chamada de ligada (bound).

    Chamamos de combinador qualquer expressão lambda irredutível (forma normal) sem variáveis livres. Exemplos famosos:

    1. \x. x (identidade)

    2. \x.\y. x (K: cria função constante)

    3. \f.\x.\y f y x (flip)

    4. \f.\g.\x f (g x) (composição)

    5. \x. x x (omega)

    Substituição:

    1. x[x ← N] = N

    2. y[x ← N] = y, se x ≠ y

    3. (M N)[x ← e] = (M[x ← e]) (N[x ← e])

    4. (\x. M)[x ← N] = \x. M

    5. (\y. M)[x ← N] = \y. (M[x ← N]), se x ≠ y e y ∉ FV(N)

    6. (\y. M)[x ← N] = \z. ((M[y ← z])[x ← N]), onde z é uma nova ("fresh") variável

    Chamamos de redex qualquer (sub)expressão com o padrão (\x.M) N, quer dizer, uma aplicação de uma abstração (\x.M) sobre uma expressão N qualquer.

    Uma expressão lambda está em forma normal se não contém nenhum redex.

    Conversão alfa: \x. M →α \y. (M[x ← y]), se y ∉ FV(M).

    Conversão beta: (\x. M) N →β M[x ← N]

    Conversão eta: (\x. M x) →η M

    Teorema de Church-Rosser: Se M →* N e M →* N', então existe P tal que N →* P e N' →* P (onde →* signfica zero ou mais reduções alfa ou beta).

    Referência adicional: A Tutorial Introduction to the Lambda Calculus; Raúl Rojas; FU Berlin, WS-97/98.

  4. Expressividade do Lambda cálculo.

    Codificação de booleanos: 

    TRUE ≡ \x.\y.x
FALSE ≡ \x.\y.y
IF ≡ \c.\t.\e.c t e
OR ≡ \p.\q.p p q
AND ≡ \p.\q.p q p
NOT ≡ \p.p FALSE TRUE

    Codificação de naturais: 

    ZERO ≡ \f.\z.z
ONE ≡ \f.\z.f z
TWO ≡ \f.\z.f (f z)
THREE ≡ \f.\z.f (f (f z))
…
INC ≡ \n.\f.\z.f (n f z)
ADD ≡ \m.\n.m inc n ≡ \m.\n.m (\n.\f.\z.f (n f z)) n
MULT ≡ \m.\n.m (add n) zero ≡ \m.\n.m (\p.n (\q.\f.\z.f (q f z)) p) (\x.\y.y)
PRED ≡ \n.\f.\x.n (\g.\h.h (g f)) (\u.x) (\u.u)
MINUS ≡ \m.\n. n PRED m

    Pares ordenados: 

    PAIR = \a.\b.\f.f a b
FIRST = \p. p (\x.\y.x)
SECOND = \p. p (\x.\y.y)

    Combinador de ponto fixo: 

    Y = \f.(\x.f (x x)) (\x. f (x x))

    Referência adicional: Introduction to Lambda Calculus; Henk Barendregt & Erik Barendsen.

  5. Linguagens funcionais puras, Haskell. Exemplos simples ("hello world", funções triviais), funções simples, definições por casos; notação lambda; tipagem; currying;

  6. Haskell: detalhes sintáticos: identificadores, identação, operadores infixados; cláusula "where" e expressão "let";

  7. Haskell: listas (head, tail, null, ':', [], [a,b,c]); exemplo simples com listas (somatório, concatenação, comprimento, index, replicate); definições por casos para listas (definição de head/tail/null); inversão (simples e com acumulador);

  8. Provas: raciocínio equacional e indução. Combinadores: id, flip, (.), const

  9. Manipulação de listas: map/filter/fold, take/drop. "List comprehension": 

    [e | True] = [e]
[e | q]    = [e | q, True]
[e | b, Q] = if b then [e | Q] else []
[e | p <- l, Q] = let ok p = [e | Q]
                      ok _ = []
                  in concatMap ok l
    Exercícios de combinatória.

  10. Tipos algébricos. Naturais como tipo algébrico; árvores; árvores de sintaxe abstrata.

  11. Um "interpretador" para expressões aritméticas. (slides)

  12. Um "interpretador" para expressões regulares. (slides)

  13. Um interpretador para uma linguagem imperativa simples. (slides)

  14. Recursão e Pontos Fixos.

  15. Um interpretador para uma linguagem funcional simples.

  16. Um Uma variante para o interpretador para uma linguagem funcional simples.

  17. Chamadas finais e continuações; CPS (continuation-passing style).

  18. Um interpretador CPS para a linguagem imperativa simples.

  19. Um interpretador CPS para a linguagem funcional simples.

  20. Uma versão mais abstrata para o interpretador CPS.

  21. Um interpretador para uma linguagem funcional com efeitos colaterais estilo ML.

  22. Uma versão mais abstrata do interpretador para uma linguagem funcional com efeitos colaterais.

  23. Continuações como valores de primeira classe em linguagens.

  24. Type Classes em Haskell.

  25. O mônada IO em Haskell.

  26. Parser Combinators. (Ver também [1] e [2])

  27. Um interpretador operacional para a linguagem imperativa simples.