Semântica de Linguagens - Exercícios

Lambda Cálculo

  1. Avalie as expressões lambda abaixo:

    1. (\x. x) (\x. x)

    2. (\x. y) (\x. x)

    3. (\x. x) (\x. x) y

    4. (\x. x x) (\x. x x)

    5. (\x. y) ((\x. x x) (\x. x x))

    6. (\t. \f. \o. o f t) (\x y. x) (\x y. y) (\p q. p p q)

  2. Liste as variáveis livres das expressões a seguir:

    1. x (\x. x)

    2. x (\y. y)

    3. x (\x. y)

    4. (\y. y) (\x. x)

    5. (\y. y) (\z. \y. x y z)

  3. Avalie as expressões lambda abaixo: (Para funções como add e inc, use as definições dadas no programa do curso.)

    1. inc two

    2. add two two

    3. inc inc

    4. (\i. \t. i t) (\n. \f. \z. f (n f z)) (\f. \z. f (f z))

  4. Avalie os resultados das substituições abaixo e destaque todos os redexes existentes nas expressões (antes e depois das substituições):

    1. (y x y)[y ← \z.x x]

    2. (\x.y x)[y <- \z.x]

    3. ((\x.y x) y)[y <- \z.x]

  5. Prove as igualdades a seguir. (Para funções como add e inc, use as definições dadas no programa do curso.)

    1. (\n.\f.\z.f (n f z)) (\f.\z.z) ≡ \f.\z.f z

    2. add one b ≡ inc b

  6. Você consegue provar a igualdade a seguir? add b one ≡ inc b

Haskell

  1. Escreva a função (||) ("ou" lógico). 

    (||) :: Bool -> Bool -> Bool

  2. Prove que sua função é associativa: 

    a || (b || c) = (a || b) || c

  3. Sua função é comutativa? 

    a || b = b || a

  4. Escreva uma função que verifique se um valor pertence a uma dada lista: 

    find :: (Eq a) => a -> [a] -> Bool

  5. Prove que sua função satisfaz a equação abaixo: 

    find x (ys ++ zs) = find x yx || find x zs

  6. Escreva uma função para ordenar uma lista: 

    sort :: (Ord a) => [a] -> [a]

Expressões Aritméticas

Escreva as árvores de sintaxe abstrata para as expressões abaixo. (Isto é, codifique as expressões como valores do tipo Exp.)
  1. 23 + 1 + 35
  2. 10 + -21 / (5 + 531 * 7)

Expressões Regulares

  1. Escreva as árvores de sintaxe abstrata para as expressões abaixo. (Isto é, codifique as expressões como valores do tipo Exp.)

    1. a*
    2. (a | b)+
    3. a?

  2. Prove as equivalências abaixo. (Observação: provar que duas expressões A e B são equivalentes significa provar que (eval A) = (eval B).)

    1. Para uma expressão X qualquer, (RESeq REEpsilon X) ≡ X
    2. Para uma expressão X qualquer, (REOr REEmpty X) ≡ X
    3. Para uma string s qualquer, eval (REKleene REAny) s = True
    4. Para duas expressões X e Y quaisquer, (REOr X Y) ≡ (REOr Y X)

  3. Defina uma função empty :: RE -> Bool, tal que empty X é verdadeiro se e somente se eval X s retorna falso para qualquer s. (A função deve ser uma recursão estrutural simples sobre a estrutura da expressão regular.) Mostre que sua função está correta.

  4. Defina uma função hasEpsilon :: RE -> Bool, tal que hasEpsilon X = eval X "". (Não vale usar eval na sua definição. A função deve ser uma recursão estrutural simples sobre a estrutura da expressão regular.) Prove que sua definição está correta, ou seja, que hasEpsilon X = eval X "".

  5. Defina uma função noEpsilon :: RE -> RE, satisfazendo as seguintes propriedades:

    1. Para qualquer expressão regular X, hasEpsilon (noEpsilon X) = False.
    2. Para qualquer expressão regular X e string não vazia s, eval X s = eval (noEpsilon X) s.
    (Ou seja, noEpsilon X aceita tudo que X aceita, menos a string vazia.) (Se possível, procure simplificar a expressão regular resultante.) Prove que sua implementação satisfaz as propriedades pedidas.

  6. Defina uma função infinite :: RE -> Bool, tal que empty X é verdadeiro se e somente se existem infinitos s tais que eval X s é verdadeiro.

