Ficha 4

Introdução

Nesta ficha vamos começar por estudar um novo combinador, de forma a termos acesso a formas mais poderosas de compor programas. Nomeadamente, vamos começar por estudar o condicional de McCarthy que nos permite escrever expressões “if-then-else”.

Olhando para a ficha, notem que p -> f,g representa um programa que dado um x, retorna f(x) ou g(x), dependendo se p envia x para f ou para g respectivamente.
Podem pensar que p é uma espécie de controlador de carris numa bifurcação que direciona um comboio (o input x) ou para a esquerda ou para a direita. Em cada lado da bifurcação estarão o f e o g à espera do dito comboio.
Mais tecnicamente ‘p’ representa um predicado.

Exercicio 1

O exercício 1 pede para provar a equação: (p -> f,g) . h = (p . h) -> (f . h), (g . h)

## Como de costume, sugiro que começem pelo lado “mais complicado da equação” e tentem chegar ao lado “mais simples” usando as leis de cálculo de programas. Vou-vos dar uma ajuda:

(p . h ) -> (f . h), (g . h)
= { Lei (30) }
[f . h, g . h] . (p . h)?
= { Lei (22) }
[f, g] . (h + h) . (p. h)?
= { Lei (29) }
[f,g] . p? . h
= { Lei (30) }
(p -> f,g) . h

Exercicio 2

No ex. 2, vamos começar por tentar provar a equação (F3).

<(p → f , h), (p → g, i )> = p → <f , g>, <h, i> (F3)

<(p -> f,h) (p -> g,i)>
= { Lei (30) }
<[f,h] . p?, [g,i]. p?>
= { Lei (9) }
<[f,h], [g,i]> . p?
= { Lei (28) }
[<f,g>, <h,i>] . p?
= { Lei (30) }
p -> <f,g>, <h,i>

Provar (F4).

<f, (p → g, h)> = p → <f, g>, <f, h> (F4)

p -> <f,g>, <f,h>
= { Lei (30) }
[<f,g>,<f,h>]. p?
= { Lei (28) }
<[f,f], [g,h]> . p?
= { Lei (9) }
<[f,f] . p?, [g,h] . p?>
= { Lei (F1) e lei (30) }
<f, p -> g,h>

Exercicio 3

O exercício 3 é semelhante ao exercício 1 da ficha nº3: temos que derivar/obter um programa (out) a partir de um conjunto de condições.
Neste caso a única condição é que out . in = id.

Notem a beleza e rigor disto: estamos a calcular um programa que nós desejamos que cumpra certas condições; de forma semelhante ao engenheiro civil que calcula o cimento que vai ser necessário para construir uma ponte.

out . in = id
= { Definição in }
out . [0̲, succ] = id
= { Lei fusão-+ }
[out . 0̲, out. succ] = id
= { Lei universal-+ }
out . 0̲ = i1
out . succ = i2
= { Igualdade extensional}
out . 0̲ () = i1 ()
out . succ n = i2 n
= { Definição 0̲, definição succ }
out 0 = i1 ()
out (n+1) = i2 n

Exercicio 4

Vamos então ao exercício 4, que incide sobre as operações curry e uncurry.
Como já falado nas teóricas, estas operações permitem-nos transformar um programa de dois argumentos num programa de um só argumento e vice-versa.
Estas funções estão, por exemplo, por detrás da elegância do Haskell.

Das aulas teóricas, sabemos que quando aplicamos a operação curry a um programa f : A x B -> C de dois argumentos obtemos um programa (curry f) : A -> C^B que dado um elemento do tipo A devolve-nos uma programa do tipo B -> C.
Podemos experimentar isso por exemplo em Haskell, e é isso que vos convido a fazer agora.

Quem tiver o ghci pode escrever: mysum (x,y) = x + y.
Esta função vai ter dois argumentos, facto que vocês podem verificar pedindo ao ghci para nos dar o tipo de mysum:
> Prelude> :t mysum
> mysum :: Num a => (a, a) -> a

E claro podem testa-la
> Prelude> mysum (2,3)
> 5

Ao usar a operação curry sobre o mysum obtemos:
> Prelude> :t (curry mysum)
> (curry mysum) :: Num c => c -> (c -> c)

Istp é, uma função que dado um número x devolve-nos a função (x+). Por sua vez, quando a função (x+) recebe um número y ela devolve x+y.
Podemos testar isto fazendo por exemplo:
> Prelude> ((curry mysum) 2) 3
> 5

A função curry mysum é igual a qual função em Haskell ? (+)

Podem experimentar fazendo: (+) 2 3; vai dar o mesmo resultado que curry mysum 2 3
E a função uncurry (+) é igual a qual função ?
Volta a ser mysum.
Portanto vamos obter que uncurry (curry mysum) = mysum
O que sugere que uncurry e curry são inversas uma da outra, e de facto é isso que acontece

a)

O objectivo é começarem com f k = ap . (k ⨯ id) e chegarem a (f k) (a,b) = k a b , em que este último passo é precisamente a definição da função uncurry.

f k = ap . (k ⨯ id)
≡ { Igualdade extensional (adição de variáveis) }
(f k) (a,b) = ap . (k ⨯ id) (a,b)
≡ { def-comp, def-x, def-id}
(f k) (a,b) = ap (k a, b)
≡ { def-ap }
(f k) (a,b) = k a b

Para esclarecer: no fim, trocando o símbolo f por uncurry e o símbolo k por f, obtemos: (uncurry f) (a,b) = f a b

Exercicio 6

É nos dito que Aᴮ⁺<sup>C</sup>2ᶜ e Aᴮ x Aᶜ são isómorficos ou seja, uma função que recebe ou B ou C e dá um A é a mesma coisa que ter duas funções, uma que só recebe Bs e outra que só recebe Cs como é que provamos isto? são nos dadas duas funções join e unjoin entre esses dois tipos e é nos dito para provar que são isomorfismos, ou seja: join . unjoin = id e unjoin . join = id.

como são funções de ordem superior

join (f,g) é pointwise: as funções são as variáveis

se as definições estão em pointwise, temos que começar por introduzir variáveis no exercício

qual é o tipo de unjoin . join?

é uma composição como qualquer outra, por isso é o tipo de entrada do join para o de saída do unjoin

por isso que variáveis é que introduzo? temos de introduzir dos dois lados (f,g)

O join recebe um par de funções Aᴮ x Aᶜ

então, agora que estamos em pointwise, é só aplicar a definição do join e unjoin, que nos é dada no exercício e as leis do formulário da última secção, que têm das definições pointwise dos operadores por isso, arrancamos com a da composição e do id, que já devem ser triviais nesta fase.

unjoin . join = id  
= { introduzir variáveis (69) }  
	(unjoin . join) (f,g) = id (f,g)  
= { def-comp (70), def-id (71) }  
	unjoin (join (f,g)) = (f,g)  
= { def-join }  
	unjoin [f,g] = (f,g)  
= { def-unjoin }  
	([f,g].i1,[f,g].i2) = (f,g)  
= { cancelamento-+ (18)}  
	(f,g) = (f,g)

Exercicio 6 - Alternativa

É nos dito que Aᴮ⁺ᶜ e Aᴮ x Aᶜ são isómorficos ou seja, uma função que recebe ou B ou C e dá um A é a mesma coisa que ter duas funções, uma que só recebe Bs e outra que só recebe Cs como é que provamos isto? são nos dadas duas funções join e unjoin entre esses dois tipos e é nos dito para provar que são isomorfismos, ou seja: join . unjoin = id e unjoin . join = id.