ficha 7

Exercicio 1

Queremos provar a propriedadef.

(for f i)= for f (f i)

Agora estamos no contexto dos naturais:

F k = id + k

Vamos substituir os for por catamorfismos:

(for f i)=?
for f (f i)= ?

como escrever?

(for f i)=(| [(const i), f] |)

e

for f (f i)= (

[(const (f i)),f]

)

Então

f. (| [(const i), f] |) = (| [(const (f i)),f] |)    
<= {46}    
f. [(const i), f] = [(const (f i)),f] . (id + f)    
<=>{20,22,1}    
[f.(const i), f.f] = [(const (f i)),f.f]    
<=>{27}    
f.(const i)= (const (f i))    
f.f=f.f    
<=>{4}    
(const (f i))=(const (f i))    
true    
<=>    
true

Exercicio 1 - Alternativa

A ideia é também provar uma propriedade de um catamorfismo, neste caso (for f i). Relembrem que (for f i) é uma função recursiva que aplica a função f n-vezes a i, em que n é o número que damos como argumento a (for f i).

Neste caso a equação que queremos provar diz que: aplicar a função f (n+1)-vezes a i é a mesma coisa que aplicar a função f n-vezes a f i.

Para este exercício, teremos que tirar partido do functor associado aos números naturais e à lei da fusão-cata.

f . (for f i) = for f (f i)
≡ { Definiçao 'for f i' e 'for f (f i)'}
f . ⦇ [i̲, f] ⦈ = ⦇ [f̲ ̲i̲, f] ⦈
<= { Lei fusão-cata, functor dos Naturais }
f . [i̲, f] = [f̲ ̲i̲, f] . (id + f)
≡ { Lei fusão-+, absorpção-+}
[f . i̲, f . f] = [f̲ ̲i̲, f . f]
≡ { Fusão-constante}
[f̲ ̲i̲, f . f] = [f̲ ̲i̲, f . f]
≡
True

Exercicio 2

Queremos mostrar que a lei da recursividade mútua generaliza a três funções:

f.in = h . F <f,<g,j>>
g.in = k . F <f,<g,j>>
j.in = l . F <f,<g,j>>
`<=>`  
`<f,<g,j>> = (| <h,<k,l>> |)`

Comecemos então:

<f,<g,j>> = (| <h,<k,l>> |)
<=> {43}
<f,<g,j>> . in = <h,<k,l>> . F <f,<g,j>>
<=> {9}
<f.in,<g,j>.in> = < h.F <f,<g,j>> , <k,l>.F <f,<g,j>> >
<=> {16}
f.in = h . F <f,<g,j>>
<g,j>.in = <k,l>.(F <f,<g,j>>)
<=> {9,16}
f.in = h . F <f,<g,j>>
g.in = k . F <f,<g,j>>
j.in = l . F <f,<g,j>> QED

Exercicio 3

impar 0 = False    
impar (n+1)= par nepar 0 = True    
par (n+1) = impar n

queremos provar que estas duas definições são equivalentes a:

impar . in = h . F<impar,par>    
par . in = k . F<impar,par>

in=[zero,succ] e F k= id + k , porque estamos no contexto dos naturais

Queremos então provar:

impar . [zero,succ] = h . (id +<impar,par>)    
par . [zero,succ] = k . (id + <impar,par>)

Então

impar 0 = False    
impar (n+1)= par n    
<=>{ def. zero, def succ, 70,69 }    
impar.zero = (const False)    
impar.succ = par    
<=> { 7}    
impar.zero = (const False)    
impar.succ = p2.<impar,par>    
<=> {27,20,1}    
impar.[zero,succ]=[(const False).id, p2.<impar,par>]    
<=> {def in, 22}    
impar.in=[(const False), p2].(id+<impar,par>)    
<=> {F k = id+k}    
impar.in=[(const False), p2]. F<impar,par>

qual o h?

h = [(const False), p2]

Vamos fazer o mesmo para par para encontrar o k

O objectivo é chegar a :

par.in=k. F<impar,par>

O cálculo é semelhante ao anterior:

par 0 = True
par (n+1) = impar n    
<=>{def. zero, def succ, 70,69}    
par.zero =(const True)    
par.succ = impar    
<=> {7}    
par.zero =(const True)    
par.succ = p1.<impar,par>    
<=>{27,20,1}    
par.[zero,succ]=[(const True).id, p1.<impar,par>]    
<=> {def. in, 22}    
par.in=[(const True), p1].(id + <impar,par>)    
<=>{F k = id + k}    
par.in=[(const True), p1] . F<impar,par>

