Pelo que entendi, na ciência da computação, os tipos de dados não são baseados na teoria dos conjuntos por causa de coisas como o paradoxo de Russell, mas como nas linguagens de programação do mundo real, não podemos expressar tipos de dados tão complexos como "conjunto que não se contém", podemos diga que, na prática, o tipo é um conjunto infinito de seus membros, em que a associação à instância é definida pelo número de recursos intrínsecos a esse tipo / conjunto (existência de determinadas propriedades, métodos)? Se não, qual seria o contra-exemplo?
11
Respostas:
A principal razão para evitar conjuntos na semântica de tipos é que uma linguagem de programação típica nos permite definir funções recursivas arbitrárias. Portanto, seja qual for o significado de um tipo, ele deve ter a propriedade de ponto fixo. O único conjunto com essa propriedade é o conjunto de singleton.
Para ser mais preciso, um valor definido recursivamente do tipo (onde tipicamente é um tipo de função) é definido por uma equação de ponto fixo onde pode seja qualquer programa. Se for interpretado como o conjunto , esperamos que todo tenha um ponto fixo. Mas o único conjunto com essa propriedade é o singleton.τ τ v = Φ ( v ) Φ : τ → τ τ T f : T → T Tv τ τ v = Φ ( v ) Φ : τ→ τ τ T f: T→ T T
Claro, você também pode perceber que o culpado é a lógica clássica. Se você trabalha com a teoria dos conjuntos intuicionista, é consistente assumir que existem muitos conjuntos com propriedade de ponto fixo. De fato, isso foi usado para fornecer semântica da linguagem de programação, veja, por exemplo,
fonte
A subtipagem semântica é baseada em uma interpretação teórica dos tipos subjacentes, em que a subtipagem é um subconjunto. O trabalho original , acredito, é de Castagna no contexto da linguagem de processamento XML CDuce. Os tipos correspondem a conjuntos de documentos XML. As idéias foram reaplicadas ao cálculo e a objetos e classes de cálculo .π
fonte
Com algumas exceções (uma que Dave Clarke cita), é difícil usar semântica simples de tipos de teoria dos conjuntos. A razão é que a abstração de dados não funciona muito bem com a semântica da teoria dos conjuntos.
fonte