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...
É sabido que no Sistema F, você pode codificar produtos binários com o tipo Pode, em seguida, definir projecção funções \ pi_1: A \ B vezes \ a A e \ pi_2: A \ vezes B \ em B .π 1 : A × B → A π 2 : A × B → BUm × B ≜ ∀ ct .( A → B → α ) → αUMA×B≜∀α.(UMA→B→α)→α A \times B \triangleq...
Recentemente, fiquei bastante interessado em parametridade depois de ver o artigo do LICS de Bernardy e Moulin em 2012 ( https://dl.acm.org/citation.cfm?id=2359499 ). Neste artigo, eles internalizam a parametridade unária em um sistema de tipo puro com tipos dependentes e sugerem como você pode...
Existe alguma maneira natural de entender a essência da semântica relacional do polimorfismo paramétrico? Acabei de começar a ler sobre a noção de parametridade relacional, como "Tipos, abstração e polimorfismo paramétrico" de John Reynolds, e estou tendo problemas para entender como a semântica...
Em Teoremas de graça! , Wadler diz que a caracterização da parametricidade pode ser re-expressa em termos de transformações naturais frouxas e isso será objeto de outro artigo. A que papel ele está se referindo? A abordagem categórica da parametericidade que conheço utiliza transformações...
Olhando para os modelos de polimorfismo paramétrico, estou curioso para saber por que são usadas categorias de gráfico reflexivo ? Em particular, por que eles não incluem composição relacional? Ao olhar para os modelos, todos parecem apoiar uma noção natural de composição...
Reynolds propôs originalmente uma semântica relacional para o cálculo lambda polimórfico de segunda ordem [1]. No entanto, mais tarde ele mostrou [2] que essa abordagem era inconsistente com a teoria clássica dos conjuntos. Pitts descreveu a estrutura dos modelos de hiperdocina e modelos topos [3]...
Somos capazes de provar um teorema de parametridade livre sobre funções como f:∀A.[A]⊸[A]f:∀A.[A]⊸[A]f : \forall A . [A] ⊸ [A] ? Supõe-se que fff pega uma lista e sempre retorna uma permutação dela. Outro exemplo: prove que a função f:∀A.(A⊸(A,A))⊸[A]⊸[A]f:∀A.(A⊸(A,A))⊸[A]⊸[A]f : \forall A . (A ⊸...
Eu encontrei este webapp que permite gerar um teorema gratuito para um determinado tipo. Os teoremas gerados quantificam tipos e relações nesses tipos. Esses teoremas (fórmulas) são teoremas de qual teoria / sistema lógico? Como esse sistema se relaciona com a teoria equacional da...