Temos então:

impar.in=[(const False), p2]. F<impar,par>    
par.in=[(const True), p1] . F<impar,par>

Queremos agora definir <impar,par> como um for

relembre que for b i = (| [(const i),b] |)

impar.in=[(const False), p2]. F<impar,par>    
par.in=[(const True), p1] . F<impar,par>    
<=> {50}    
<impar,par>=(| <[(const False), p2],[(const True), p1] > |)    
<=>{28 }    
<impar,par>=(| [<(const False), (const True)>, < p2, p1>] |)    
<=> {def. swap }    
<impar,par>=(| [(const (False, True)), swap] |)

logo:

<impar,par> = for swap (False, True)

Exercicio 3 - Alternativa

O exercício 3 apresenta funções mutuamente recursivas i.e. funções que se chamam uma à outra (relembrem que uma função recursiva é uma função que se chama a ela própria).

O objectivo do exercício é mostrar que funções mutuamente recursivas também podem ser capturadas na forma de um catamorfismo. E para tal, é bastante útil usar a lei de Fokkinga.

O exercício procede em duas partes: primeiro temos que converter as definições de ‘impar’ e ‘par’ no sistema de equações

impar . in = h . F <impar,par>  
par . in = k . F <impar,par>

para um dado h e k, e em que F é o functor dos números naturais. Isto vai-nos permitir aplicar a lei de Fokkinga para obter <impar,par> na forma de um catamorfismo. A segunda parte, é simplificar este catamorfismo usando as leis usuais de cálculo de programas.

O processo de converter funções mutuamente recursivas (sejam elas sobre números naturais, listas, ou árvores) vai ser sempre análogo ao processo que acabei de descrever.

Então para este exercício específico, temos que chegar ao sistema,

impar . in = h . F <impar,par>  
par . in = k . F <impar,par>

1a)

impar 0 = False
impar (n+1) = par n
≡ { Definição composição, Definição 0̲, F̲a̲l̲s̲e̲, e succ.}
impar . 0̲ x = F̲a̲l̲s̲e̲ (x)
impar . succ n = par n
≡ { Igualdade extensional}
impar . 0̲ = F̲a̲l̲s̲e̲
impar . succ = par
≡ { Lei Eq-+}
[impar . 0̲, impar . succ] = [F̲a̲l̲s̲e̲, par]
≡ { Lei Fusão-+ }
impar . [0̲,succ] = [F̲a̲l̲s̲e̲, par]
≡ { Definição in}
impar . in = [F̲a̲l̲s̲e̲, par]
≡ { Lei cancelamento-x}
impar . in = [F̲a̲l̲s̲e̲, p2 . <impar,par>]
≡ { Lei natural-id, lei absorpção-+}
impar . in = [F̲a̲l̲s̲e̲, p2] . (id + <impar,par>)

1b)

par 0 = True
par (n+1) = impar n
≡ { Definição composição, Definição 0̲, T̲r̲u̲e̲, e succ.}
par . 0̲ x = T̲r̲u̲e̲ (x)
par . succ n = impar n
≡ { Igualdade extensional}
par . 0̲ = T̲r̲u̲e̲
par . succ = impar
≡ { Lei Eq-+}
[par . 0̲, par . succ] = [T̲r̲u̲e̲, impar]
≡ { Lei Fusão-+ }
par . [0̲,succ] = [T̲r̲u̲e̲, impar]
≡ { Definição in}
par . in = [T̲r̲u̲e̲, impar]
≡ { Lei cancelamento-x}
par . in = [T̲r̲u̲e̲, p1 . <impar,par>]
≡ { Lei natural-id, absorpção-+}
par . in = [T̲r̲u̲e̲, p1] . (id + <impar,par>)

Portanto, conseguimos chegar ao sistema de equações pretendido, nomeadamente:

impar . in = [F̲a̲l̲s̲e̲, p2] . (id + <impar,par>)
par . in = [T̲r̲u̲e̲, p1] . (id + <impar,par>)

com base em 1a. e 1b.

Agora temos que efectuar o 2º passo usando a lei de Fokkinga

impar . in = [F̲a̲l̲s̲e̲, p2] . (id + <impar,par>)
par . in = [T̲r̲u̲e̲, p1] . (id + <impar,par>)
≡ { Fokkinga }
<impar,par> = ⦇ <[F̲a̲l̲s̲e̲, p2],[T̲r̲u̲e̲, p1]> ⦈

e agora podemos simplificar a equação resultante:

<impar,par> = ⦇ <[F̲a̲l̲s̲e̲, p2],[T̲r̲u̲e̲, p1]> ⦈
≡ { Lei da troca }
<impar,par> = ⦇ [<F̲a̲l̲s̲e̲,T̲r̲u̲e̲>, <p2,p1>] ⦈
≡ { Definição swap, definição constante }
<impar,par> = ⦇ [(̲F̲a̲l̲s̲e̲,̲T̲r̲u̲e̲)̲, sw] ⦈
≡ { Definição for }
for sw (False,True)

Exercicio 8

Considere o functor:

T X = X x X

T f = f x fe as funções:miu = p1 x p2
u = <id,id>

Temos de provar que:

miu . T u = id e que miu . u = id

Substituindo as definições temos:

 miu . T u
= {def miu, def T f}
(p1 x p2) . (u x u)
= {14}
(p1 . u) x (p2 . u)
= {def u}
(p1 . <id,id>) x (p2 . <id,id>)
= {7}
id x id
={15}
id

Vamos agora a: miu . u = id

miu . u
={def miu, def u}
(p1 x p2).<id,id>
= {11, 1}
<p1,p2>
={8}
id

Exercicio 9

Estamos no contexto das LTree:

data LTree a = Leaf a | Fork (LTree a, LTree a)    
F X = A + X x X    
F f = id + f x f

  

Leaf: A -> LTree A    
Fork: LTree A x LTree A -> LTree Ain=[Leaf,Fork]

a funçãomirror: LTree A -> LTree A

mirror (Leaf x) = (Leaf x)    
mirror (Fork (e,d)) = Fork (mirror d, mirror e)

pode ser definida como um catamorfismo de LTree:

mirror = (|in.(id+swap)|)

Então

mirror.mirror = id    
<=> { def mirror, 45 }    
mirror.(|in.(id+swap)|) = (|in|)    
<= {46}    
mirror.in.(id+swap) = in.(id+(mirror x mirror))    
<=> {def. mirror}    
(|in.(id+swap)|).in.(id+swap) = in.(id+(mirror x mirror))    
<=>{44}    
in.(id+swap).(id+(mirror x mirror)).(id+swap) = in.(id+(mirror x mirror))    
<=>{25,1}    
in.(id+swap.(mirror x mirror).swap)=in.(id+(mirror x mirror))    
<=>{natural swap:(fxg).swap = swap.(gxf) }    
in.(id+swap.swap.(mirrorxmirror)) = in.(id+(mirror x mirror))    
<=> {swap.swap=id, 1}    
in. ((id+(mirror x mirror))= in. (id+(mirror x mirror)    
<=>    
true

Exercicio 9 - Alternativa

O objectivo é provarmos que espelhar uma árvore duas vezes é equivalente a fazer nada.

Este exercício procede de forma análoga aos anteriores. Só que agora em vez de listas e números naturais, iremos trabalhar com a estrutura algébrica (tipo de dados) ‘Leaf trees’. Como vamos proceder de forma
análoga aos exercícios anteriores, convém então relembrar a definição do functor associado às ‘Leaf trees’: F f = id + f^2.
Lembrem-se também que teremos que usar a lei fusão-cata.

mirror . mirror = id
≡ { Definição mirror, reflexão-cata}
mirror . ⦇ in . (id + sw) ⦈ = ⦇ in ⦈
<= { Fusão-cata, functor das Leaf trees }
mirror . in . (id + sw) = in . (id + mirror^2)
≡ { Definição in }
mirror . [Leaf,Fork] . (id + sw) = [Leaf,Fork] . (id + mirror^2)
≡ { Definição Absorpção-+ }
mirror . [Leaf,Fork . sw] = [Leaf,Fork . mirror^2]
≡ { Definição Fusão-+ }
[mirror . Leaf, mirror . Fork . sw] = [Leaf,Fork . mirror^2]
≡ { Lei Eq-+ }
mirror . Leaf = Leaf
mirror . Fork . sw = Fork . mirror^2
≡ { Lei isomorfismos }
mirror . Leaf = Leaf
mirror . Fork . sw . sw = Fork . mirror^2 . sw
≡ { sw . sw = id }
mirror . Leaf = Leaf
mirror . Fork = Fork . mirror^2 . sw
≡ { Igualdade extensional }
mirror (Leaf a) = Leaf a
mirror (Fork (x,y)) = Fork . mirror^2 (y,x)
≡ { Lei composição }
mirror (Leaf a) = Leaf a
mirror (Fork (x,y)) = Fork (mirror y, mirror x)
≡ { Definição mirror }
True