Em um tópico recente na lista de discussão da Agda, surgiu a questão das leis , na qual Peter Hancock fez comentários instigantes .
Meu entendimento é que leis vêm com tipos negativos, ie. conectivos cujas regras de introdução são invertíveis. Para desabilitar para funções, Hank sugere o uso de um eliminador personalizado, com divisão de diversão , em vez da regra usual do aplicativo. Eu gostaria de entender a observação de Hank em termos de polaridades.
Por exemplo, há duas apresentações -types. Existe o eliminador de divisão tradicional Martin-Löf , em um estilo positivo:
E há a versão negativa:
Esta última apresentação facilita a obtenção de para pares, ie. para qualquer par (onde == representa a igualdade de definição). Em termos de provabilidade, essa diferença não importa: intuicionisticamente, você pode implementar projeções com divisão ou o contrário.( π 0 p , π 1 p ) = = p p
Agora, os tipos são geralmente (e sem controvérsia, acredito) tomados negativamente:
O que nos fornece para funções: .λ x . f x = = f
No entanto, nesse e-mail, Hank lembra do eliminador de divisões simples (Programação na teoria do tipo ML, [http://www.cse.chalmers.se/research/group/logic/book/], p.56). É descrito na estrutura lógica por:
Curiosamente, Nordstrom et al. motive esta definição dizendo que "[esta] forma não canônica alternativa se baseia no princípio da indução estrutural". Há um forte cheiro de positividade nessa declaração: as funções seriam 'definidas' pelo construtor .
No entanto, não consigo definir uma apresentação satisfatória dessa regra na dedução natural (ou, melhor ainda, no cálculo sequencial). O (ab) uso da estrutura lógica para introduzir parece crucial aqui.
Então, é divertida uma apresentação positiva do tipo ? Também temos algo semelhante no cálculo sequencial (não dependente)? Como seria?
Quão comum / curioso é isso para os teóricos da prova em campo?
fonte
Aqui está uma perspectiva um pouco diferente da resposta de Fredrik. Geralmente, as codificações impredicativas dos tipos da Igreja satisfarão as leis relevantes , mas não as leis .ηβ η
Portanto, isso significa que podemos definir um par dependente da seguinte maneira:
No entanto, a segunda projeção é realizável e, em um modelo paramétrico, você pode mostrar que também possui o comportamento correto. (Veja meu rascunho recente com Derek Dreyer sobre parametridade no Cálculo de construções para mais informações.) Então, acho que a projeção exige fundamentalmente algumas propriedades de extensionalidade fortes para que faça sentido.π2
Em termos de cálculo sequencial, o eliminador fraco possui uma regra que se parece um pouco com:
fonte
Richard Garner escreveu um bom artigo sobre application vs funsplit, Sobre a força dos produtos dependentes na teoria dos tipos de Martin-Löf (APAL 160 (2009)), que também discute a natureza de ordem superior da regra do funsplit (com uma referência a Uma extensão natural da dedução natural de Peter Schroeder-Heister (JSL 49 (1984))).
Richard mostra que, na presença de tipos de identidade (e regras de formação e introdução para os tipos ), o funsplit é interderível com a regra de aplicação acima + eta proposicional, ou seja, as duas regras a seguir:Π
Ou seja, se você tiver uma divisão simples, poderá definir application e como acima, para que válido. Mais interessante, se você tiver aplicação e as regras eta proposicionais, poderá definir divisão simples.η ( Π -Prop- η-Comp )
Além disso, o funsplit é estritamente mais forte que a aplicação: as regras eta proposicionais não são definíveis em uma teoria com apenas aplicação - portanto, o funsplit não é definível, pois as regras eta proposicionais também seriam. Intuitivamente, isso ocorre porque as regras do aplicativo oferecem um pouco mais de folga: diferentemente do funsplit (e eta), eles não informam o que são funções, apenas que podem ser aplicadas aos argumentos. Acredito que o argumento de Richard também possa ser repetido para os tipos , para mostrar o mesmo resultado paraΣ s p l i t projeções vs.
Observe que se você tivesse regras eta definicionais, certamente as teria proposicionalmente também (com ). Portanto, acho que suas afirmações "[...] que nos dão para funções" e "[...] esta última apresentação facilitam a obtenção de para pares" estão erradas. A Agda, no entanto, implementa para funções e pares (se for definido como um registro), mas isso não ocorre apenas no aplicativo.η( m ) : = r e fl (m) η η η Σ
fonte