Cálculo Lambda: unindo computação e lógica · AGENDA 1.CálculoLambdaSemTipos • Sintaxe • Semântica • Propriedades 2.CálculoLambdacomoModelodeComputação • Operaçõeslógicas

CÁLCULO LAMBDA: UNINDOCOMPUTAÇÃO E LÓGICA

Rodrigo Machado28 de Novembro de 2017

ALGUMAS PERGUNTAS INICIAIS

• Qual modelo de computação universal é mais conhecido em Ciênciada Computação?

• Quem sabe quem foi Alonzo Church?• Quem sabe o que quer dizer correspondência Curry-Howard?• Quem já utilizou um assistente de prova?• Quem programa em Haskell ou Ocaml?• Qual a grande novidade do Java 8?• O que é inferência de tipos?• Qual o aspecto comum a todas as respostas acima?• Por que um tutorial em 2017 sobre um tópico anterior à segunda

guerra mundial?

2

OBJETIVOS DESTE TUTORIAL

Apresentar uma visão geral sobre diversas versões do Cálculo Lambda, ealguns pontos importantes de sua história.

Detalhar o cálculo lambda como:• modelo de computação• lógica

Motivar a aplicabilidade dos conceitos formais por meio de duas vertentes:linguagens de programação e sistemas de prova.

3

AGENDA

1. Cálculo Lambda Sem Tipos• Sintaxe• Semântica• Propriedades

2. Cálculo Lambda como Modelo de Computação• Operações lógicas• Operações aritméticas• Pares ordenados• Pontos fixos e recursão

3. Cálculo Lambda Tipado• Tipos simples• Polimorfismo• Tipos parametrizados• Tipos dependentes

4. Cálculo Lambda como Lógica• Proposições como Tipos• Codificações lógicas

5. Aplicações• Linguagens Funcionais• Assistentes de Prova

6. Conclusões4

1 CÁLCULO LAMBDA SEM TIPOS

CÁLCULO LAMBDA

O cálculo lambda foi proposto nadécada de 30 por Alonzo Church.

Um cálculo de funções,formalizando essencialmentedefinição e aplicação das mesmas.

Church e seus alunos Stephen ColeKleene e John Barkley Rossermostraram que esse formalismo étão expressivo quanto outrosmodelos de computação propostos.

Alonzo Church

Kleene Rosser5


CÁLCULO LAMBDA: ORIGEM

Considere a seguinte definição matemática:

f(x) = x2 + 7

A igualdade acima está definindo uma função f, que consome um númeroe devolve um número.

f(3) = 32 + 7 = 16

A igualdade acima está aplicando a definição de f a um valor específico.

O propósito original da notação lambda foi resolver a seguinteambiguidade:

f(e) = e2 + 7

Afinal, se trata da aplicação de f sobre a constante e = 2.716 . . . ou dadefinição de f?

6


CÁLCULO LAMBDA: ORIGEM (2)

A notação lambda permite diferenciar claramente a definição de umafunção de sua respectiva aplicação.

f = λx.x2 + 7

Acima temos a definição da função. O λx indica que x deve serinterpretado como um parâmetro formal, isto é, um nome temporário parao valor a ser recebido pela função.

f(3) = (λx.x2 + 7)(3) = 32 + 7

Acima temos a aplicação da função f, definida anteriormente, ao valor 3.

Note que o significado da aplicação é a substituição do parâmetroformal x pelo valor concreto 3.

7

1 CÁLCULO LAMBDA SEM TIPOSSINTAXE

SINTAXE FORMAL DE PRÉ-TERMOS

Sintaxe (pré-termos)

x, y, z ∈ VarM,N ∈ Λ

–

M,N ::= x | M N | λx.M

Exemplos:xx yλx.x(λx.x) yλx.(x y)(λx.x) (λx.x)

Nota: cada termo é uma árvore desintaxe

x λy.(λx.x y)(z w)

m

@

λy

@

@

wz

λx

@

yx

x

8


VARIÁVEIS LIVRES, LIGADAS E SUBSTITUIÇÃO

