Parametricidade da Lógica Linear

9

Somos capazes de provar um teorema de parametridade livre sobre funções como f:A.[A][A] ? Supõe-se que f pega uma lista e sempre retorna uma permutação dela.

Outro exemplo: prove que a função f:A.(A(A,A))[A][A] sempre retornará uma lista permutada com exatamente um elemento copiado.

Łukasz Lew
fonte
1
Sim, isso é possível. Nós exploramos esse tema em um cenário um pouco diferente (o cálculo \ pi- cálculo linear polimórficoπ ).
Martin Berger

Respostas:

7

Várias pessoas estão interessadas em provar esse tipo de coisa. Neel Krishnaswami mencionou esse teorema em particular aqui . Também vi Frank Pfenning dar alguns exemplos interessantes de lógicas ordenadas. Por exemplo, se você tiver , em um sistema de tipos ordenados, deve anexar as listas e .A,x:[A],y:[A]e:[A]exy

A resposta curta é que sim, podemos provar seu primeiro exemplo. No contexto do cálculo lambda, uma abordagem lógica baseada em relações é descrita neste artigo . Eles provariam seu teorema em duas etapas:

  1. Defina uma interpretação relacional dos tipos e use-a para provar um teorema livre convencional ignorando completamente a linearidade, ou seja, usando essencialmente o mesmo raciocínio que você vê em, por exemplo, "Teoremas de graça!". Dado , o teorema livre usual nos diz que retorna uma lista que contém apenas elementos que estavam presentes na lista que foi fornecida. Dada uma lista de variáveis ​​lineares distintas livres , deduzimos que avaliado para alguma lista que .f:A.[A][A]fx1xnf[x1,...,xn][y1,...,ym]{y1,,ym}{x1,...,xn}
  2. Observe que variáveis ​​lineares livres devem ser preservadas sob avaliação. Isso nos permite tirar proveito da linearidade. Se não fosse uma permutação de , isso implicaria que alguns foram perdidos ou duplicados durante a avaliação, o que não pode acontecer.[y1,,ym][x1,...,xn]xi

Porém, esses tipos de teoremas ficam mais interessantes quando analisamos uma linguagem com efeitos e nossa capacidade de prová-los para essas linguagens é tristemente limitada. Por exemplo, considere o isomorfismo do Sistema F. Em uma configuração de chamada por valor, esse isomorfismo é interrompido quando adicionamos não terminação. Porém, devemos recuperar um isomorfismo semelhante com tipos lineares: . Infelizmente, não temos relações lógicas operacionais que possam provar isso.τA.(τA)AτA.(τA)A

Dito isto, também existem métodos sintáticos que podem provar esse isomorfismo e seu teorema. Essa parece ser uma abordagem particularmente útil em um cenário linear e é muito menos onerosa do que estabelecer uma relação lógica para provar teoremas simples.

Edit: Desde que você perguntou, aqui está um exemplo de uma prova sintática de um teorema livre para o tipo em uma configuração com um termo que fica em loop para sempre e é bem digitado em qualquer contexto e tipo. A idéia é encontrar um conjunto de termos canônicos de um tipo e usá-lo para determinar quais são os possíveis valores de retorno para uma função. Começamos com um teorema da solidez para termos bem digitados.A.(AA)A

Teorema (Canonicidade). If entãoΔ;Γe:τ

  • ev , que é um valor tal que .Δ;Γv:τ
  • en , um termo que está bloqueado porque está tentando usar uma variável livre em e OUΓΔ;Γn:τ
  • e

Aqui, é sua noção favorita de equivalência para o idioma e é um ambiente que contém variáveis ​​de tipo livre. Considerarei variáveis ​​livres como valores. Para linguagens simples, um argumento direto de progresso e preservação pode ser feito para justificar esse teorema.Δx

Agora, com um valor , sabemos que onde . Do tipo de e, temos alguns casos possíveis:f:A.(AA)Afλx.eA;x:(AA)e:A

  • e é equivalente a um par . Este caso é impossível, pois e devem ser valores do tipo , que é uma variável de tipo livre. Não existem tais valores, pois não há variáveis no contexto de tipo .A;x:(AA)(v1,v2):Av1v2AA
  • e é equivalente a um termo que tenta usar a variável livre .x
  • e diverge. Este caso nos fornece um valor possível para : .fλx.

Como o segundo caso é o único que resta, assumimos onde . Até agora na prova, estabelecemos que . Finalmente, aplicamos nosso teorema de canonicidade mais uma vez e descobrimos que deve divergir: os únicos valores do tipo são variáveis, mas temos duas variáveis ​​no contexto, portanto não pode ser o caso que .e let(x1,x2)=x in eA;x1:A,x2:Ae:Afλx.let (x1,x2)=x in eeAexi

Portanto, temos que o único habitante de todos é é .A.(AA)Aλx.λx.let (x1,x2)=x in 

Você pediu uma referência para esse tipo de prova, mas não tenho certeza de uma boa. Esse tipo de raciocínio é bem conhecido em certos círculos e remonta talvez até Gentzen. Disseram-me que é uma reminiscência da pesquisa de provas focada em cálculo sequencial, mas não sei exatamente qual é a conexão.

Dito isto, não conheço nenhum trabalho publicado moderno que explique bem esse método relativamente simples. É certo que é um pouco limitado em sua aplicabilidade a idiomas mais simples. Por outro lado, acho que foi ofuscado por "Teoremas de graça!" et al. e, como resultado, muitos pesquisadores seniores imediatamente pensam em relações lógicas quando ouvem a frase "teorema livre", sem saber que técnicas como essa podem ser uma abordagem alternativa mais simples a essas provas (especialmente no contexto de sistemas de tipos lineares).

Quanto ao seu segundo exemplo, não acho que o teorema livre que você deseja tenha. Eu poderia, por exemplo, instanciar com o tipo inteiro e depois passar uma função que retorna números inteiros que não estão na lista que dou para . Talvez esteja mais próximo do tipo que você tinha em mente. Mas, mesmo assim, nenhuma função do tipo existe, pois ela teria que duplicar sua entrada.AfA.(B.B(B,B))[A][A]B.B(B,B)

Nick Rioux
fonte
Você pode dar uma referência para esse método sintático de que você fala?
Łukasz Lew
Não tenho certeza de uma boa referência, mas adicionei um exemplo ao post. Deixe-me saber se algo não está claro.
Nick Rioux
1
Não linear, mas aqui está um blog sobre o uso de análises teóricas da prova para obter teoremas do tipo paramtricidade
Max New
Além do artigo de Zhao et al, publicado no post, Lars Birkedal e seus co-autores estenderam também o modelo paramétrico de Reynolds ao caso linear em seu artigo Linear Abadi e Plotkin Logic .
Neel Krishnaswami
Isto é interessante. Mas será que pretende ser equivalência beta, equivalência beta-eta ou equivalência observacional? Para estabelecer a teoria da equivalência observacional, você normalmente precisa de relações lógicas, mesmo para muitos fatos básicos. Uma referência à qual lógica linear você está usando também seria útil - você usa eta para pares, mas se isso é válido geralmente é sutil (pelo menos em contextos não lineares).
Blaisorblade