Que propiedades tiene el calculus of inductive constructions?
El Cálculo de Construcciones Inductivas (CIC), la teoría de tipos en la que se basan Coq/Rocq y, con variantes, Lean, tiene estas propiedades principales:
Propiedades metateóricas - Normalización
fuerte: todo término bien tipado reduce a una forma normal en
un número finito de pasos, y ninguna secuencia de reducción es infinita.
Por eso todas las funciones definibles terminan. Es el motivo de que Coq
exija recursión estructural o bien fundada. - Confluencia
(Church-Rosser): el resultado de reducir no depende del orden
en que se apliquen las reglas, así que la forma normal es única. -
Preservación de tipos (subject reduction): si un
término tiene tipo T, sigue teniéndolo después de reducirse. -
Consistencia lógica: no existe ningún término cerrado
de tipo False, por lo que no se puede demostrar una
contradicción. Es consecuencia de la normalización. -
Decidibilidad del chequeo de tipos: verificar si un
término tiene un tipo dado es un problema decidible. Gracias a esto el
ordenador puede comprobar las demostraciones de forma mecánica.
Propiedades estructurales - Tipos
dependientes: un tipo puede depender de un valor, por ejemplo
“vector de longitud n”. - Correspondencia de
Curry-Howard: las proposiciones son tipos y las demostraciones
son programas. - Tipos inductivos: permite definir
naturales, listas, árboles y predicados, junto con sus principios de
eliminación y recursión. - Jerarquía de universos:
Prop es impredicativo y Type₀ : Type₁ : … es
predicativo. La jerarquía evita paradojas como la de Girard. -
Condición de positividad estricta: los constructores no
pueden mencionar el tipo que se define a la izquierda de una flecha. Sin
esta restricción se perdería la consistencia. - Lógica
constructiva: el tercero excluido no es demostrable, aunque
puede añadirse como axioma sin volver el sistema inconsistente. -
Extracción de programas: a partir de una demostración
se puede obtener código ejecutable, por ejemplo en OCaml o Haskell,
borrando las partes de Prop.
Lo que no tiene de serie: extensionalidad de funciones, irrelevancia de pruebas obligatoria y univalencia. Todas pueden añadirse como axiomas.
¿Quieres que profundice en alguna, por ejemplo por qué la normalización implica la consistencia?
Con que logica se corresponde?
Con la lógica intuicionista de orden superior: una lógica de predicados constructiva en la que se puede cuantificar sobre predicados, funciones y proposiciones, enriquecida con definiciones inductivas.
Por partes:
Π x:A. P x dan el cuantificador universal ∀, y los tipos Σ
dan el existencial ∃.Prop se puede cuantificar sobre las propias
proposiciones, por ejemplo ∀ P : Prop, P → P. Por eso es
más que lógica de primer orden.En el cubo lambda de Barendregt, el Cálculo de Construcciones sin inductivos ocupa el vértice superior (λC) y corresponde a la lógica de predicados intuicionista de orden superior. En la escala de lógicas, la lógica proposicional corresponde al λ-cálculo simplemente tipado, la de segundo orden al Sistema F y la de orden superior a Fω. Al añadir tipos dependientes se llega a la lógica de predicados correspondiente.
En fuerza, CIC es aproximadamente equiparable a una teoría de conjuntos de tipo ZF intuicionista con universos inaccesibles, mucho más fuerte que la aritmética de Peano. Si se le añaden el tercero excluido y el axioma de elección, se acerca mucho a las matemáticas clásicas habituales.
Que quiere decir que es inpredicativo?
Que una proposición puede cuantificar sobre una colección que la contiene a ella misma.
Ejemplo en Coq:
∀ P : Prop, P → PEsta expresión es a su vez una Prop. Al definirla se
cuantifica sobre todas las proposiciones, incluida ella misma.
Esa autorreferencia es justo lo que significa “impredicativo”: se define
algo apelando a una totalidad a la que ese algo pertenece.
Lo contrario, predicativo: en Type,
cuantificar sobre todos los tipos de un nivel te hace subir de
nivel.
∀ A : Type₀, A → A : Type₁El resultado vive en un universo superior, de modo que nunca se habla de una colección que te incluya. Esto es más seguro pero menos expresivo.
Por qué importa: - Ventaja: permite
codificar dentro de Prop los conectivos y definiciones de
forma muy cómoda. Por ejemplo, False := ∀ P, P y la
igualdad de Leibniz x = y := ∀ P, P x → P y. -
Riesgo: la impredicatividad sin control produce
paradojas. La de Russell es un caso, y la de Girard muestra que
Type : Type es inconsistente. Por eso CIC solo la permite
en Prop y mantiene Type estratificado en
niveles. - Precio: para no perder la consistencia, de
una prueba en Prop no se puede extraer información para
construir datos en Type. Esa es la restricción de
eliminación que habrás visto en Coq.
Origen histórico: Poincaré y Russell criticaban las definiciones “círculo vicioso”, y la teoría de tipos ramificada de Russell nació para evitarlas. CIC llega a un compromiso: tolera la impredicatividad, pero solo en el mundo de las proposiciones.
¿Cuáles son los axiomas de la lógica?
Buena pregunta, pero tengo que precisar algo antes: no hay un único conjunto de axiomas de “la lógica”. Depende de qué lógica y de qué presentación uses. Te doy los casos más habituales.
Lógica proposicional clásica (presentación de
Hilbert), tres esquemas de axioma más una regla: -
A → (B → A) -
(A → (B → C)) → ((A → B) → (A → C)) -
(¬B → ¬A) → (A → B) - Regla: modus ponens (de A y
A→B se deduce B)
Con esos tres esquemas y modus ponens se demuestra todo lo demostrable en lógica proposicional clásica.
Lógica intuicionista: la misma, pero el tercer
axioma se sustituye por uno más débil sobre la negación, por ejemplo
A → (¬A → B) (de una contradicción se sigue cualquier
cosa). Lo que se pierde es justamente ¬¬A → A y el tercero
excluido A ∨ ¬A.
Lógica de predicados (primer orden): se añaden los
esquemas para cuantificadores, como - (∀x. A) → A[t/x]
(instanciación) - ∀x.(A → B) → (A → ∀x. B) cuando x no es
libre en A - Regla de generalización.
Una presentación alternativa, la deducción natural, prescinde casi de axiomas y usa en su lugar reglas de introducción y eliminación para cada conectivo (∧, ∨, →, ¬, ∀, ∃). Es la que conecta de forma directa con Curry-Howard y con lo que hablábamos de CIC: esas reglas son los constructores y eliminadores de los tipos.
Un matiz importante: estos axiomas fijan las reglas de inferencia, no verdades sobre el mundo. Son puramente formales.
¿Te interesa alguna lógica concreta, o cómo estos sistemas se relacionan con la teoría de tipos que veníamos tratando?
Después de que me cae de construcciones.
Perdona, no te acabo de captar la frase. ¿Me preguntas qué viene después del cálculo de construcciones, es decir, qué extensiones o sistemas lo suceden?
Si es eso, la línea de evolución es más o menos así:
Type y universos acumulativos, que
es lo que Coq usa en realidad hoy. Deja Prop como único
universo impredicativo.Prop impredicativo con irrelevancia de
pruebas, y axiomas clásicos de serie.¿Era por ahí la pregunta, o te referías a otra cosa con “después”?
fondo con el cálculo de construcciones.
Ah, creo que ahora sí: me preguntas por el fondo, el núcleo o fundamento del cálculo de construcciones. Dime si voy bien encaminado.
El fondo del Cálculo de Construcciones es esta idea unificadora: todo es un término, y los tipos son también términos. No hay una separación entre el nivel de los datos, el de los tipos y el de las proposiciones; todos viven en el mismo lenguaje y se gobiernan con las mismas reglas.
Sobre eso se montan dos pilares:
El producto dependiente Π x:A. B
como única construcción básica. Con él solo se expresan la función
ordinaria, el cuantificador universal, la implicación y el polimorfismo.
Todo lo demás son casos particulares de ese producto.
La impredicatividad en el fondo del sistema: el universo de las proposiciones se cierra sobre sí mismo, lo que permite codificar los conectivos y los datos sin necesitar nada más. Esto era precisamente lo que veíamos antes.
Y debajo de todo está la correspondencia de Curry-Howard llevada al extremo: demostrar y programar son literalmente la misma actividad. Una proposición es un tipo, su demostración es un término de ese tipo, y comprobar la prueba es comprobar que el término tipa.
Dicho en una frase: el fondo del CoC es un lambda-cálculo con tipos dependientes e impredicativo en el que lógica y computación son la misma cosa.
¿Es eso lo que buscabas, o querías que bajara al detalle de las reglas de tipado?
Curry Howard.
Vale, Curry-Howard. Te lo cuento de fondo.
La correspondencia de Curry-Howard es la observación de que la lógica y la computación son la misma estructura vista de dos maneras. Formalmente:
Del cálculo de construcciones.
Entendido: Curry-Howard dentro del cálculo de construcciones en concreto. Ahí la correspondencia se lleva al extremo, porque lógica y programa no son dos cosas análogas sino literalmente la misma.
La traducción es esta:
A → B es a la vez “A implica B” y “el tipo de las funciones
de A en B”.A → B es construir una función que, dada una
prueba de A, devuelve una prueba de B.Lo que aporta el cálculo de construcciones por…
La lógica que axiomas tiene.
Vale, entonces conectando con Curry-Howard: la lógica del cálculo de construcciones casi no tiene axiomas, y eso es lo interesante.
En lugar de axiomas al estilo Hilbert, lo que tiene son reglas de tipado, que por Curry-Howard son exactamente las reglas de deducción natural. Es decir, los “axiomas” de esta lógica son los constructores y eliminadores de cada tipo:
A → B no se axiomatiza:
se da con una regla para construir funciones (la abstracción lambda, que
es la introducción de →) y otra para aplicarlas (modus ponens, que es la
eliminación de →).∀ sale del
producto dependiente, con sus reglas de introducción y eliminación.Así que la respuesta corta: esta lógica no tiene esquemas de axioma propios, sino reglas. Lo único que de verdad hace falta postular aparte son los axiomas opcionales que el sistema no demuestra por sí mismo:
∀P, P ∨ ¬P∀P, ¬¬P → PEsos sí son axiomas en sentido estricto, y los añades solo si quieres recuperar la matemática clásica. Sin ellos, el sistema ya es una lógica completa y consistente por sí misma.
¿Quieres que te enseñe cómo se ve, por ejemplo, la definición inductiva de la conjunción con sus reglas?
Si he de forzar el multiplicador de la. Cpu en throttlestop para que la velocidad suba (sino se queda en 800 Mhz) es debido a un problema de hardware? Tengo un zbook 15u g2
No necesariamente es una avería de la CPU. En los HP, que la CPU se quede clavada a 800 MHz suele deberse a que algo le indica al procesador que frene, casi siempre la señal BD PROCHOT (throttling externo). Las causas típicas, por orden de probabilidad:
Para diagnosticarlo, abre en ThrottleStop la ventana “Limits”: te dice qué está limitando la CPU. Si aparece PROCHOT EXT, el origen es el cargador o la batería. Mientras tanto, desmarcar “BD PROCHOT” en la pantalla principal suele resolverlo sin forzar el multiplicador. Hazlo vigilando las temperaturas, porque desactivas una protección.
Así que puede ser hardware, pero de un componente barato de sustituir (cargador o batería), no de la placa ni de la CPU.
Software windows alarma temperatura
Las mejores opciones gratuitas:
Para tu caso, sobre todo si desactivas BD PROCHOT en ThrottleStop, te recomiendo HWiNFO, con una alerta en torno a 90–95 °C. La CPU de tu ZBook se protege sola cerca de 105 °C.