Dentro do pré-termo λx.M, dizemos que M é o escopo de λx. Umaocorrência de x dentro do escopo de λx é dita ligada. Caso contrário, xocorre livre.

Exemplo: no termo λa.a b, temos que a ocorre ligada, e b ocorre livre

A notação M [x ← N] descreve o termo resultante da substituição detodas as ocorrências livres de x em M por N, evitando captura devariáveis livres.

Exemplo: o resultado da substituição (λa.a b)[b← (z z)] é λa.a (z z)

9


EQUIVALÊNCIA ALFA

Dois pré-termos M e N são ditosα-equivalentes (M =α N) sss elesdiferem somente na escolha dosnomes de variáveis ligadas.

Exemplo: λx.x y =α λz.z y eλx.x y 6=α λy.y y

Um termo lambda é uma classe deequivalência de pré-termosα-equivalentes.

Exemplo: o termo identidade é{ λx.x, λy.y, λz.z, . . .}

Definição: Λ = Λ–/=α

pré-termos

termos

10

1 CÁLCULO LAMBDA SEM TIPOSSEMÂNTICA

REDEXES E FORMAS NORMAIS

Um redex (reducible expression) é um subtermo de M com o formato

(λx.P) Q

e o seu respectivo contractum é

P[x ← Q]

Um termo que não contenha nenhum redex é chamado forma normal (outermo irredutível).

Exemplo:

a) λy.(λx.y x) ((λy.x) y) contém dois redexesb) λx.λy.x x é uma forma normal

11


REDUÇÃO BETA

Redução beta descreve a avaliação de termos lambda através desubstituição.

Dizemos que M beta-reduz para N, denotado M→β N, se obtivermos N apartir da contração de algum redex de M.

Exemplo:(λz.λx.x z) y →β λx.x y

λy.(λx.y x) ((λy.x) y) →β λy.(λx.y x) x

Denotamos M �β N quando M reduz para N em 0 ou mais passos deredução beta (é o fecho transitivo e reflexivo da redução beta).

12


EQUIVALÊNCIA BETA

Equivalência beta identificatermos que possuem reescritasconfluentes:

M �β P N �β PM =β N

Dizemos que um termo M possuiforma normal sss M =β N e N éuma forma normal.

Exemplo:(λx.x x) a possui forma normalΩ = (λx.x x) (λx.x x) não possuiforma normal (ele β-reduz para simesmo)

termosredução beta

...

forma normal

beta-equivalência

13


ESTRATÉGIAS DE AVALIAÇÃO

Um termo P pode ter diversos redexes e, portanto, avaliar para distintostermos. Uma estratégia de avaliação é uma escolha fixa para todos ostermos de qual redex tem prioridade na redução.

Avaliação normal:• mais à esquerda, mais externo• realiza a aplicação sem

normalizar a função ou osargumentos

Avaliação aplicativa (estrita):

• mais à esquerda, mais interno

• normaliza a função e todos osargumentos antes de realizar aaplicação

Exemplo:

• normal: ((λx y.x) I Ω) →β (λy.I) Ω →β I• aplicativa: ((λx y.x) I Ω) →β (λy.I) Ω →β (λy.I) Ω →β . . .

14

1 CÁLCULO LAMBDA SEM TIPOSPROPRIEDADES

PROPRIEDADES DO CÁLCULO LAMBDA

Teorema: (Confluência, Church-Rosser) se N←β M→β N′ então existe Ptal que N �β P �β N′

Teorema: se o termo M possui forma normal N, então avaliar M usando aestratégia normal certamente alcança N.

Nota:

• nem todo termo possui forma normal.• a avaliação estrita nem sempre alcança a forma normal.• determinar equivalência beta de termos é um problema indecidível.

15

2 CÁLCULO LAMBDA COMO MODELO DE COMPUTAÇÃO

CÁLCULO LAMBDA COMO MODELO DECOMPUTAÇÃO UNIVERSAL

A linguagem de termos lambda juntamente com a redução beta (e umaestratégia de avaliação fixa) compõe um modelo de computação.

Podemos enxergar a seguinte associação:• termo lambda = estado da máquina• redução beta = passo de execução da máquina• formas normais = valores finais (parada da máquina)

