Tau y la crisis de verdad - De qué trata TauChain en profundidad - Actualización del progreso del proyecto

Esta es una traducción al castellano de un artículo publicado el 10 Septiembre de 2016 en el blog de Tauchain por Ohad Asor

---

Vivimos en un mundo en el cual nadie conoce la ley. Excepto en casos triviales, tu no puedes conocer que es legal y que no, todo lo que puedes hacer es intentar preguntar al juez o al policía sus opiniones después de cometer las acciones, las cuales por supuesto diferirán de uno a otro. O puedes consultar a un abogado quien te dirá que no hay respuestas absolutas, y al final del día hay muchas probabilidades de que desafortunadamente no conozcas como calcularla. Puedes hacer lo mejor para llevar una vida productiva y seguir las reglas como tu las entiendes o como los abogados te guíen, pero nadie puede garantizar que no seas considerado un criminal, o que las acciones legales no se vuelvan contra ti. Igualmente, uno puede vivir una vida dañando a mucha gente y ningún sistema legal lo detendrá, incluso si el sistema está al corriente de las acciones que lleva a cabo. Tal situación tan pesimista no es nueva ni es local, y para mi gusto quien mejor la describió fue Franz Kafka.

Jugando con palabras y tomándolas en la dirección deseada, conscientemente o no, con buenas o malas intenciones, es como la humanidad ha aprendido siempre a hablar. La peor mentira contiene sólo verdades, así los peores crímenes son autorizados, y los argumentos pueden ser tomados para justificar casi cualquier cosa. Esta "crisis de verdad" es la fundación de la corriente postmoderna en filosofía, notablemente la aproximación Deconstructivista, la cual demuestra que los textos pueden ser interpretados de muchas (contradictorias) formas. "No hay una verdad" es la base del postmodernismo. Pero ¿podemos al menos tener una isla de verdad en la cual los contratos sociales puedan ser útiles y tener sentido?

No sólo las leyes no pueden ser entendidas en una única forma, si no que ni siquiera trivialmente pueden ser realizadas mediante un proceso determinado. Las leyes tienen que ser cambiadas con el tiempo y por lo tanto necesitamos leyes para cambiar las leyes. Pero entonces necesitaremos leyes que cambien las leyes hechas para cambiar las leyes, hasta el infinito. Por lo tanto nosotros permanecemos sin base lógica para los procesos de hacer leyes, no sólo con la crisis de decidir qué es legal y qué es ilegal. Esta paradoja fue descrita en el libro disponible online "La paradoja de la autoenmendación (o autocorreción)" de Peter Suber. La solución de Suber es resumida en el apéndice del libro que describe el juego Nomic. El ofrece un sistema de dos niveles en el cual nosotros tenemos reglas mutables e inmutables, incluyendo reglas que transformen una regla (es decir, que hagan inmutable una regla mutable o viceversa). Este camino puede eludir la infinita jerarquía de esquemas de enmienda, pero todavía permanecemos con la crisis de verdad en la cual no hay verdad, especialmente cuando desesperadamente la necesitas, a pesar de muchas propuestas de leyes para un cierto orden social.

Cuando volvemos atrás al mundo de la legalidad e intentamos 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 hacerse más fácil. Las lógicas han completado aquellas ideas por siglos y surgieron con la noción de Decidibilidad. Un lenguaje es decidible si todas las declaraciones expresables en este lenguaje pueden ser decididas siempre que sigan las reglas expresadas en ese lenguaje lo mejor posible. Un sorprendente ejemplo podría ser el teorema de Godel: si tu lenguaje está capacitado para expresar la aritmética de Peano, es decir, si contiene los números naturales 1, 2, 3... equipado con la suma y la multiplicacion y sus reglas (que en efecto las determinan singularmente), entonces siempre habrá algunas declaraciones sobre la aritmética de Peano que no podrán ser probadas desde las definiciones. Serán requeridos infinitamente tantos axiomas en el orden de ser capaces de decidir la incorrección de cada declaración. Un ejemplo de decibilidad podría ser la aritmética de Presburger: si nosotros sacrificamos la multiplicación y definimos números con sumas solamente (de una determinada manera), entonces volvemos atrás a la decibilidad y todas las declaraciones expresables podrían ser decididas en un proceso finito ya sean verdaderas o falsas. Lo mismo se aplica a los 2000 años de antigüedad de geometría Euclídea, la cual es en efecto una teoría decidible.

