Quais são as diferenças entre relações lógicas e simulações?

29

Sou iniciante trabalhando em métodos que provam equivalência de programa. Li alguns artigos sobre como definir relações lógicas ou simulações para provar que dois programas são equivalentes. Mas estou bastante confuso sobre essas duas técnicas.

Só sei que as relações lógicas são definidas indutivamente enquanto as simulações são baseadas na coindução. Por que eles são definidos dessa maneira? Quais são seus prós e contras, respectivamente? Qual devo escolher em diferentes situações?

Hongjin Liang
fonte
11
Convém fornecer links para esses documentos que você leu. Isso tornaria mais claro quais exemplos específicos estão confundindo você.
Marc Hamann
11
Para relações lógicas, li o artigo recente de Hur e Dreyer "Uma relação lógica de Kripke entre ML e montagem" (POPL'11). Também li os capítulos clássicos do livro de Pierce, "Tópicos avançados em tipos e linguagens de programação". Acho que as relações lógicas são definidas indutivamente na estrutura de tipos da linguagem, mas e se a linguagem não tiver uma estrutura de tipos (como C)? (Parece outra pergunta, eu acho.)
Hongjin Liang
11
Para simulações, li o artigo original "Leis algébricas para não determinismo e simultaneidade" de Hennessy e Milner. Os "pequenos bisimulações de Koutavas e Wand para raciocinar sobre programas imperativos de ordem superior" (POPL'06) são incompreensíveis para mim e não sei por que eles chamaram seu método de "bisimulação".
Hongjin Liang 12/03
3
seria melhor se você incluísse as informações que você forneceu nos comentários da postagem. Você pode editar sua pergunta clicando no link editar abaixo da pergunta.
Kaveh
11
@ HongjinLiang: Se você não possui uma estrutura de tipos (ou se possui tipos recursivos), pode usar relações lógicas indexadas por etapas - com relações lógicas você usa indução em tipos, com indexação por etapas você faz indução em etapas de observação. Você encontrará indicadores na declaração de pesquisa de Amal Ahmed: ccs.neu.edu/home/amal/ahmed-research.pdf . (Outra visão geral da pesquisa sobre relações lógicas é essa palestra de Derek Dreyer e em sua declaração de pesquisa: mpi-sws.org/~dreyer/research.pdf ).
Blaisorblade 24/03

Respostas:

20

Eu tenho uma resposta para esta pergunta que é possivelmente nova. De fato, ainda estou pensando nos últimos 6 meses ou mais, e ainda não foi escrito em artigos.

A tese geral é que princípios de raciocínio relacional como "relações lógicas", "simulações" e até "invariantes" são manifestações de abstração de dados ou ocultação de informações. Onde quer que oculte informação, esses princípios surgem.

As primeiras pessoas a descobri-lo foram os teóricos dos autômatos. Os autômatos têm um estado oculto. Portanto, você precisa de um raciocínio relacional para falar sobre sua equivalência. Os teóricos dos autômatos lutaram com os homomorfismos por um tempo, desistiram e criaram uma noção chamada "cobertura relacional", que é uma forma de relações de simulação.

Milner pegou a idéia em um artigo pouco conhecido, mas muito fundamental, chamado " Uma noção algébrica de simulação entre programas " em 1971. Hoare sabia disso e a usou na criação de " Prova de correção de representações de dados " em 1972 (mas usada abstração funciona em vez de relações, porque ele pensava que eram "mais simples"). Mais tarde, ele retirou a reivindicação de simplicidade e voltou a usar as relações em " Refinamento de dados refinado ". Reynolds usou o raciocínio relacional em " Craft of Programming"", Capítulo 5 (1981). Ele achava que as relações eram mais naturais e gerais do que as funções de abstração. Se você voltar e ler este capítulo, encontrará idéias de parametridade relacional à espreita, à espera de serem descobertas. Com certeza, dois anos depois, Reynolds publicou "Tipos, abstração e polimorfismo paramétrico" (1983).

Parece que todas essas idéias não têm nada a ver com tipos, mas realmente têm. Linguagens e modelos com estado têm abstração de dados incorporada . Você não precisa definir um "tipo de dado abstrato" para ocultar as informações. Você apenas declara uma variável local e a oculta. Podemos ensiná-lo aos alunos do primeiro ano nas aulas de Java nas primeiras semanas. Sem suor.

Linguagens e modelos funcionais, por outro lado, precisam esconder suas informações por meio de tipos . Os modelos funcionais não possuem abstração de dados incorporada. Temos que adicioná-lo explicitamente, usando ou . Portanto, se você traduzir um idioma com estado para um idioma funcional, notará todo o estado local sendo traduzido em variáveis ​​de tipo. Para uma descrição explícita de como isso funciona, consulte meu artigo " Objetos e classes em linguagens semelhantes a Algol ", mas as idéias realmente vêm de Reynolds 1981 ("A Essência de Algol"). Estamos apenas entendendo melhor essas idéias clássicas agora.

Pegue duas máquinas e M ' que você deseja provar equivalentes. Milner 1971 diz, define uma relação entre os estados de M e M ' e mostra que as duas máquinas preservam a relação. A parametridade de Reynolds diz: pense nos estados das máquinas como pertencendo aos tipos X e X ' . Defina uma relação R entre eles. Se as máquinas são do tipo F ( X ) e F ( X ) , parametrizadas pelos tipos de seus estados, verifique se as duas máquinas estão relacionadas pela relação FMMMMXXRF(X)F(X) . F(R)

Portanto, simulações e parametridade relacional são essencialmente a mesma idéia . Não é apenas uma semelhança superficial. O primeiro é feito para linguagens com estado onde há abstração de dados embutida. O último é feito para linguagens sem estado onde a abstração de dados é obtida por meio de variáveis ​​de tipo.

E as relações lógicas, então? Aparentemente, as relações lógicas parecem ser uma ideia mais geral. Enquanto a parametridade fala sobre como relacionar variáveis ​​de tipo dentro do mesmo modelo, relações lógicas parecem relacionar tipos entre modelos diferentes. (Dave Clarke escreveu uma exposição brilhante disso antes.) Mas meu sentimento é (e ainda precisa ser demonstrado) que esse é um exemplo de alguma forma de parametridade de tipo superior que ainda não foi formulada. Fique atento para mais progresso nessa frente.


[Nota adicionada] A conexão entre relações lógicas e simulações é discutida em nosso artigo recente Relações lógicas e parametria: Um programa de Reynolds para teoria de categorias e linguagens de programação .

Uday Reddy
fonte
Eu estava perguntando se seria verdade dizer que a relação mencionado acima, é a assim chamada elevação relação de R dada F descrevendo a máquina. F(R)Rfunctor F
21413 Dave Clarke
@DaveClarke Sim, é a mesma ideia. No estilo de definição de Reynolds, cada construtor de tipo vem equipado com uma ação de relação que associa, a cada relação R : X X , uma relação correspondente F ( R ) : F ( X ) F ( X ) satisfazendo alguns axiomas. Em algumas outras comunidades, eles gostariam de obter F ( R ) de outros princípios, donde eles chamam liftings relação . O F (FR:XXF(R):F(X)F(X)F(R) que produzem por esse processo seria uma ação de relação no sentido de Reynolds. F(R)
Uday Reddy
14

Uma das principais diferenças é que as relações lógicas são usadas como uma técnica para mostrar que uma classe de programas (por exemplo, entrada para um compilador) corresponde a outra classe de programas (por exemplo, a saída do compilador), enquanto as relações de simulação são usadas para mostrar a correspondência entre dois programas.

A semelhança entre as duas noções é que ambas definem uma relação usada para mostrar a correspondência entre duas entidades diferentes. Em certo sentido, pode-se pensar em uma relação lógica como uma relação de simulação definida indutivamente na sintaxe dos tipos. Mas existem diferentes tipos de relações de simulação.

As relações lógicas podem ser usadas para mostrar a correspondência entre um idioma como ML e sua tradução para o idioma assembly, como no artigo que você lê. Uma relação lógica é definida indutivamente na estrutura de tipos. Uma relação lógica fornece um meio de composição para mostrar, por exemplo, que uma tradução está correta, mostrando que a tradução está correta para cada tipo de construtor. Nos tipos de função, a condição de condição de correção diria algo como, a tradução dessa função leva entrada bem traduzida para saída bem traduzida.

As relações lógicas são uma técnica versátil para idiomas com base no cálculo lambda. Outras aplicações de relações lógicas incluem ( daqui ): caracterização da definibilidade lambda, relacionando definições semânticas denotacionais, caracterizando polimorfismo paramétrico, modelando a interpretação abstrata, verificando representações de dados, definindo semântica totalmente abstrata e modelando o estado local em linguagens de ordem superior.

As relações de simulação são geralmente usadas para mostrar a equivalência de dois programas. Normalmente, esses programas produzem algum tipo de observação, como o envio de mensagens nos canais. Um programa P simula outro Q se P pode fazer tudo o que Q pode fazer, embora talvez mais.

A bisimulação é, grosso modo, duas relações de simulação reunidas. Você mostra que o programa P e simula o programa Q e esse programa Q pode simular o programa P e você tem uma bimimulação, embora geralmente existam condições adicionais. A entrada da Wikipedia sobre bisimulação é um bom ponto de partida (mais preciso). Existem milhares de variantes da idéia, mas é uma idéia fundamental que foi reinventada de forma mais ou menos igual à da ciência da computação, lógica modal e teoria dos modelos. O artigo de Sangiorgi fornece uma história maravilhosa da idéia.

Um artigo que estabelece uma relação entre as duas noções é Uma Nota sobre Relações Lógicas entre Semântica e Sintaxe, de Andy Pitts, que usa relações lógicas, em última análise, uma noção semântica definida sintaticamente, para provar uma certa propriedade sobre a bisimulação aplicada , que é uma noção puramente sintática.

Dave Clarke
fonte
Muito obrigado pela sua explicação detalhada! Vou ler suas referências e tentar descobrir profundas conexões / diferenças entre os dois.
Hongjin Liang 13/03
tem certeza da afirmação "Você mostra que o programa P e simula o programa Q e esse programa Q pode simular o programa P e você tem uma bimimulação"? Seja A = (a. (B + c)) + (a.b + ac) e B = a.b + ac quando, tanto quanto eu posso dizer, A é semelhante a B, B é semelhante a A, mas A e B não é bisimilar.
András Salamon
@ András: Você está certo. Minha afirmação não é precisa o suficiente. A diferença é abstraída pela frase "Algumas condições adicionais podem estar presentes".
Dave Clarke
Hennessy e Milner definiram três tipos de relações de equivalência em seu artigo original para bisimulação e deram alguns exemplos para ilustrar suas diferenças. Sua afirmação original é na verdade a de nível médio em seu trabalho, mais fraca que a bisimulação e mais forte que a equivalência de traços. Não tenho certeza de qual equivalência é melhor. Talvez dependa de uso prático.
Hongjin Liang
A simulação também é usada como uma técnica de prova para estabelecer o refinamento de dados entre dois tipos de dados. Cada uma dessas provas de simulação relaciona classes inteiras de programas. Veja, por exemplo, [1] para detalhes. Isso sugere que a distinção entre os dois conceitos é ainda mais desfocada. [1]: CAR Hoare, He J e JW Sanders. Pré-especificação no refinamento de dados. Information Processing Letters , 25: 71-76, 1987.
Kai
8

Os dois tipos de relações parecem ser usados ​​em contextos diferentes. Simulações lógicas para linguagens digitadas e relações de simulação ao lidar com cálculos de processos ou lógicas modais interpretadas em sistemas de transição. Dave Clarke forneceu muitas explicações intuitivas, portanto, adicionarei algumas dicas que podem ajudar.

Tem havido trabalho para caracterizar as duas noções usando interpretação abstrata. Pode não ser o que você deseja, mas pelo menos as duas noções são tratadas na mesma estrutura matemática.

Samson Abramsky usou relações lógicas para provar a solidez e a análise de rigidez do cálculo preguiçoso de Lambda ( Interpretação abstrata, relações lógicas e extensões de Kan ). Ele também mostrou que as relações lógicas definem funções de abstração no sentido de conexão de Galois da interpretação abstrata. Mais recentemente, Backhouse e Backhouse mostraram como construir conexões de Galois para tipos de ordem superior a partir de conexões de Galois para tipos de base e que essas construções podem ser descritas de forma equivalente usando relações lógicas (relações lógicas e conexões de Galois ). Assim, no contexto específico das linguagens funcionais digitadas, as duas noções são equivalentes.

As relações de simulação caracterizam a preservação da propriedade entre as estruturas de Kripke para várias lógicas modais e temporais. Em vez de tipos, temos modalidades em uma lógica. As relações de simulação também definem conexões de Galois e, portanto, abstrações. Pode-se perguntar se essas abstrações têm propriedades especiais. A resposta é que as abstrações padrão são sólidas e as abstrações baseadas em relações de simulação estão completas. A noção de completude diz respeito às conexões de Galois, que podem não coincidir com a interpretação intuitiva. Esta linha de trabalho foi desenvolvida por David Schmidt ( relações binárias de preservação de estrutura para abstração de programa ) e Francesco Ranzato e Francesco Tapparo ( preservação forte generalizada por interpretação abstrata ).

Vijay D
fonte
Sua resposta é muito útil para conectar os conceitos à interpretação abstrata. Obrigado!
Hongjin Liang
Uma pergunta sincera: não sou especialista, mas Reynolds (1983, "Tipos, abstração e polimorfismo paramétrico") já define relações lógicas que são conexões de Galois (Seção 6)? As únicas diferenças que noto: ele não diz o termo "conexão de Galois", mas apenas o equivalente "funcionamentos adjuntos entre ordens parciais consideradas como categorias", e ele se restringe a domínios. OTOH, Backhouse e Backhouse citam Reynolds, mas não discutem essa afirmação, de um jeito ou de outro.
Blaisorblade
6

Eu diria que os dois conceitos são um tanto vagos. Ambos são sobre relações binárias de mecanismos computacionais que de alguma forma incorporam uma noção de igualdade. As relações lógicas são definidas pela indução da estrutura do tipo, enquanto as simulações podem ser definidas da maneira que você desejar, mas o termo alude à coindução.

π

Martin Berger
fonte
Sua referência é muito legal! Eu nunca ouvi relações lógicas para programas concorrentes antes. Obrigado! Eu acho que a dificuldade de definir uma relação lógica é encontrar a estrutura de tipos. Com a mesma estrutura de tipo, uma relação lógica pode ser definida entre diferentes linguagens de programação. Por outro lado, uma simulação requer programas de modelagem por um sistema de transição de estados, o que pode ser desconfortável se os programas forem escritos para diferentes modelos de estados.
Hongjin Liang
Olá! Sim, encontrar uma estrutura de tipos apropriada nem sempre pode ser fácil. Você pode definir simulações usando diferentes sistemas de transição para os dois cálculos que deseja comparar. Alguém poderia argumentar que a definição de simulação fraca faz exatamente isso. Tudo o que você realmente precisa para definir simulações é uma relação para comparar rótulos de transição.
Martin Berger