Todas as funções Turing-computáveis podem ser descritas em cálculolambda.

16

2 CÁLCULO LAMBDA COMO MODELO DE COMPUTAÇÃO

CODIFICAÇÕES

Como a linguagem lambda pura provê somente variáveis, abstração lambdae aplicação de termos a termos, é necessário codificar em termos lambda

Dados:• valores booleanos e operações

lógicas• números, operações aritméticas

e operações relacionais• coleções: pares e listas

Estruturas de controle:• execução condicional• definições locais• recursão

Nota: nessas codificações o foco não é eficiência!

17

2 CÁLCULO LAMBDA COMO MODELO DE COMPUTAÇÃOOPERAÇÕES LÓGICAS

BOOLEANOS

Definição: booleanos de Church:

true = λx y . xfalse = λx y . y

Definição: construção if-then-else :

if a then b else c = λa b c . a b c

Ideia: aplicar o booleano resultante do teste sobre os valores a seremretornados.

Justifica a definição de valores-verdade como seletores.

18

2 CÁLCULO LAMBDA COMO MODELO DE COMPUTAÇÃOOPERAÇÕES ARITMÉTICAS

NÚMEROS NATURAIS

Definição: numerais de Church:

0 = λf x . x1 = λf x . f x2 = λf x . f (f x)3 = λf x . f (f (f x))...

n = λf x .n︷︸︸︷

f (f (f . . . (f x) . . .))

Também referenciados por cn, para n ∈ N.

19


OPERAÇÕES ARITMÉTICAS: SUCESSOR

Função sucessor:succ = λn p q . p (n p q)

Ideia da construção:1. receber um numeral de Church n com estrutura

n = λf x . f (f . . . (f x) . . .)

2. o resultado deve ter p e q ligados por lambdas:

λp q . . . .

3. o termo (n p q) muda os f’s em p’s, e o x em q.4. por último, introduzimos um p adicional ao número.

20


OPERAÇÕES ARITMÉTICAS E RELACIONAIS

Definição: operações aritméticas básicas:

add = λ m n p q . m p (n p q)mult = λ m n p q . m (n p) qexp = λ m n . n m

Definição: teste de zero:

isZero = λn . n (λx.false) true

Nota: a função predecessor é trabalhosa e será vista posteriormente.

21

2 CÁLCULO LAMBDA COMO MODELO DE COMPUTAÇÃOPARES ORDENADOS

PARES ORDENADOS

Definição: um par (M,N) pode ser representado por pair M N onde

pair = λ m n b. b m n

Exemplo:pair 0 true = λb. b 0 true

Definição: funções de acesso ao conteúdo de um par

fst = λp. p truesnd = λp. p false

22

2 CÁLCULO LAMBDA COMO MODELO DE COMPUTAÇÃOPARES ORDENADOS

PARES ORDENADOS: PREDECESSOR

Usando pares podemos definir pred : N→ N onde