Por lo tanto, estaríamos interesados en crear un proceso social en el cual expresamos leyes en un lenguaje únicamente decidible, una forma colaborativa enmendable de contratos sociales sin bucear en paradojas. Eso es de lo que trata Tau-Chain.

Esta larga introducción viene a subrayar la importancia y el rol central de la decibilidad generalmente en la vida y específicamente en Tau. Si nosotros queremos que algo como Tau aporte una contribución real al mundo, debemos usar un lenguaje decidible. El objetivo del diseño inicial de Tau era responder a estos requerimientos, pero recientemente he hallado que yo estaba equivocado, el lenguaje elegido inicialmente es simplemente indecidible. La teoría intuicionista de Martin-Lof (MLTT) sólo es decidible en determinados aspectos (específicamente, igualdad). Pero no en el caso de todo lo expresable es decidible. Esta situación me ha llevado a la conclusión de que la MLTT es una opción equivocada, y otra solución lógica debe ser considerada. En efecto algunas declaraciones mías en vídeos fueron erróneas, la MLTT no tiene una verificación de caracteres decidible en general.

La MLTT va sobre los llamados "tipos dependientes", de la cual intentaré dar una pequeña muestra en este párrafo. Nosotros tenemos "condiciones" (terms) y "tipos" (types). Podemos tomar las condiciones como declaraciones y los tipos como especificaciones que requieren que aquellas declaraciones cumplan. ¿Cómo pueden ser en general las especificaciones? Los tipos dependientes vienen a dar a las especificaciones máxima expresividad en cierto sentido: los tipos pueden depender de las condiciones y las condiciones pueden depender de los tipos (y aquí es de donde viene el nombre "tipos dependientes"). Estamos capacitados para expresar cualquier especificación que nuestro lenguaje de condiciones está capacitado para expresar, o más exactamente, los tipos pueden ser fijados por un programa que los calcule, que puede depender de otras partes del código. Los programas pueden incluir especificaciones y las especificaciones pueden incluir programas. La "verificación de caracteres" (typecheck) es el proceso de asegurar que las condiciones en efecto conocen sus tipos. Pero si los tipos pueden ser programas genéricos, los requerimos para ser ejecutados y que devuelvan un resultado en un tiempo finito. Para ello tendremos que asegurarnos que nuestros programas se interrumpan, así que hemos alcanzado el Problema de la parada. Sólo si tu puedes afirmar que tus tipos son calculados en un proceso finito, entonces el mismo proceso de chequeo de tipos se vuelve decidible. Pero esta tarea es indecidible por sí misma ya que el problema de la parada es indecidible. Así que si tu quieres alcanzar decibilidad sobre los tipos dependientes, primero tendrás que superar una indecidible barrera de parada. Esto es posible en muchos casos como muchos programas que están capacitados para ser escritos en una forma que probablemente termina (por ejemplo, recursión primitiva, la cual es la base de la programación funcional total), pero esto es inherentemente imposible que surja con semejante método para todos los programas, en ese caso el problema de la parada se volvería decidible.

Los lenguajes de tipos dependientes son extensamente usados en el mundo de las pruebas de ayuda con ordenador y en verificación formal, pero tienen la reputación de ser duro trabajar con ellos. La dureza se deriva no sólo de que su teoría sea significativamente más complicada que en otros lenguajes, si no que la parte más dura es convencer al verificador de caracteres (o la terminación y el verificador total que intenta asegurarse que el proceso de verificación es en efecto finito) de que tu código conoce sus especificaciones. Por lo tanto, el proceso de verificación de caracteres no es automático y requiere una cantidad significativa de intervención humana sólo para convencerlo a aceptar declaraciones verdaderas, una dificultad que se deriva exactamente de la indecibilidad del lenguaje. Subsecuentemente, hemos perdido la habilidad de, siempre, de forma completamente automática, determinar si una sentencia es verdadera, o equivalentemente, si una acción (declaración) es legal (bien escrita) o ilegal de acuerdo a las reglas dadas.