Linguagem Imperativa Simples

(Nesses e nos demais exercícios, vamos usar uma pseudo-sintaxe livre para representar Árvores de Sintaxe Abstrata.)

  1. Escreva as árvores de sintaxe abstrata para os programas abaixo. (Isto é, escreva os valores Haskell do tipo Cmd correspondentes.)

    1. x = 10; y = 20; z = x + y
    2. while 1 do {}
    3. x = 10; while x do { y = y + 1; x = x - 1; }

  2. Prove que (x = 10; y = 20) ≡ (y = 20; x = 10).

  3. Prove que, para qualquer comando C, (skip ; C) ≡ C

  4. Modifique o construtor CmdSeq para ele conter uma lista de comandos, e adeque evalCmd a essa nova definição.

  5. Implemente o comando repeat until.

  6. Prove que, para qualquer comando C, (repeat C until 1) ≡ C.

  7. É possivel provar a equivalência abaixo, para qualquer expressão E e comando C? Discuta sua resposta. 

    (if E then C else C) ≡ C

Linguagem Funcional Simples

  1. Escreva as árvores de sintaxe abstrata para as expressões abaixo. (Isto é, escreva os valores Haskell do tipo Exp correspondentes.)

    1. (\x -> x + 10) 20
    2. \x -> \y -> x
    3. (\f -> f(10 * 30))(\x -> x)

  2. Implemente funções com vários argumentos na linguagem. (Dica: você deverá mudar ExpLambda, ExpApp e ValFunc para trabalharem com listas nos lugares adequados.)

  3. Prove que, para qualquer expressão E, ((\x -> x) E) ≡ E

  4. Impemente um operador "or" com curto circuito, isso é, a segunda expressão só deve ser avaliada se a primeira for falsa.

  5. Prove que sua implementação do operador "or" satisfaz as seguintes equivalências: (0 || E) ≡ E; (1 || E) ≡ 1;

  6. Podemos ter valores pré-definidos nos nossos interpretadores simplesmente colocando-os no ambiente ou memória inicial usados para executar os programas. Por exemplo, considere as linhas abaixo no interpretador de linguagens funcionais: 

    initialEnv = bind "square" (ValFunc square) emptyEnv
  where square (ValInt i) = ValInt (i * i)
    Se usarmos o ambiente initialEnv ao avaliarmos uma expressão, essa expressão poderá usar a função pré-definida square.

    Use essa técnica para criar uma função pré-definida addK, equivalente a definição abaixo: 

    addK = \k -> (\x -> x + k)
    (Note que a função addK retorna outra função. Cuidado com os tipos! Em particular, lembre-se de distinguir entre funções Haskell e funções da linguagem, que tem tipo Value com construtor ValFunc, e converter de um para o outro quando necessário.)

Linguagem Imperativa com Continuações

  1. Refaça todos os exercícios sobre a linguagem imperativa simples para essa nova implementação.

  2. Implemente um comando CmdBreak na linguagem, com a semântica usual de break em linguagens como C. (Dica: modifique o tipo de evalCmd para 

          evalCmd :: Cmd -> K -> K -> Mem -> Result
    onde a segunda continuação indica para onde o break deve continuar a execução do programa.)

  3. Prove que sua implementação de break satisfaz a equivalência (while 1 do break) ≡ skip

  4. Após a implementação de break, você ainda consegue provar a equivalência (repeat C until 1) ≡ C? Explique.

Linguagem Funcional com Continuações

  1. Refaça todos os exercícios sobre a linguagem funcional simples para essa nova implementação.

  2. Implemente uma expressão return exp, que termina imediatamente a execução da função corrente retornando o valor de exp. (Dica: use uma abordagem similar à usada na implementação do comando break, com uma continuação separada para ser usada pelo return.)

  3. Com sua implementação de return, é possivel provar a equivalência abaixo para qualquer expressão E? Discuta sua resposta. 

    ((\x -> return x) E) ≡ E

  4. Reimplemente a expressão return usando a seguinte abordagem: ao invés de return ser uma expressão especial na gramática da linguagem, return será uma função "comum". Cada função, ao ser chamada, coloca no seu ambiente uma nova variável return, cujo valor é um ValFunc que, ao ser executado, faz o retorno desejado. Como você compara essa implementação com a anterior?

