Qual é o modelo popular da lógica linear?

23

Provavelmente, a aplicação mais comum de tipos lineares no PL é usá-los para fornecer linguagens que controlam o aliasing (ou seja, um valor linear tem um único ponteiro para ele, mais ou menos).

Mas há uma pequena incompatibilidade entre esse uso e os modelos denotacionais típicos da lógica linear. IIRC, Benton mostrou que, se uma categoria fechada cartesiana tem uma mônada comutativa forte , então sua categoria de álgebras será simétrica fechada monoidal (isto é, um modelo de lógica linear). Mas esse teorema não se aplica ao uso de controle de alias, pois a mônada do estado não é comutativa. De fato, nos últimos anos, Simpson e seus colegas de trabalho deram cálculos para mônadas fortes em geral, que não são cálculos de termos para lógica linear.

Então, minha pergunta é: qual é a semântica denotacional de linguagens lineares com estado? Existe uma categoria fechada simétrica monoidal não degenerada (isto é, o tensor não é um produto cartesiano) na qual alocação, leitura e atualização linear podem ser modeladas?

Neel Krishnaswami
fonte
6
Esse é o tipo de pergunta que eu esperaria que você respondesse a Neel, sem perguntar. ;-)
Marc Hamann
5
se você pode atrair pesquisadores para cstheory.stackoverflow.com que sejam capazes de responder a essa pergunta, o mundo será um lugar melhor para isso.
101110 Dave

Respostas:

9

Parece-me que a direção que você deve considerar gira em torno da semântica de jogos para referências gerais e a semântica relacionada à lógica linear, como aquelas baseadas nos jogos de Conway . Um relato algébrico de referências na semântica de jogos de Paul-André Melliès e Nicolas Tabareau é provavelmente o melhor lugar para começar. Neste artigo, a lógica linear é simplificada para a chamada lógica tensorial, para que as coisas funcionem, portanto não é exatamente a configuração desejada. Mas eles confiam nos jogos da Conway, então certamente há uma conexão com os modelos de lógica linear. Eles também realmente não exploram a linearidade como nos tipos lineares, mas a maquinaria existe para fazer isso, se você quiser, acredito.

O trabalho de Jim Laird (como A Game Semantics of Names and Pointers ) e Guy McCusker também pode contribuir para sua busca. A recente tese interessante Semântica de jogos para uma linguagem orientada a objetos de Nicholas Wolverson empurra essas idéias ainda mais em um cenário OO. Ele considera detalhadamente o encadeamento linear , apenas uma operação ativa por vez, e descreve como adicionar classes lineares . Ambos contam com digitação linear. Novamente, no entanto, o modelo subjacente não é estritamente um modelo de lógica linear, mas está próximo.

Dave Clarke
fonte
1
Apenas curioso Neel. Isso foi útil para você ou você já sabia de todas essas coisas?
Dave Clarke
T(A)=SA×S
1
Talvez o estado Global de Uday Reddy seja considerado desnecessário: Uma introdução à semântica baseada em objetos, J. Lisp e Symbolic Computation, 9 (1996): 7-76.
Dave Clarke
Estou lendo isso agora, na verdade!
Neel Krishnaswami
7

(Nossa, Neel, essa foi uma pergunta difícil.)

O "modelo popular" da lógica linear é definitivamente o modelo de espaços coerentes, discutido no artigo Linear Logic de Girard (e também em "Provas e tipos"). Isso não é degenerado no sentido que você descreve.

Se essa semântica lança alguma luz sobre como uma linguagem funcional linear pode ser implementada, não tenho certeza. Quando você está falando sobre alocação, leitura e atualização linear, está realmente falando sobre a implementação. Então, talvez, sua pergunta possa ser formulada como "como posso provar a implementação de uma linguagem funcional linear que usa atualização de estado?" Não sei a resposta para isso, mas acho que deve existir nos documentos que propõem implementações lineares de atualização.

Uday Reddy
fonte
Na verdade, é muito fácil provar a correção das implementações do estado linear - a linearidade é uma restrição estrutural tão forte que você quase não precisa de nenhuma semântica para fazer essas provas. Como resultado, não conheço uma semântica denotacional simples de estado linear. As duas coisas mais próximas do que eu quero são seu trabalho sobre semântica baseada em objetos e o modelo de "espaços de comprimento" de Hofmann em seu trabalho sobre complexidade implícita.
Neel Krishnaswami
Na verdade, eu não descreveria a semântica baseada em objetos como modelagem de "estado linear". É bastante "estado seqüencial" e "objetos lineares", sendo o latte imposto pelo SCI. Os modelos de jogos do Algol Idealizado, que também são "baseados em objetos" no mesmo sentido, não possuem nada linear.
Uday Reddy
Você pode fazer algumas referências sobre onde essas provas de correção podem ser encontradas? (Desculpe, virando as costas pergunta para você!)
Uday Reddy
1
A prova de som mais simples para uma linguagem linear com o estado que conheço é "L3: uma linguagem linear com locais", de Ahmed, Fluet e Morisett. ( ttic.uchicago.edu/~amal/papers/linloc-fi07.pdf ) No artigo, eles fornecem uma relação lógica simples, mas mencionam que uma prova sintática de progresso e preservação também passa.
Neel Krishnaswami
Aqui está outro trabalho que me chamou a atenção. Experimente o citeseer para Stephen Cooper, no link "Tipos lineares e atualização imperativa" . Eu deveria saber disso, mas não sabia.
Uday Reddy