IDNI Blog

  • Tau y la crisis de la verdad

    Ohad Asor Publicado el 10 de septiembre de 2016, a las 11:25

    Vivimos en un mundo en el que nadie conoce la ley. Excepto casos triviales, no se puede saber qué es legal y qué no, todo lo que se puede hacer es probar y ver cuál es la opinión del juez o del policía después de haber tomado tus acciones, dichas opiniones por supuesto difieren la una de la otra. O, puede consultar a un abogado que le dirá que no hay respuestas absolutas y, a fin de cuentas, es una cuestión de probabilidad que desafortunadamente nadie sabe cómo calcular. Puede hacer su mejor esfuerzo para tener una vida productiva y seguir las reglas tal como las entiende o como lo guían los abogados, pero nadie puede garantizar que no será considerado un delincuente, o que no se tomarán acciones legales en su contra. Del mismo modo, uno puede vivir una vida haciendo daño a muchas personas y ningún sistema legal lo detendrá, incluso si el sistema es consciente de las medidas adoptadas. Tal situación pesimista no es nueva y no es local, y para mi gusto fue mejor descrita por Franz Kafka.

    El jugar con las palabras y llevarlas a cualquier contexto deseado, conscientemente o no, con buenas o malas intenciones, siempre estuvo ahí desde que la humanidad aprendió a hablar. Las peores mentiras solo contienen verdades y los peores crímenes tienen licencia, además se pueden presentar argumentos para justificar casi cualquier cosa. Esta "crisis de la verdad" es la base de la corriente postmoderna de la filosofía, especialmente el enfoque deconstructivista que demuestra cómo los textos pueden interpretarse de muchas maneras (contradictorias). "No hay una sola verdad" es la base del postmodernismo. Pero, ¿podemos al menos tener algún terreno de verdad en la que los contratos sociales pueden ser útiles y tener sentido?

    No solo las leyes no se pueden entender de una manera absoluta, sino que ni siquiera se pueden hacer trivialmente mediante un proceso absoluto. Las leyes tienen que cambiarse con el tiempo y, por lo tanto, también necesitamos leyes para cambiar las leyes. Pero luego necesitaremos leyes para cambiar las leyes, para cambiar las leyes, ad infinitum. Por lo tanto, permanecemos sin ninguna base lógica para el proceso de reglamentación, no solo la crisis de decidir qué es legal y qué es ilegal. Esta paradoja fue descrita en el libro disponible en línea La paradoja de la auto enmienda de Peter Suber. La solución de Suber se resume en el apéndice de ese libro que describe el juego Nomic. Él ofrece un sistema de dos niveles en el que tenemos reglas mutables e inmutables, incluidas las reglas de transmutación de una regla (es decir, hacer que la regla inmutable sea mutable o viceversa). De esta manera uno puede evitar la jerarquía infinita de esquemas de enmienda, pero aún permanecemos con la "crisis de la verdad" en la que no hay una sola verdad, especialmente cuando la necesitamos desesperadamente, y a pesar del propósito mismo de las leyes para tener un cierto orden social en vez de desinformación y caos.

    Al retroceder desde el mundo de las legalidades y tratar de responder preguntas similares en el mundo de los números y los objetos matemáticos, la tarea no se vuelve fácil, pero podría decirse que es más fácil. Los lógicos han contemplado esas ideas durante siglos y se les ocurrió la noción de decibilidad. Un lenguaje es decidible si cada declaración expresable en un lenguaje puede decidirse si sigue las reglas expresadas en ese lenguaje. Un ejemplo asombroso sería el teorema de Godel: si nuestro lenguaje es capaz de expresar la aritmética de Peano, es decir, contiene los números naturales 1,2,3, ... equipados con suma y multiplicación y sus reglas (que de hecho los determinan de manera única), entonces siempre habrá algunas afirmaciones verdaderas sobre la aritmética de Peano que no pueden probarse a partir de las definiciones. Por ende, se necesitan infinitos axiomas para poder decidir la corrección de cada enunciado. Un ejemplo de decidibilidad sería la aritmética de Presburger: si abandonamos la multiplicación y definimos los números solo con suma (de cierta manera), volvemos a la decidibilidad y cada afirmación podría decidirse en un proceso finito como verdadera o falsa. Lo mismo se aplica a la geometría Euclides de 2000 años de antigüedad, que es una teoría decidible.

    Por lo tanto, estamos interesados en crear un proceso social en el que expresemos las leyes solo en un lenguaje decidible y colaborativamente formemos contratos sociales modificables sin caer en paradojas. De esto se trata Tau-Chain.

    Esta larga introducción sirve para enfatizar la importancia y el papel central de la decidibilidad en general en la vida y específicamente en Tau. Si queremos que Tau haga una contribución real al mundo, debe usar un lenguaje decidible. El diseño inicial de Tau pretendía responder a esos requisitos, pero recientemente descubrí que estaba equivocado, y el lenguaje elegido inicialmente es simplemente indecidible. La teoría de tipos Martin-Lof (MLTT) tiene solo ciertos aspectos decidibles (específicamente, la igualdad). Pero no es el caso que todo lo expresable sea decidible. Esta situación me llevó a la conclusión de que MLTT era una elección incorrecta, y, por tanto, era necesario considerar otra lógica. De hecho, algunas declaraciones mías en algunos blogposts y videos fueron erróneas, ya que MLTT no tiene una comprobación de tipo decidible.

    MLTT trata de los llamados "tipos dependientes", de los que trataré de dar una pequeña muestra en este párrafo. Tenemos "términos" y "tipos". Puede ver términos como declaraciones y tipos como especificaciones que esas declaraciones deben cumplir. ¿Cómo de general pueden ser las especificaciones? Los tipos dependientes vienen a darles máxima expresividad en cierto sentido: los tipos pueden depender de los términos, y los términos pueden depender de los tipos (y de ahí viene el nombre "tipos dependientes"). Podemos expresar cualquier especificación que nuestro lenguaje de términos pueda expresar, o más exactamente, los tipos pueden ser establecidos por un programa que los calcule, que pueden depender de otras partes del código. Los programas pueden incluir especificaciones y las especificaciones pueden incluir programas. Typecheck es el proceso de asegurarse de que los términos cumplan con sus tipos. Pero si los tipos pueden ser programas genéricos, tenemos que exigir que se ejecuten y devuelvan un resultado en un tiempo finito. Para eso tendremos que asegurarnos de que nuestros programas se detengan, por lo que hemos alcanzado el problema de la parada. Solo si puede afirmar que sus tipos se calculan en un proceso finito, entonces el proceso mismo del comprobador se vuelve decidible. Pero esta tarea es indecidible por sí misma ya que el problema de la parada es indecidible. Entonces, si quieres llegar a la decidibilidad sobre los tipos dependientes, primero hay que pasar una barrera indecidible de la parada. Esto es posible en muchos casos, ya que muchos programas pueden escribirse en una forma que probablemente termine (por ejemplo, la recursión primitiva que es la base de la programación funcional total), pero es inherentemente imposible encontrar un método para todos los programas, de lo contrario, el problema de la parada sería decidible.

    Los lenguajes de tipo dependiente se usan ampliamente en el mundo de las pruebas asistidas por computadora y la verificación formal, pero tienen la reputación de ser difíciles de trabajar. La dificultad proviene no solo de que su teoría es significativamente más complicada que la de otros lenguajes, sino que la parte más difícil es convencer al contador de tipos (o comprobador de terminación y totalidad intenta asegurar que el proceso de verificación de tipo sea finito) de que su código cumpla con sus especificaciones. Por lo tanto, el proceso de verificación de tipo no es automático y requiere una cantidad significativa de intervención humana solo para convencerlo de que acepte declaraciones verdaderas, una dificultad que surge exactamente de la indecidibilidad del lenguaje. Posteriormente perdemos la capacidad de determinar siempre y de forma totalmente automática si una oración es verdadera, o equivalentemente, si alguna acción (término) es legal (bien tipado) o ilegal de acuerdo con las reglas dadas.

    El remedio para esta situación es escoger una lógica diferente, una lógica "completa". Una lógica completa significa que todo es decidible, y no solo ciertos aspectos de la misma (como la igualdad en MLTT). Godel demostró que cada lógica que se completa y es capaz de expresar la aritmética de Peano inevitablemente será inconsistente, por lo que para disfrutar de consistencia y completitud tendremos que renunciar a una parte de la aritmética. No solo se conocen lógicas completas y consistentes que podemos usar, sino que recientemente se descubrió que estas familias de idiomas son mucho más expresivas de lo que se sabía anteriormente. Específicamente, ciertas clases de Lógica de Segundo Orden de Monadic (MSO o MSOL) fueron completas y constantes desde la década de 1960, pero no tenían habilidades expresivas satisfactorias. No fue sino hasta 2006 que Luke Ong presentó una prueba de integridad de MSOL sobre los llamados "Esquemas de recursión de orden superior", que es un lenguaje funcional de orden superior de tipo simple (más bien dependiente) con recursión, que mejoró drásticamente la expresividad de lenguajes conocidos como completamente decidibles. Desde entonces, se hicieron avances tanto en la teoría como en la práctica, especialmente por Naoki Kobayashi.

    Fue un largo viaje hasta que descubrí que mis premisas básicas estaban equivocadas y, de hecho, no era un lógico (persona que se dedica al estudio de la lógica) cuando comencé el viaje. Afortunadamente ahora podemos modificar el diseño de Tau en algo que es incluso mejor de lo que pensábamos antes, incluso si MLTT fuese decidible. Mencionar tres ventajas: la existencia de un modelo computacional directo, la capacidad de inferir programas y la simplicidad de uso.

    Las teorías de MSO tienen un modelo computacional directo en términos de autómatas. Las fórmulas de MSO se pueden traducir en máquinas redundantes que leen una declaración y deciden si cumple con la fórmula. Además, esos autómatas se pueden minimizar de una manera única, por lo que obtenemos un código potencialmente óptimo. Por otro lado, MLTT no disfruta de una traducción directa a autómatas, sino que más bien la conexión lógica-autómata admite un concepto más general de programas como pruebas, donde el proceso de prueba se deja más vagamente especificado en términos computacionales y una traducción directa a autómatas no existe. No puede existir, ya que los autómatas son un procedimiento explícito de decisión finita, mientras que los tipos dependientes no son completamente decidibles.

    La segunda ventaja notable es la programación automática, más comúnmente llamada "síntesis de programa" en la literatura. Si damos una especificación de un programa (o base de reglas), ¿puede la máquina calcular el programa (o las reglas) por sí misma? Esta tarea es indecidible en MLTT, pero en una lógica completa es posible. Podemos tener programas y contratos correctos por construcción, simplemente indicando lo que esperamos que hagan, y ordenando a la máquina que encuentre una estructura que admita nuestros requisitos.

    La lógica MSO es más fácil de usar por las razones mencionadas anteriormente: es un lenguaje más simple, y no requiere intervención humana para convencer que una declaración verdadera es verdadera. También representa una lógica más intuitiva: MLTT es una lógica intuicionista que significa que una afirmación que resultó ser falsa no implica necesariamente que su contraste sea verdadero. Por ejemplo, uno no siempre puede usar una prueba por contradicción. La lógica intuitiva permite probar la inexistencia por contradicción: puede suponerse que algo existe, derivar una contradicción y, por lo tanto, concluir que no existe. Pero no puede sustentar una demostración por contradicción de la no existencia: asumir que algo no existe y derivar una contradicción no prueba que exista, bajo lógica intuicionista. Más formalmente, la lógica intuicionista niega explícitamente la ley del tercero excluido. Y esto, por supuesto, es muy poco intuitivo y permite la posibilidad de errores humanos, especialmente en estructuras complicadas. Por otro lado, MSO es una lógica clásica, significa que incluye la ley del tercero excluido: es simplemente imposible que cualquier cosa sea verdadera y falsa al mismo tiempo. El tercero está completamente excluido, mientras que, si agregamos esta regla a MLTT, pierde su consistencia.

    Como conclusión, nuestro viaje resultó ser diferente de lo que esperábamos desde el aspecto de la implementación, pero terminará con un mejor producto que nos dará la oportunidad de resolver la crisis de la verdad y la paradoja de la auto-enmienda en un contexto global, social y electrónico. Personalmente tengo la intención (y prometí) de seguir trabajando a tiempo completo hasta cumplir con Tau y Agoras que introducirán muchas más características de las que se describen aquí. Recientemente grabé una descripción condensada de los productos que me he comprometido a entregar. Otro artículo y otro video están en camino para explicar más detalles. Si está dispuesto a ayudar a lograr estos objetivos y se encuentra a usted mismo (o a su amigo) comprendiendo los documentos de Kobayashi, estaré encantado de cooperar.