El remedio para esta situación es escoger una lógica diferente, una "completa". Una lógica completa significa que todo es decidible, y no sólo en ciertos aspectos (como igualdad en MLTT). Godel mostró que toda lógica que es completa y es posible explicarla en la aritmética de Peano, será inevitablemente inconsistente, así que en el orden de disfrutar tanto la consistencia como la completitud, vamos a tener que sacrificar una parte de la aritmética. No sólo ya hay conocidas las completas y consistentes lógicas que nosotros podemos usar, si no que muy recientemente algunas familias de lenguajes han sido descubiertas para ser mucho más expresivas que las conocidas previamente. Específicamente, determinadas clases de Lógicas Monádicas de Segundo Orden (MSO o MSOL por sus siglas en inglés) fueron halladas para ser completas y consistentes desde los años 60, pero ellas no obtuvieron habilidades expresivas satisfactorias. No fue hasta 2006 que Luke Ong irrumpió con una prueba completa de MSOL, llamada "Escenas de recursión de alto orden", la cual es un lenguaje de orden funcional más elevado de mecanografiado simple con recursión, que mejora dramáticamente la expresividad de los lenguajes decidibles ya conocidos. Hasta entonces los avances tanto en teoría como en prácticas fueron hechos mayoritariamente por Naoki Kobayashi.

Fue un largo camino hasta que averigüé que mis premisas básicas estaban equivocadas y en efecto no fui lógico cuando el viajé comenzó. Afortunadamente nosotros podemos ahora modificar el diseño de Tau en algo que es incluso mejor de lo que habíamos pensado anteriormente, incluso si la MLTT fuera decidible. Mencionar 3 ventajas: la existencia de un modelo computacional directo, la habilidad de inferir programas y la simplicidad de uso.

Las teorías de MSO tienen un modelo computacional directo en condiciones de autómatas. Es posible traducir las fórmulas de MSO en máquinas redundantes que lean declaraciones y decidan si conocen la fórmula. Es más, aquellos autómatas pueden ser minimizados en una única manera, así obtener incluso un probable código óptimo. Por otra parte, MLTT no provee una traducción directa a autómatas sino 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 libremente especificado en declaraciones computacionales y no existe una directa traducción a los autómatas. No es posible que exista mientras los autómatas sean una decisión de procedimiento finito, mientras los tipos dependientes, no sean completamente decidibles.

La segunda ventaja notable es la programación automática, más comunmente llamada "síntesis de programas" en la literatura. ¿Si tomamos una especificación de un programa (o regla básica), la máquina puede calcular el programa (o reglas) por sí misma? Esta tarea es indecidible en MLTT, pero en una lógica completa es en efecto posible. Podemos tener programas y contratos correctos-por-construcción, meramente indicando que es lo que esperamos que hagan, y comandando a la máquina a buscar tal estructura que admita nuestros requerimientos.

La lógica MSO es más simple de usar por las razones mencionadas anteriormente: es un lenguaje simple y no requiere intervención humana para convencer que una declaración verdadera es, en efecto, verdadera. También representa una lógica más intuitiva: MLTT es una lógica intuicionista por la cual una declaración que ha sido probada que es falsa no necesariamente implica que su contraste es verdadera. Por ejemplo, uno no siempre puede usar una prueba por contradicción. La lógica intuicionista permite probar la no existencia por contradicción: puede ser asumido que algo exista, derivar una contradicción, y por ello concluir que no existe. Pero no puede soportar una prueba por contradicción de no existencia: asumiendo que algo no existe y derivando una contradicción no probamos que eso exista bajo la lógica intuicionista. Más formalmente, la lógica intuicionista niega explícitamente el principio del tercero excluido. Y esto es por supuesto altamente contraintuitivo, y permita la posibilidad de errores humanos especialmente sobre estructuras complicadas. Por otra parte MSO es una lógica clásica, lo que significa que incluye el principio del tercero excluido: es simplemente imposible para nada ser verdadero y falso al mismo tiempo. El excluido es completamente excluido, mientras nosotros añadimos esta regla a la MLTT, pierde su consistencia.

Como conclusión, nuestro viaje ha resultado ser diferente a lo que esperábamos desde el aspecto de la implementación, pero terminará con un producto mejor que nos dará una oportunidad para resolver la crisis de verdad y la paradoja de la autocorrección en un contexto social global y electrónico. Yo personalmente intento (y prometí) continuar trabajando a tiempo completo hasta cumplir Tau y Agoras, que introducirá mucha de las características descritas aquí. Recientemente di una descripción resumida filmada de los productos que estoy cometido a desarrollar. Otro artículo y otro vídeo están en camino para explicar más detalles. Si estás dispuesto a ayudar a conseguir estos objetivos y logras por ti mismo (o tu amigo) entender los papeles de Kobayashi, estaré muy contento por tu cooperación.