Se dice que el CoC es la culminación de las tres dimensiones del Cubo Lambda. Esto no es aparente para mí en absoluto. Creo que entiendo las dimensiones individuales, y la combinación de cualquiera de los dos parece resultar en una unión relativamente sencilla (¿tal vez me falta algo?). Pero cuando...
Coq, Agda e Idris tienen una jerarquía de tipos infinita (Tipo 1: Tipo 2: Tipo 3: ...). Pero, ¿por qué no hacerlo como λC, el sistema en el cubo lambda que está más cerca del cálculo de las construcciones, que tiene solo dos tipos, ∗∗* y , y estas reglas?◽◽◽ ∅ ⊢∗:◽∅⊢∗:◽\frac {} {∅ ⊢ * : ◽} Γ ⊢...
Para sistemas sin tipos dependientes, como el sistema de tipos Hindley-Milner, los tipos corresponden a fórmulas de lógica intuicionista. Allí sabemos que sus modelos son álgebras de Heyting y, en particular, para refutar una fórmula, podemos restringir a un álgebra de Heyting donde cada fórmula...
¿Es la teoría de tipo Martin-Löf básicamente el cálculo predicativo de construcciones inductivas sin impredicative ?PropProp\mathtt{Prop} Si están estrechamente relacionados pero con más diferencias que solo , ¿cuáles son esas
Soy consciente de que el cálculo de construcciones se está normalizando fuertemente, lo que significa que cada expresión tiene una normalidad que no puede ser beta, eta-reducida aún más. De hecho, esta es la expresión más eficiente que calcula el mismo valor que la expresión original. Pero en...
En el papel clásico de cálculo de construcciones hay una regla que establece (página 7 del pdf, página 101 del documento original) Esta regla significaría que cualquier contexto es reducible a un miembro de ese contexto. Parece que esto no debería ser correcto, ya que implicaría 1 ≅ Nat 3 ≅...
Quiero saber si la capacidad de decisión de igualdad de dos pruebas decidibles de la misma proposición puede demostrarse sin ningún axioma adicional en el cálculo de construcciones inductivas. Específicamente, quiero saber si esto es cierto sin ningún axioma adicional en Coq. ∀ P: Prop , P∨ ¬ P⇒...