Uma versão mais abstrata para o interpretador CPS

  1. Considerando as definições no código, prove as igualdades abaixo:

    1. op1 (op0 x) f = f x (para quaisquer f e x).
    2. op1 c op0 = c (para qualquer computação c).
    3. op1 (op1 c g) f = op1 c (\v -> op1 (g v) f) (para quaisquer f, g e c).

Linguagem Funcional com Efeitos Colaterais

  1. Nessa linguagem, a construção letrec ainda é necessária? Mostre como podemos escrever uma função explet que gere um código equivalente ao construtor ExpLet. (Você consegue provar que sua implementação está correta?)

Versão mais Abstrata da Linguagem Funcional com Efeitos Colaterais

  1. Considerando as definições no código, prove as igualdades abaixo:

    1. bind (unit x) f = f x (para quaisquer f e x).
    2. bind c unit = c (para qualquer computação c).
    3. bind (bind c g) f = bind c (\v -> bind (g v) f) (para quaisquer f, g e c).

Monadic Parser

  1. Execute o parser para as expressões abaixo e confira o resultado:

    1. (\x -> x + 10) 20
    2. \x -> \y -> x
    3. (\f -> f(10 * 30))(\x -> x)

  2. Acrecente ao parser a sintaxe let x = exp in exp', como açucar sintático para ((\x -> exp')(exp)).

  3. Acrescente ao parser a sintaxe \x y z -> ... (com uma ou mais variáveis), como açucar sintático para \x -> \y -> \z -> ....

  4. Conecte o parser com algum interpretador estudado, para criar um interpretador que lê a entrada padrão com um programa, cria uma árvore de sintaxe abstrata, executa o programa na árvore e imprime o resultado final.

  5. Neste parser, usamos somente o combinador orelse para opções, ao invés do +++. Para cada uso de orelse, discuta as vantagens e desvantagens de trocarmos para +++.

  6. Modifique o código do parser para usar o tipo Maybe, ao invés de listas. Que operações não têm uma tradução natural para esta modificação?

  7. Prove que sua implementação de monad do item anterior satisfaz as três leis monádicas.

Semântica Operacional para Linguagem Imperativa

  1. Considere a relação definida como (c, m) → (c', m') sse (c', m') = step c m, e a relação ⇒ definida como o fecho reflexivo-transitivo de →. Prove que, se (c1 , m) ⇒ (c1', m'), então (c1;c2 , m) ⇒ (c1';c2 , m').

  2. Usando a definição de evalCmd dada na semântica denotacional simples, prove que:

    1. se (c, m) → (c', m'), então evalCmd c' m' = evalCmd c m.
    2. se (c, m) ⇒ (c', m'), então evalCmd c' m' = evalCmd c m.

  3. Nesta semântica operacional, podemos definir uma relação de equivalência entre dois comandos c1 ≡ c2 sse evalCmd c1 m = evalCmd c2 m. Usando essa definição, prove as equivalências abaixo:

    1. skip ; c ≡ c.
    2. c ; skip ≡ c.

  4. Prove que, se c1 ≡ c2 nesta semântica operacional, então c1 ≡ c2 na semântica denotacional simples. Você consegue provar a volta dessa implicação?

Semântica Operacional para Linguagem Funcional com Efeitos Colaterais

  1. Mostre passo a passo a avaliação da expressão let f = \x -> x + 3 in f(4 + 5). (Lembre-se que o let é apenas açucar sintático.)

  2. Prove que se uma expressão exp não tem variáveis livres, e todos os valores na memória m não têm variáveis livres, e (exp, m) → (exp', m'), então exp' e m' também não têm variáveis livres.

  3. O inverso do exercício anterior é verdadeiro? (Isso é, se exp' não tem variáveis livres então exp também não tem.)