pred(n) ={

0 se n ≤ 1n – 1 caso contrário

Função auxiliar: shiftInc(a, b) = (b, b + 1)

shiftInc = λp.pair (snd p) (succ (snd p))

Definição: o termo pred abaixo implementa a função pred

pred = λn.fst (n shiftInc (pair 0 0))

23

2 CÁLCULO LAMBDA COMO MODELO DE COMPUTAÇÃOPONTOS FIXOS E RECURSÃO

PONTOS FIXOS: COMBINADOR Y

Chamamos o termo abaixo de combinador Y (ou combinador de pontofixo)

Y = λf.(λx.f(x x))(λx.f(x x))

Teorema: o combinador Y produz um ponto fixo para seu argumento

Demonstração: YS →β(λx.S(x x)) (λx.S(x x)) →β

S (λx.S(x x)) (λx.S(x x)) =βS(YS)

YS =β S(YS) e, portanto, YS é um ponto fixo de S

Utilizando o combinador Y, podemos construir cadeias “infinitas” (sobdemanda) de expressões if-then-else, simulando recursão.

24


PONTOS FIXOS: COMBINADOR Y EM AÇÃO

@

�Y →β

@

λx

@

@

xx

�

λx

@

@

xx

�

→β

@

@

λx

@

@

xx

�

λx

@

@

xx

�

�

→β

@

@

@

λx

@

@

xx

�

λx

@

@

xx

�

�

�

�β

@

@

@

@

@

@

. . .�

�

�

�

�

�

25


PONTOS FIXOS: COMBINADOR Y EM AÇÃO (2)

se S =βλ X

λ n

if

mult

X

(pred n)

n

1(isZero n)

26


PONTOS FIXOS: COMBINADOR Y EM AÇÃO (3)

então (Y S) =β

λ n

if

mult

if

mult

if

mult

· · ·(pred (pred n))

1(isZero (pred (pred n)))

(pred n)

1(isZero (pred n))

n

1(isZero n)

27


FUNÇÕES RECURSIVAS E OPERADOR Y

Usando Y podemos codificar funções como termos nos baseando em suasdefinições recursivas.

Definição recursiva:

fact(n) ={

1 se n ≤ 1n ∗ fact(n – 1) caso contrário

Combinador:

F = λM.λn.if (isZero (pred n))1(mult n (M (pred n)))

Definição final: fact = YF

28


UNIVERSALIDADE

Sendo possível definir:• booleanos e condicionais• aritmética natural• estruturas de dados• recursãotemos os componentes de uma linguagem de programação que permiterepresentar qualquer algoritmo.

A avaliação de termos lambda pode entrar em laço infinito, visto que nemtodo termo possui forma normal.

29

3 CÁLCULO LAMBDA TIPADO

TIPOS SIMPLES

Motivação: considere• if = λa b c.a b c• 2 = λf x.f (f x)• 3 = λf x.f (f (f x))

Pergunta: qual o resultado da avaliação expressão if 2 2 3 visto que2 6= true e 2 6= false ?

Resposta: algum termo “estranho” (no caso, 81)

Em outras palavras não há uma noção de compatibilidade entre funções eargumentos: podemos aplicar qualquer termo a qualquer outro termo(inclusive realizar uma auto-aplicação).

30

3 CÁLCULO LAMBDA TIPADOTIPOS SIMPLES

TIPOS SIMPLES

Podemos utilizar tipos para categorizar termos da linguagem.

Definição: linguagem de tipos

T ::= α, β, γ, . . . tipos básicos| T→ T tipos funcionais

Exemplo:

α α→ αα→ β α→ (α→ α)(α→ α)→ (β→ β) (α→ β)→ γ

31


INTERPRETAÇÃO DE TIPOS

Tipos básicos (referenciado por α) podem ser interpretados como tiposprimitivos disponíveis em uma dada arquitetura de computador (tais comobooleanos ou inteiros)

Tipos funcionais (referenciados por T1 → T2) são tratados como funçõesque recebem elementos do domínio T1 e geram elementos docontradomínio T2.

Exemplo: 42 : Nλx.x + 1 : N→ N

λf. λx. f(f x) : (N→ N)→ N→ N

Notação: a expressão e : T significa "termo e é do tipo T"

32


AMBIENTES DE TIPOS

Definição: um ambiente de tipos Γ é uma sequência de atribuições detipos para variáveis x, y, z, . . . ∈ Var.

Exemplo:

• Γ1 = ε

• Γ2 = x : Int, y : Bool, f : Int→ Int

Ambientes pode ser• consultados: Γ2(x) = Int• atualizados: Γ3 = Γ2, x : Bool

33


JULGAMENTO DE TIPO

Notação: um julgamento de tipo

Γ ` e : T

é uma afirmação de que o termo e é do tipo T sob ambiente Γ.

Exemplo: x : α, y : β ` x : α

Definição: um sistema de tipos é uma coleção de regras de dedução quepermitem construir julgamentos de tipos

34


CÁLCULO LAMBDA TIPADO SIMPLES

Sintaxe:e ::= x | e e′ | λx :T.e

Exemplo: λx :α.λy :β.y

Sistema de Tipos

Γ(x) = TΓ ` x : T

(Var)

Γ ` e : T→ T′Γ ` e′ : T

Γ ` e e′ : T′ (App)

Γ, x : T ` e : T′

Γ ` λx :T.e : T→ T′ (Lam)

35


SISTEMA DE TIPOS SIMPLES: PROPRIEDADES

O Cálculo Lambda Tipado Simples possui diversas propriedadesinteressantes:• Confluência: se e→β e1 e e→β e2, então existe e′ tal que e1 �β e′

e e2 �β e′

• Preservação de tipos: se Γ ` e : T e e→β e′, então Γ ` e′ : T• Normalização: se ε ` e : T então existe forma normal e′ tal que

e �β e′

Diversos termos importantes do cálculo lambda sem tipos não sãotermos válidos de λ→. Por exemplo, não há tipo possível para o termo

λx :?.x x

O Cálculo Lambda Tipado Simples não é Turing-completo. Todos ostermos possuem forma normal.

36


CUBO LAMBDA

O Cálculo Lambda Tipado Simples somente apresenta abstração de termospara termos. Isso pode ser generalizado:

Dependências entretipos e termos

e //

��

e

: :

T

@@

// T

Cubo lambda

λC

λω

λ2

λ→

Tipos parametrizados

OO

Tipos dependentes//

Polimorfismo==

λP37

3 CÁLCULO LAMBDA TIPADOPOLIMORFISMO

POLIMORFISMO

Slogan: termos que dependem de tipos.

Polimorfismo = poli (múltiplas) + morfos (formas). Duas interpretaçõesprincipais:• uma única definição de rotina aplicável em diversos cenários distintos

(polimorfismo paramétrico, “generics”)• uma coleção de rotinas distintas que compartilham o mesmo nome,

sendo a escolha de qual será usada determinada pelo contexto(polimorfismo ad-hoc, overloading)

Exemplo: (em Haskell)

1 ident :: forall a. a -> a2 ident x = x3 foo1 = 1 + 14 foo2 = 1 + 4.0

38

3 CÁLCULO LAMBDA TIPADOTIPOS PARAMETRIZADOS

TIPOS PARAMETRIZADOS

Slogan: tipos que dependem de tipos (construtores de tipos)

Considere as seguintes definições de listas em Haskell.

1 data ListaInt = Nempty2 | Ncons Int ListaInt3 l1 = Ncons 3 (Ncons 5 Nempty)

1 data ListaChar = Cempty2 | Ccons Char ListaChar3 l2 = Ccons 'a' (Ccons 'b' (Ccons 'c' Cempty ))

Note que os dois tipos são similares: onde o único ponto de variação é otipo do dado armazenado na lista.

39

3 CÁLCULO LAMBDA TIPADOTIPOS PARAMETRIZADOS

TIPOS PARAMETRIZADOS

Slogan: tipos que dependem de tipos (construtores de tipos)

Possibilidade: abstrair o tipo de listas como um construtor de tipos, isto é,uma função List : Type→ Type

1 data List a = Empty2 | Cons a (List a)3

4 l3 = Cons 4 (Cons 2 Empty)

Nota: em Haskell, tipos básicos são referenciados por ?. Expressõesformadas por ? e → são chamadas “kinds” (ou “tipos dos tipos”)

Exemplo: List : ?→ ?

40

3 CÁLCULO LAMBDA TIPADOTIPOS DEPENDENTES

TIPOS DEPENDENTES

Slogan: tipos que dependem de termos (famílias de tipos indexadaspor valores).

Exemplo: listas com tamanho fixo (vec) em Coq.

1 Inductive vec : nat -> Type :=2 | nil : vec 03 | cons : forall (n:nat),4 nat -> vec n -> vec (S n).

Nessa linguagem podemos criar versões de operações como indexação,soma elemento-a-elemento e concatenação que carregam o tamanhoda estrutura como parte do tipo.

41


CÁLCULO DE CONSTRUÇÕES

Cálculo de construções: λC

λC = λ→ + λ2 + λω+ λPλC

λω

λ2

λ→

OO

//

==

λP

O cálculo λC inclui polimorfismo,construtores de tipos e tipos

dependentes.

Apesar desta extensões, mantémcaracterísticas importantes de λ→como normalização forte econfluência.

Muitos termos que não sãobem-tipados em λ→ podem tertipos atribuídos em λC.

Exemplo: auto-aplicação λa.a a

42


SINTAXE

Sintaxe de λC

A,B ::= � (tipo de todos os kinds)| ? (tipo dos tipos simples)| x (variáveis)| A B (aplicação )| λx :A.B (dependência funcional)| Πx :A.B (produto dependente)

K é um kind ⇔ ` K : �T é um tipo ⇔ ` T : K : �

E é um termo ⇔ ` E : T : K : �

Açúcar sintático:• A→ B é açúcar sintático para Πx :A.B para x /∈ FV(B).• ∀T.B é açúcar sintático para ΠT:?.B

43


SISTEMA DE TIPOS

Conformidade: Γ ` A (todas as variáveis em A estão declaradas em Γ e sãoconsistentes)

(s1, s2) ∈ {(?, ?), (?,�), (�, ?), (�,�)}

Sistema de tipos

ε ` ? : � (sort)

Γ ` A : s x /∈ ΓΓ, x : A ` x : A

(var)

Γ ` A : B Γ ` C : s x /∈ ΓΓ, x : C ` A : B

(weak)

Γ ` A : s1 Γ, x : A ` B : s2Γ ` Πx :A.B : s2

(form)

Γ ` M : Πx :A.B Γ ` N : AΓ ` M N : B[x ← N]

(appl)

Γ, x : A ` M : B Γ ` Πx :A.B : sΓ ` λx :A.M : Πx :A.B

(abst)

Γ ` A : B Γ ` B′ : s B =β B′

Γ ` A : B′

(conv)

44


SEMÂNTICA

Semântica

(λx : A.B) C→β B[x ← C] (beta)

(Πx : A.B) C→β B[x ← C] (betaPi)

Nota: distinção entre termos e tipos exclusivamente por conta do sistemade tipos (mesma linguagem)

45

4 CÁLCULO LAMBDA COMO LÓGICAPROPOSIÇÕES COMO TIPOS

LÓGICA E CÁLCULO LAMBDA

Um similaridade interessante surge quando comparamos regras de lógica eregras de tipos do cálculo lambda tipado simples:

Exemplo: Modus Ponens

A→ B AB

(MP)

Exemplo: Regra da aplicação

Γ ` f : A→ B Γ ` x : AΓ ` f x : B

(APP)

A única diferença está na forma como registramos as subprovas (árvores dededução vs ambientes e termos).

46


PROPOSIÇÕES COMO TIPOS

Cada versão do cálculo lambda tipado corresponde a um sistema dedutivode uma lógica (intuicionista).• λ→ : lógica proposicional minimal• λ2 : lógica proposicional de segunda ordem• λP : lógica de predicados de primeira ordem minimal

Um cálculo lambda tipado pode ser considerado tanto um modelo decomputação quanto uma lógica.

A conexão entre essa visões é denominada Correspondência Curry-Howardou Proposições como Tipos, na qual• tipos da linguagem são vistos como fórmulas lógicas (proposições)• termos (bem-tipados) são vistos como provas do respectivo tipo

47


HABITAÇÃO DE TIPOS

Um tipo T é habitado se existe termo e tal que ` e : T.

A seguinte interpretação é utilizada:• se um tipo é habitado, ele possui uma prova. Portanto, a proposição

é verdadeira.• se um tipo não é habitado, ele não possui prova. Portanto, a

proposição é falsa.

Exemplo: em λC• ΠX:?.X→ X é habitado pelo termo λX:?.λx :X.x• ΠX:?.X não é habitado, pois não conseguimos construir um

expressão que escolhe um termo a partir de um tipo qualquer.Nota: podemos utilizar ΠX:?.X como ⊥ (falso), e ΠX:?.X→ X como >(true).

48

4 CÁLCULO LAMBDA COMO LÓGICACODIFICAÇÕES LÓGICAS

CODIFICAÇÃO DE OPERADORES LÓGICOS

No cálculo λC, podemos codificar lógica de predicados intuicionista:• Implicação A ⊃ B é representada diretamente pelo tipo funcional:

A→ B ou (Π_ : A.B na sintaxe de λC)• Negação ¬A pode ser codificada por A→ ΠX:?.X visto que¬A ≡ A ⊃ ⊥

• Conjunção A ∧ B é representada por ΠC:?.(A→ B→ C)→ C• Disjunção A∨B é representada por ΠC:?.(A→ C)→ (B→ C)→ C• Quantificação universal como ∀x ∈ S, P(x) é representada

diretamente utilizando o tipo dependente Πx : S.(P x)• Quantificação existencial como ∃x ∈ S, P(x) é representada

diretamente utilizando o tipo dependenteΠY : ?.(Πx : X.P x → Y)→ Y (note que x /∈ FV(Y))

49

5 APLICAÇÕES

APLICAÇÕES

Pergunta: Ok. Interessante. O que eu faço com isso?

Resposta: no mínimo as seguintes coisas bastante importantes. . .• programação de computadores• estudo formal de linguagens de programação• matemática em geral

Vou mencionar dois exemplos importantes:• Linguagem de Programação (Ex: Haskell)• Assistente de Provas (Ex: Coq)

50

5 APLICAÇÕESLINGUAGENS FUNCIONAIS

LINGUAGENS FUNCIONAIS

Não há definição exata do que é uma linguagem funcional, porém acreditoque uma boa aproximação seria:

Uma linguagem que favorece e encoraja a definição de funções ea composição das mesmas como princípio fundamental paraconstrução de programas.

Linguagens funcionais podem ser• puras (Haskell) ou impuras (OCAML, Scala, LISP)• dinamicamente tipadas (LISP, Scheme) ou estaticamente tipadas

(OCAML, Haskell)

51


LINGUAGENS FUNCIONAIS E CÁLCULOLAMBDA

Linguagens de programação estaticamente tipadas são essencialmente• cálculo lambda com constantes• sistema de tipos• estratégia de avaliação• operador de recursão (como primitiva)

Atualmente a maior parte das linguagens de programação de uso geral éhíbrida, suportando o estilo de programação funcional. Exemplo:Python, Javascript, Ruby.

Suporte a closures (termos lambda em contexto léxico) constituemnovidade importante em linguagens já estabelecidas (por exemplo, Java)

52


LINGUAGEM HASKELL

Haskell é uma linguagem de uso geral funcional pura e com avaliaçãotardia.

O sistema de tipos de Haskell suporta polimorfismo, construtores de tipo einferência de tipos.

Haskell não é a mais popular das linguagens de programação existentes,contudo ela é extremamente influente por ter disseminado conceitosimportantes como• avaliação tardia (lazyness)• programação funcional pura (sem efeitos colaterais)• mônadas como forma de estruturar código• typeclasses para integrar polimorfismo paramétrico e polimorfismo

ad-hoc

53


LINGUAGEM HASKELL: EXEMPLO DE CÓDIGO

Exemplo: Quicksort em Haskell

1 quicksort :: (Ord a) => [a] -> [a]2

3 quicksort [] = []4

5 quicksort (x:xs) =6 let7 smallSorted = quicksort [a | a <- xs, a <= x]8 bigSorted = quicksort [a | a <- xs, a > x]9 in

10 smallSorted ++ [x] ++ bigSorted

54

5 APLICAÇÕESASSISTENTES DE PROVA

ASSISTENTES DE PROVA

Um assistente de prova é uma ferramenta que auxilia determinação depropriedade e construção de provas para as mesmas, garantindo a suavalidade.

Eles diferem de provadores automatizados de teoremas ouverificadores de modelos, pois assistentes requerem intervenção humana.

Exemplo:

• Coq• Agda• Isabelle• L∃∀N

55


COQ

Coq é uma assistente de provas construído sobre uma extensão de λC(adicionando tipos indutivos como primitivas), mantendo propriedadesimportantes como consistência e normalização.

Funciona via Curry-Howard:• programas ⇔ provas• tipos ⇔ propriedades

Coq permite:• programar (restrito a um subconjunto de funções recursivas)• definir objetos matemáticos (conjuntos, listas, relações)• especificar propriedades (sobre programas e objetos matemáticos)• provar propriedades (usando uma linguagem de tática)

56


EXEMPLO DE CÓDIGO

Definição de uma lista de naturais, e uma operação de concatenação.

1 Inductive natlist :=2 | empty : natlist3 | prefix : nat -> natlist -> natlist.4

5 Example ex1 : natlist := prefix 4 (prefix 2 empty).6

7 Fixpoint append (n1 n2:natlist) : natlist :=8 match n1 with9 | empty => n2

10 | prefix h t => prefix h (append t n2)11 end.12

13 Notation " A |+| B " := (append A B)14 (at level 50, left associativity).

57


EXEMPLO DE PROVA SOBRE OPERAÇÕES

Definição de uma propriedade de natlists, e sua respectiva provautilizando a linguagem de prova.

1 Theorem app_assoc :2

3 forall (n1 n2 n3:natlist),4 (n1 |+| n2) |+| n3 = n1 |+| (n2 |+| n3).5

6 Proof.7 induction n1.8 (* n1 empty *)9 intros. simpl. reflexivity.

10 (* n1 prefix *)11 intros. simpl. rewrite IHn1. reflexivity.12 Qed.

58


EXEMPLO DE PROVA EM DEDUÇÃO NATURAL

Considere o seguinte sequente em dedução natural.

A→ B,A→ C, (B ∧ C)→ D ` A→ D

A árvore de prova da propriedade acima pode ser vista abaixo:

A1 A→ B (→e)BA1 A→ C (→e)C (∧i)B ∧ C (B ∧ C)→ D (→e)D (→i 1)A→ D

59


EXEMPLO DE PROVA EM DEDUÇÃO NATURAL(CONT.)

O seguinte script Coq constrói a árvore de prova do seguinte sequente:` (A→ B)→ (A→ C)→ (B ∧ C→ D)→ A→ D

1 Variables A B C D:Prop.2 Theorem thm1 : (A->B) -> (A->C) -> ((B/\C)->D) ->

(A->D).↪→

3 Proof.4 intros P1 P2 P3.5 intro HA.6 assert B. apply P1. assumption.7 assert C. apply P2. assumption.8 assert (B/\C). apply conj. assumption. assumption.9 apply P3. assumption.

10 Qed.

60


EXEMPLOS MAIS SIGNIFICATIVOS

Compcert C compiler• compilador C escrito em Coq• performance do código gerado comparável à do código gerado pelo

GCC• passos de tradução provados corretos• http://compcert.inria.fr/compcert-C.html

seL4 (Secure Embedded L4 microkernel)• formalização de um microkernel de sistema operacional em Isabelle

(outro assistente de prova baseado em lógica de alta ordem)• ver http://ssrg.nicta.com.au/

61

http://compcert.inria.fr/compcert-C.html

http://ssrg.nicta.com.au/

6 CONCLUSÕES

CONCLUSÕES

Cálculo lambda está presente na área da computação desde o princípio, aaproximadamente 80 anos.

Apesar de não ser popular como o modelo Máquina de Turing, é muitoinfluente e relevante em áreas como• linguagens de programação• sistemas de tipos• assistentes de prova

Estudar cálculo lambda assegura uma melhor compreensão da relaçãoentre computação e lógica, assim como ferramentas que habitam essaregião (como modernos assistentes de prova).

62

6 CONCLUSÕES

REFERÊNCIAS

Para saber mais:• programe em linguagens funcionais (ou em estilo funcional)• use assistentes de prova ao investigar matemática• referências:

63

OBRIGADO!

[email protected]

Rodrigo MachadoInstituto de Informática — UFRGS

INSTITUTODE INFORMÁTICAUFRGS

64

[email protected]

Documents

Cálculo Lambda: unindo computação e lógica · AGENDA 1.CálculoLambdaSemTipos • Sintaxe • Semântica • Propriedades 2.CálculoLambdacomoModelodeComputação • Operaçõeslógicas