Sé que las operaciones a nivel de bits son tan rápidas en los procesadores modernos, porque pueden operar en 32 o 64 bits en paralelo, por lo que las operaciones a nivel de bits solo requieren un ciclo de reloj. Sin embargo, la adición es una operación compleja que consiste en al menos una y...
He oído hablar de inducción (estructural). Le permite construir estructuras finitas a partir de otras más pequeñas y le ofrece principios de prueba para razonar sobre tales estructuras. La idea es lo suficientemente clara. ¿Pero qué pasa con la coinducción? ¿Como funciona? ¿Cómo se puede decir...
En la página de Wikipedia para Fixed Point Combinators está escrito el texto bastante misterioso. El combinador Y es un ejemplo de lo que hace que el cálculo Lambda sea inconsistente. Por lo tanto, debe considerarse con sospecha. Sin embargo, es seguro considerar el combinador Y cuando se define...
Estoy aprendiendo la prueba de teorema automatizado / solucionadores SMT / asistentes de prueba por mi cuenta y publico una serie de preguntas sobre el proceso, comenzando aquí. Tenga en cuenta que estos temas no se digieren fácilmente sin un fondo en lógicas (matemáticas). Si tiene problemas con...
Estaba tratando de explicarle a alguien que C es Turing completo, y me di cuenta de que en realidad no sé si es, de hecho, técnicamente Turing completo. (C como en la semántica abstracta, no como en una implementación real). La respuesta "obvia" (más o menos: puede abordar una cantidad arbitraria...
Sé cómo codificar factoriales usando tanto iterativo como recursivo (por ejemplo, n * factorial(n-1)por ejemplo). Leí en un libro de texto (sin más explicaciones) que hay una forma aún más eficiente de codificar los factoriales dividiéndolos por la mitad de forma recursiva. Entiendo por qué ese...
He estado investigando las matemáticas detrás de la conversión de cualquier base a cualquier base. Esto se trata más de confirmar mis resultados que de nada. Encontré lo que parece ser mi respuesta en mathforum.org pero todavía no estoy seguro de tener la respuesta correcta. La conversión de una...
Podría haber una disculpa por hacer otra pregunta sobre los requisitos previos, pero estaba confundido acerca de los puntos de partida. Me he encontrado con varios términos como "Lógica modal", "Lógica temporal", "Lógica de primer orden", "Lógica de segundo orden" y "Lógica de orden...
¿Por qué las computadoras usan el sistema de números binarios (0,1)? ¿Por qué no usan el Sistema de números ternarios (0,1,2) o cualquier otro sistema de
Muchos libros de texto cubren los tipos de intersección en el cálculo lambda. Las reglas de tipeo para la intersección se pueden definir de la siguiente manera (además del cálculo lambda simplemente tipado con
Wikipedia, así como otras fuentes que he encontrado, enumeran el voidtipo de C como un tipo de unidad en lugar de un tipo vacío. Esto me parece confuso, ya que me parece que se voidajusta mejor a la definición de un tipo vacío / inferior. No habito valores void, por lo que puedo decir. Una...
El combinador de punto fijo FIX (también conocido como el combinador Y) en el cálculo lambda ( tipo) ( ) se define como:λλ\lambda FIX≜λf.(λx.f (λy.x x y)) (λx.f (λy.x x y))≜λf.(λx.f (λy.x x y)) (λx.f (λy.x x y))\triangleq \lambda f.(\lambda x. f~(\lambda y. x~x~y))~(\lambda x. f~(\lambda y....
Tengo un conjunto de pares. Cada par tiene la forma (x, y) de modo que x, y pertenecen a enteros del rango [0,n). Entonces, si n es 4, entonces tengo los siguientes pares: (0,1) (0,2) (0,3) (1,2) (1,3) (2,3) Ya tengo las parejas. Ahora, tengo que construir una combinación usando n/2pares de...
Sé que el algoritmo de Euclides es el mejor algoritmo para obtener el GCD (gran divisor común) de una lista de enteros positivos. Pero en la práctica, puede codificar este algoritmo de varias maneras. (En mi caso, decidí usar Java, pero C / C ++ puede ser otra opción). Necesito usar el código más...
La mayoría de nosotros conocemos la correspondencia entre la lógica combinatoria y el cálculo lambda . Pero nunca he visto (tal vez no he mirado lo suficientemente profundo) el equivalente de "combinadores mecanografiados", correspondiente al cálculo lambda simplemente mecanografiado. ¿Existe tal...
Me parece que 'implica' en el idioma inglés no significa lo mismo que el operador lógico 'implica', de manera similar a cómo la palabra 'OR' en la mayoría de los casos significa 'OR exclusivo' en nuestro uso cotidiano del idioma. Tomemos dos ejemplos: Si hoy es lunes, mañana es martes. Esto...
La lógica constructivista es un sistema que elimina la Ley del Medio Excluido, así como la Doble Negación, como axiomas. Se describe en Wikipedia aquí y aquí . En particular, el sistema no permite pruebas por contradicción. Me pregunto, ¿alguien está familiarizado con cómo esto afecta los...
Estoy buscando un cálculo simple que admita el razonamiento sobre la reflexión , a saber, la introspección y la manipulación de programas en ejecución. ¿Existe una extensión de cálculo tipo que permita convertir los términos λ en una forma que pueda ser manipulada sintácticamente y luego...
Me gustaría saber si hay una regla para probar esto. Por ejemplo, si uso la ley distributiva solo obtendré .( A ∨ A ) ∧ ( A ∨ ¬ B )(A∨A)∧(A∨¬B)(A \lor A) \land (A \lor \neg
¿Cómo podría expresar una puerta AND usando solo puertas