Exercícios adicionais

Muitas funções comuns em listas podem ser implementado em termos de Fold. Por exemplo, aqui está uma definição alternativa de comprimento:

Fold_length <x> (xs: List x) : Nat
Fold_length xs = Fold (x => y Nat.succ y) xs 0n

Test_fold_length1 : Equal (Fold_length [4, 7, 0]) 3n
Test_fold_length1 = Equal.refl

Prove a validade de Fold_length:

Fold_length_correct <x> (xs: List x) : Equal (Fold_length xs) (List.length xs)
Fold_length_correct xs = ?

Nós também podemos definir Map nos termos de Fold. Termine a função:

Fold_map <x> <y> (f: x -> y) (xs: List x) : List y
Fold_map f xs = ?

Escreva um teorema fold_map_correct em Kind declarando que Fold_map está correto e prove isso:

Fold_map_correct : ?

No Kind, uma função f: a -> b -> c realmente tem o tipo a -> (b -> c). Ou seja, se você der a f um valor do tipo a, ele fornecerá a função g: b -> c. Se você der a ´g´ um valor do tipo ´b´, ele retornará um valor do tipo ´c´. Isso permite a aplicação parcial, como em Plus3. Processar uma lista de argumentos com funções que retornam funções é chamado de currying, em homenagem ao lógico Haskell Curry.

Por outro lado, podemos reinterpretar a função f: a -> b -> c como (Pair a b) -> c. Isso é chamado de uncurrying. Com uma função binária uncurry, ambos os argumentos devem ser fornecidos ao mesmo tempo como um par; não há aplicação parcial.

Podemos definir o curry da seguinte forma:

Pair_curry <x> <y> <z> (f: (Pair x y) -> z) (x_val: x) (y_val: y) : z 
Pair_curry f x_val y_val = ?

Como exercício, defina seu inverso, Pair_uncurry. Em seguida, prove os teoremas abaixo para mostrar que os dois são inversos.

Pair_uncurry <x> <y> <z> (f: x -> y -> z) (p: Pair x y) : z
Pair_uncurry f p = ?

Como um exemplo (trivial) da utilidade do curry, podemos usá-lo para encurtar um dos exemplos que vimos acima:

Test_map2 : Equal (Map (x => Plus 3n x) [2n,0n,2n]) [5n,3n,5n]
Test_map2 = Equal.refl

Exercício de reflexão: antes de executar os comandos a seguir, você pode calcular os tipos de Pair_curry e Pair_uncurry?

Uncurry_curry <x> <y> <z> (f: x -> y -> z) (x_val: x) (y_val: y) : 
   Equal z (Pair_curry (p => Pair_uncurry f p) x_val y_val) (f x_val y_val)
Uncurry_curry f x_val y_val = ?

Curry_uncurry <x> <y> <z> (f:(Pair x y) -> z) (p: Pair x y) : 
   Equal z (Pair_uncurry (x => y => Pair_curry f x y) p) (f p)
Curry_uncurry f p = ?

Lembre-se da definição da função Nth_error(Nth_error_informal):

Nth_error_informal <x> (l: List x) (n: Nat) : Maybe x
Nth_error_informal List.nil n = Maybe.none 
Nth_error_informal (List.cons head tail) Nat.zero = Maybe.some head 
Nth_error_informal (List.cons head tail) (Nat.succ n) = Nth_error tail n

Escreva uma prova informal do seguinte teorema:

Nat -> List -> (Equal (Length List) Nat) : Equal (Nth_error_informal List Nat) Maybe.none

Nós podemos explorar uma forma alternativa de definir os números naturais, usando os Numerais de Church, nomeado em homenagem ao matemático Alonzo Church. Podemos representar um número natural n como uma função que recebe uma função s como parâmetro e retorna s iterado n vezes.

Num <x> : Type
Num x = (x -> x) -> x -> x

Vamos ver como escrever alguns números com esta notação. Iterar uma função uma vez deve ser o mesmo que apenas aplicá-la. Desta forma:

One : Num
One = s => z => s z 

Perceba, a função aplica um s a um z, se lermos o s como sucessor e o z como zero, temos que o One é igual ao sucessor de zero.

Similarmente, o Two aplica a função s duas vezes ao z:

Two : Num
Two = s => z => s (s z)

Definir zero é um pouco mais complicado: como podemos “aplicar uma função zero vezes”? A resposta é realmente simples: basta retornar o argumento intocado.

Zero : Num
Zero = s => z => z

Mais geralmente, um número n pode ser escrito como s => z => s (s ... (s z) ...), com n ocorrências de s. Observe em particular como a função doit3times que definimos anteriormente é, na verdade, apenas a representação de Church do 3.

Three : Num
Three = s => z => Doit3times s z

Complete as definições das seguintes funções. Certifique-se de que os testes unitários correspondentes sejam aprovados, provando-os com Equal.refl

Sucessor

Sucessor de um número natural:

Succ (n: Num) : Num
Succ n = ?

Succ_1 : Equal (Succ Zero) (One)
Succ_1 = ?

Succ_2 : Equal (Succ One) (Two)
Succ_2 = ?

Succ_3 : Equal (Succ Two) (Three)
Succ_3 = ?

Adição

Adição de dois números naturais:

Plus (n: Num) (n: Num) : Num
Plus n m = ?

Plus_1 : Equal (Plus One Zero) (One)
Plus_1 = ?

Plus_2 : Equal (Plus Two One) (Plus One Two)
Plus_2 = ?

Plus_3 : Equal (Plus (Plus Two Two) Three) (Plus One (Plus Three Three))
Plus_3 = ?

Multiplicação

Mult (n: Num) (m: Num) : Num
Mult n m = ?

Mult_1 : Equal (Mult One One) One
Mult_1 = ?

Mult_2 : Equal (Mult Zero (Plus Three Three)) Zero
Mult_2 = ?

Mult_3 : Equal (Mult Two Three) (Plus Three Three)
Mult_3 = ?

Exponenciação

Não é possível fazê-lo funcionar com Exp (n: Num) (m: Num) : Num. O polimorfismo desempenha um papel crucial aqui. No entanto, escolher o tipo certo para iterar pode ser complicado. Se você encontrar um erro de "inconsistência", tente iterar em um tipo diferente: o próprio Num geralmente é problemático.

Exp (n: Num) (m: Num -> Num) : Num
Exp n m = ?

Exp_1 : Equal (Exp Two Two) (Plus Two Two)
Exp_1 = ?

Exp_2 : Equal (Exp Three Two) (Plus (Mult Two (Mult Two Two)) One)
Exp_2 = ?

Exp_3 : Equal (Exp Three Zero) One
Exp_3 = ?

Predecessor

Pred (n: Num -> Num) : Num
Pred n = ?

Pred_1 : Equal (Pred Zero) (Zero)
Pred_1 = ?

Pred_2 : Equal (Pred Two) (One)
Pred_2 = ?

Pred_3 : Equal (Pred Three) (Two)
Pred_3 = ?

Subtração

Sub (n: Num) (m: Num) : Num
Sub n m = ?

Sub_1 : Equal (Sub One Zero) (One)
Sub_1 = ?

Sub_2 : Equal (Sub Two Two) (Sub One One)
Sub_2 = ?

Sub_3 : Equal (Sub Three One) Two
Sub_3 = ?