Suscríbete a RCast en iTunes | Google Play | Grapadora
Greg Meredith se une a Isaac DeFrain y Christian Williams para discutir las etapas finales antes del lanzamiento de Mainnet.
Aquí están los documentos discutidos en este RCast:
Greg: Christian, acabas de mencionar la conexión entre las especies y las teorías de tipo lineal, lo cual es muy interesante porque Mike y yo hemos estado trabajando en este lado de la teoría de la prueba de LADL. Ayer me di cuenta, mientras lo escribíamos, que esencialmente lo que está sucediendo con este uso de un catalizador habilitante es factorizar la parte lineal. Resulta que puede componer esta restricción de recursos para la ejecución junto con cualquier sistema de reescritura. Como resultado, estás forzando un tipo de linealidad en esta situación.
Es un tipo de composición. Visto desde el otro lado, estás factorizando el material lineal en su propio subcomponente. Así es como terminamos obteniendo un aspecto lineal de las teorías de tipos que estamos generando. No se me había ocurrido hasta ayer que se puede pensar de esa manera. Eso termina siendo una buena manera de descifrar la argumentación sobre cómo y por qué funciona esto.
Hoy quería hablar un poco, no sobre el lado de la teoría de la prueba, sino sobre la justicia en lugar de la vida. Si realmente va y hace una revisión de la literatura sobre equidad, especialmente en los últimos 15 años, así es como pasé mi último fin de semana, ha habido algo de desarrollo, pero la equidad es una consideración interesante y generalmente se trata de manera algo diferente a las limitaciones de la vida. que uno puede considerar
En particular, siempre he sido sensible a las restricciones de equidad, después de haber construido un montón de sistemas de actores. Carl Hewitt solía bromear mucho diciendo que los actores eran estrictamente más poderosos que las máquinas de Turing porque la demanda era que la capa de comunicación fuera justa. Las exigencias de equidad como esa son estrictamente más poderosas de lo que realmente puede calcular dentro de un sistema Turing. Solía hacer ese tipo de comentarios solo para golpear a las personas en las costillas y despertarlas. Fue un comentario humorístico porque despertaría muchas cejas.
Pero en el caso de los sistemas de actores, la justicia es fácil de describir. La equidad en un sistema de actores se reduce al siguiente tipo de consideración. Donde los actores calculan enviándose mensajes entre ellos y se almacenan entre sí mediante un buzón. El buzón representa efectivamente una cola de mensajes. Frente a esta cola de mensajes se encuentra lo que se llama un serializador primitivo que serializa el orden no determinista de los mensajes en algún tipo de programación. Hay restricciones en ese horario para que sea justo.
La caracterización se puede describir en términos de un trío de actores. Supongamos que tiene un actor que desempeña el rol de servidor y que presta servicios a otros dos clientes. Están enviando mensajes al servidor. Un cliente es muy detallado y el otro cliente es conciso. No puede tener un prefijo infinito en el buzón de los mensajes detallados del cliente. Tiene que haber algunos de los concisos espolvoreados en alguna muestra finita. ¿Tiene sentido?
Isaac: Con los clientes detallados y concisos, ¿estás diciendo que tienen mensajes más largos o más cortos o que están enviando más o menos mensajes?
Greg: Más. Se trata del volumen de los mensajes en comparación con el tamaño de los mensajes.
cristiano: ¿Cómo sería un prefijo si los estás construyendo en binario uno a otro?
Greg: Debido a que el serializador primitivo siempre puede ser injusto, siempre favorece al cliente detallado sobre el cliente conciso. Cada vez que tiene la opción de ordenarlos, siempre pone el otro, porque siguen entrando: "Oh, aquí hay otro del tipo detallado. Pon eso delante del otro. Oh, aquí hay otro del tipo detallado. Pongamos ese frente ". Así es como termina siendo injusto.
Isaac: ¿Estás diciendo que independientemente del orden en que se reciben los mensajes?
Greg: En el sentido de que siempre y cuando sigan llegando. El serializador primitivo está dando una vista ordenada al actor del servidor.
Isaac: Eso tiene sentido. La equidad, usted dice, es solo una noción bien definida de alternancia entre todos los mensajes posibles de clientes que están llegando.
Greg: Así lo ven los actores. Si examina la literatura, una de las cosas que es realmente interesante es que mucha de la literatura quiere verla como una propiedad del sistema completo, lo que hace que sea mucho más difícil de verificar, mucho más difícil de aplicar en términos de código local. Si nos fijamos en las bisimulaciones, Thomas Hildebrandt, que trabajó en bigraphs, caracteriza la bisimulación conservadora de la historia, que es decidible para los sistemas de estado finito, y la bisimulación hereditaria preservadora de la historia, las cuales le proporcionan información suficiente para tomar algunas decisiones sobre equidad o para describir propiedades de equidad. La bisimulación hereditaria que preserva la historia no es decidible incluso para sistemas de estado finito.
Cuando comienza a tomar esta vista de sistemas completos, en lugar de mirar las cosas de una manera más local, puede perder rápidamente la capacidad de hacer que estas cosas sean decididas. Eso es realmente importante.
Hay otra pieza del rompecabezas. Shri Rajamani analizó la equidad en el contexto de CTL y CTL *. La perspectiva es sistemas completos. Lo que estaban viendo era reducir el conjunto total de modelos a los más justos y luego demostrar que lo que era cierto en CTL o CTL * era cierto en el subconjunto justo. Podrías continuar haciendo tu razonamiento y factor de equidad a un lado, lo cual es una vez más, la mayor evidencia del tipo de perspectiva que quería presentar para su consideración, que es que la equidad generalmente se considera por separado de otras restricciones de vida.
En particular, si solo consideramos el punto muerto como una especie de consideración típica de la vida, puede tener sistemas injustos que eviten el punto muerto. Siempre hay algún controlador Uber que está repartiendo el trabajo y lo garantizan. De hecho, la razón por la que se les pone en esta posición de ser los controladores de Uber porque no garantizan ningún punto muerto. Es en vivo, pero no es justo.
Isaac: Es como un jugador con veto en la teoría de juegos.
Greg: Eso es exactamente correcto. Por otro lado, puedes tener cosas que son justas pero no vivas. Todo el mundo recibe una sacudida justa, pero se atascan. Esa es una manera de ver que la equidad es un poco diferente a algunas de estas otras consideraciones de vida.
cristiano: Todavía no estoy seguro de entender la justicia. Tiene algo que ver con la alternancia o la proporcionalidad de la capacidad de enviar. ¿Pero luego dijiste que podías formularlo en términos de bisimulación?
Greg: Eso es correcto. La bisimulación se puede ver como gobernando quién ve qué mensajes. Puede hablar sobre la adición de restricciones de equidad en ese tipo de entorno. ¿Tiene sentido?
Isaac: Estás diciendo que solo te aseguras de que suficientes personas estén viendo los mensajes, o supongo que no estoy realmente seguro de cómo conectar esos dos …
Greg: Siempre puede ver el sistema agregado total de todos los agentes que están computando. Entonces puedes ver todas las transiciones de ese sistema. Entonces puedes comparar eso con un sistema en el que los actores son justos. La forma en que haría esa comparación es la bisimulación. Cada transición en una se corresponde con una transición en la otra. Así es como se relacionan los dos.
Lo que notamos, que es lo que hacemos con el cálculo de Pi y el cálculo de Rho, si reconoce o respeta la distinción entre productor y consumidor, puede caracterizar el tipo de restricciones de vida que estábamos viendo antes de una manera diferente a Usted caracteriza las restricciones de equidad. En particular, las restricciones de sincronización que hemos implementado están en el lado de la producción. Un validador solo puede producir mensajes si cumple con ciertas consideraciones con respecto a haber escuchado a los otros actores en el sistema, los otros validadores, que forzarán absolutamente un tipo de característica de vida en la red. De hecho, hay una gran cantidad de características de vida diferentes que puede obtener imponiendo gramáticas ponderadas en los árboles de especificación de los bloques que se proponen.
Pero también puedes hacerlo por el lado del consumo. No solo del lado de la producción de mensajes, sino también del lado del consumo. Hay una línea de investigación interesante que me ha llamado la atención desde hace mucho tiempo, realizada por Oleg Kiselyov. Él y un par de sus colaboradores de toda la vida proporcionaron un transformador de mónada, al que llaman LogicT. Esencialmente, proporciona combinaciones justas de flujos. Piense en una corriente como efectivamente una mónada. Cuando desee agregar secuencias juntas, una posibilidad, como con una lista, es agregar un anexo. Pero si en el caso de una secuencia en la que tiene una lista infinita, si agrega y lo hace en el orden incorrecto, por ejemplo, si agrega todas las probabilidades a la lista uno, dos, tres, está su gadget de prefijo infinito.
cristiano: ¿Entonces cremallera?
Greg: Puedes poner cremallera o puedes hacer otro tipo de cosas. Lo que hizo fue proporcionar un dispositivo de uso general al que llama LogicT, que implementa el seguimiento. Si lo piensa, ahora desea agregar a través de un montón de flujos, no solo dos. Entonces desea agregar de acuerdo a ciertas restricciones.
Otra aplicación de este tipo de maquinaria es la comprensión en el cálculo Rho, donde cada puerto que está escuchando puede verse como una secuencia, pero tiene restricciones de coincidencia de patrones. Solo desea realizar un evento si coincide con el patrón. De lo contrario, desea omitirlo, que es similar al pico. Si hace esto en varias secuencias, es posible que desee ver todas las combinaciones hasta que encuentre la que coincida con todas las restricciones del patrón. Eso se convierte obviamente en un problema de retroceso en el caso general. LogicT proporciona eso.
Le he sugerido al equipo de desarrollo, esa es la API abstracta. Cree una vista de cada uno de los validadores como si estuvieran proporcionando una secuencia de mensajes. Puede ver los bloques que entran y puede ordenarlos por firma del productor. Eso proporciona una señal lógica. Luego agrega las señales lógicas utilizando este método de agregación de tarifas.
La versión más baja de esto es, como dijiste, Christian, cremallera, que es round robin. Esa es la forma más barata de hacerlo, pero puedes ser más elegante. Oleg proporciona una disyunción justa en una conjunción justa. Ahora tiene un pequeño lenguaje que le permite hacer políticas: desunir estas corrientes y unir estas corrientes y luego desunir estas corrientes y así sucesivamente. Puede agregar un árbol completo de estas secuencias usando este pequeño lenguaje. ¿Tiene sentido?
Isaac: Todo esto es un esfuerzo para que los mensajes de nadie tengan prioridad sobre los de los demás. Básicamente, la aplicación de la descentralización.
Greg: Sí, pero no es que los mensajes de nadie tengan prioridad sobre los de nadie más. Es que tiene un lenguaje de política prioritario. Eso es realmente lo que proporciona el transformador de mónada LogicT.
cristiano: ¿Cuál es la diferencia entre disyunción y conjunción?
Greg: Estamos hablando de una disyunción justa, por lo que es una unión justa porque las transmisiones son como conjuntos. La disyunción es como una unión justa. La conjunción es como una intersección justa.
cristiano: ¿Qué significa eso para las transmisiones?
Greg: La respuesta más simple es que puedes hacer un intercalado; puedes hacer un round robin; pero puedes hacer cosas más complicadas. La unión es un entrelazado.
Isaac: El aspecto de la equidad está llegando porque hay un orden implícito allí.
Greg: Porque hay un pedido y porque algunos de ellos pueden divergir. Supongamos que tiene una lista que tiene un huevo de Pascua en alguna parte. Si el cálculo no tiene que tocar el huevo de Pascua, no explotará. Dependiendo de cómo realice el intercalado o de cómo combine estas dos listas, ya sea que proporcione ambas cosas o proporcione algo de ambas cosas, que coincida con un criterio, esa es la parte de intersección, cómo lo hace desde cada flujo importará si una de las corrientes puede contener un huevo de Pascua.
cristiano: ¿Qué quieres decir con un huevo de Pascua?
Greg: Tocas la cosa y entra en un cálculo divergente. Ese es el otro aspecto de esto. No es solo que las corrientes puedan ser infinitas, sino que también pueden contener huevos de Pascua. Pueden contener cálculos divergentes. La forma típica de lidiar con no tocar los cálculos de desvío es que eres lo más vago posible. Lo que pasa con LogicT es que le permite dar esta mezcla de pereza y entusiasmo. Eso es lo bueno de esto.
Isaac: ¿Estás diciendo que el validador básicamente podría jugar según sus propias reglas y, en cierta medida, dentro del marco de esta restricción de equidad?
Greg: Esa es la idea. Como con todo, ese es precisamente el punto. Usted aclaró esto. Lo que he estado discutiendo es que todo lo relacionado con las restricciones de sincronización era proporcionar un lenguaje en el que expresar las restricciones para que no estuviéramos atrapados.
Estoy sugiriendo lo mismo en el lado de la equidad. No fije esto en una solución única para todos. Proporcione un lenguaje: ahí es donde encaja LogicT. Lo bueno es que LogicT tiene una caracterización clara y nítida en términos de semántica teórica de categoría. Sin embargo, lo interesante de LogicT es que es un transformador de mónada y no una ley distributiva.
Isaac: ¿Qué quieres decir con transformador de mónada? Creo que entiendo heurísticamente, pero no estoy seguro de cuál es la definición real.
Greg: Sin entrar en muchos detalles, el transformador de mónada es otra forma de combinar mónadas y garantizar que el resultado sea una mónada. En general, cuando combina mónadas, el resultado no es necesariamente una mónada. Si tienes una ley distributiva, es una mónada. Eso es fácil de probar. El transformador de mónada es otra forma.
Lo que he argumentado en el pasado es que la ley distributiva es muy superior en muchos casos. He tratado de usar LADL como ejemplo de un lugar donde realmente lo necesitas debido a su caracterización ecológica que hace que el razonamiento sea mucho más fácil. De hecho, las ecuaciones son precisamente lo que lo saca de la dificultad de hacer la suma de dos teorías. En el caso de LADL, está tratando de llegar a esta semántica, que es la recopilación de los términos. Tienes estos términos de combos de colección en la combinación de las teorías. No puede salir a menos que tenga una ley distributiva.
cristiano: ¿Por qué no podemos usar el mismo idioma para las restricciones de sincronización que para este problema?
Greg: Esto es lo que estaba tratando de hacer en la parte superior de la conversación: observar cómo la literatura tiene en cuenta la justicia. La equidad generalmente se considera separada. El argumento es que podemos tener sistemas vivos pero no justos. Dimos algunos bocetos de cómo son esos. Tenemos sistemas que son justos pero no vivos. Dimos algunos ejemplos de esos.
cristiano: ¿Por qué eso significa que no pueden tener el mismo idioma?
Greg: La siguiente pieza fue hablar sobre eso en términos de la vista de implementación del sistema. Las restricciones de la vida son sobre la producción de mensajes y las restricciones de equidad son sobre el consumo de mensajes. El lado de la producción no tiene que preocuparse por los huevos de Pascua, por lo general, o entrelazar cosas, mientras que el lado del consumo tiene que preocuparse exactamente por esas cosas. El lenguaje tiene que tener primitivas diferentes, esencialmente. Pero están estrechamente relacionados.
Este es todo el enfoque de RChain. Básicamente es un enfoque basado en el lenguaje. Al final del día, soy un friki del lenguaje. Creo fundamentalmente que los problemas informáticos más interesantes se reducen a la construcción de un pequeño mini lenguaje en el que expresar una variedad de soluciones.
Isaac: ¿Es posible que la equidad y los idiomas vivos de los que estamos hablando sean duales en algún aspecto?
Greg: Son duales, al menos en la forma en que hemos descompuesto el sistema. Si nos fijamos en la literatura, esa dualidad no es explícita. Eso se debe a que se caracterizan como estas propiedades de todo el sistema.
Isaac: Estás diciendo desde la perspectiva del actor, son dos idiomas.
Greg: De hecho, no solo los actores, sino los agentes en el cálculo Pi, los agentes en el cálculo Rho, todos esos modelos computacionales que respetan la dualidad entre entrada y salida, en realidad están representados explícitamente.
Isaac: Derecha. Supongo que necesitas eso en el nivel del suelo antes de que puedas hablar de dualidad.
Greg: Exactamente Hay otros tipos de dualidad, como los duales Morgan y cosas así. El material de bisimulación generalmente se realiza sobre árboles de sincronización completos en lugar de mirarlo en términos de entrada y salida.
Por lo que puedo decir, esta es una perspectiva única. Todavía tengo que encontrar un artículo o algo en la literatura que analice cosas como esta. Sin embargo, es fácilmente comprensible. No creo que haya nada aquí que sea ciencia espacial. Hemos podido cubrir la mayoría de los conceptos en un corto período de tiempo.
Lo que es realmente hermoso es que hay estos dispositivos listos para usar que podemos sacar del estante. Esa es una de las cosas que he estado tratando de seguir tanto como sea posible. En el caso del cálculo Rho, comencemos con los mejores modelos, veamos dónde hay huecos, arregle esos huecos y luego obtenga un modelo de cálculo que podamos reducir y practicar a partir de ahí.
Lo mismo con LADL. Estoy mucho más interesado en la semántica que se basa en cosas que conocemos y tratamos de ser súper conservadores. Mike y yo pasamos mucho tiempo, por ejemplo, en lugar de hacer todo lo posible para tratar de evitar arrastrar todo TOPOSIS. ¿Podemos construir el lenguaje de comprensión que solo usa la maquinaria monádica? Pero finalmente descubres que hay ciertos teoremas de no ir con respecto a las leyes distributivas y, por lo tanto, te ves obligado a tener más y más dispositivos similares. Eso es lo que justifica el uso de TOPOSIS. La metodología de diseño, la ética de trabajo, es no inventar nada si no es necesario.
cristiano: ¿Qué entendemos por idiomas duales?
Greg: De lo que hablaba es de la dualidad entre producción y consumo.
cristiano: ¿Crees que esto podría ser algún tipo de dualidad matemática real?
Greg: Efectivamente, es covariante versus contravariante. Es solo una covariante iterada porque estás hablando de flujos o contravariante iterada.
Isaac: Esto es algo que se combinará con la restricción de vida que ya existe.
Greg: Eso es exactamente correcto. En realidad, estamos trabajando en la emisión de boletos en este momento para agregar la versión más simple de este gadget. Si fuera yo, pondría el LogicT como API y luego, debajo de él, en lugar de hacer un seguimiento completo, haría algo simple que cumpla con las restricciones de la ecuación. Dadas las limitaciones de tiempo, podemos incurrir en un poco de deuda técnica y simplemente hacer lo más simple y luego agregar la API post facto, después del mantenimiento. Es un problema de restricción de recursos en lugar de arquitectónicamente lo que está sucediendo. Sabemos arquitectónicamente y teóricamente qué está pasando y ahora estamos poniendo la mejor implementación que hará el trabajo. Con suerte, podemos proporcionar una mejor factorización después del hecho. Nuevamente, las matemáticas ganan.
Isaac: ¿No es así siempre? La restricción de la vida se estableció inicialmente debido a los largos tiempos de propuesta, ¿verdad?
Greg: Para ser claros, Casper no está activo a menos que agregue algún tipo de restricción de sincronización. Sabíamos que íbamos a tener que hacer eso.
Isaac: Esto es solo la manifestación de eso.
Greg: Los tiempos de propuesta largos se muestran como una manifestación. Si aumenta la restricción de sincronización hasta 11, los tiempos de la propuesta se mantienen estables. Tenemos los datos sobre eso.
Isaac: Con eso te refieres a la restricción síncrona 0,99.
Greg: Exactamente La restricción de sincronización es solo una de una gran cantidad de ellas. Hay todo un lenguaje de restricciones de sincronización. Simplemente elegimos el que podemos implementar como un dial y tan rápido de verificar. Cuando lo arrancas por completo, eso limita el rendimiento de la red.
Isaac: Básicamente obliga a un round robin, o algo parecido a un round robin.
Greg: Es una especie de round-robin-ish.
cristiano: ¿Qué significa eso?
Greg: No es necesariamente que vaya del validador uno para validar o dos para validar tres. Eso es un round robin. Podría tener un validador funcionando nuevamente. Podrías tener algo de tartamudeo en esto siempre que tengan suficiente interés en sus justificaciones. Son permutaciones en el orden admitido. Solo tienes que visitarlos todos.
Básicamente, lo que obtendrá es cualquier permutación de todo N y luego otra permutación de todo N y luego otra permutación de todo N, así. Entonces no es un round robin. El round-robin será uno, dos, tres, cuatro cinco, hasta N, y luego, uno, dos, tres, cuatro, cinco hasta N. Nunca verás una permutación.
cristiano: Eso parece lo más justo para que sea una secuencia de permutaciones: eficientemente al azar.
Greg: Esto en realidad va a los algoritmos de corte de torta. Es más justo en abstracto. Cuando comienzas a cortar un pastel, alguien dice: "No me gusta tanta guinda. ¿Puedes darme la pieza de la esquina? ”. Ese tipo de consideraciones prácticas, se mapean en cosas como,“ Bueno, este tipo tiene más memoria. Este chico tiene más ancho de banda. Esta chica tiene más poder de cómputo ”. Exactamente la misma ranura no es realmente justa si asimilas todo. Es justo en abstracto, pero puedes hacerlo mejor. En particular, desea poder tener algo de margen de maniobra en el sistema.
Derek: Tuvimos un breve bloqueo del sistema aquí. Retomando a Greg otra vez …
Greg: Christian preguntaba sobre papeles y recursos. Te enviaré algunos enlaces, Derek, para agregar a las notas. Lo único que dije, para beneficio de los oyentes, es que después del trabajo de Oleg había un grupo de personas implementadas en N Queens y otros problemas clásicos de retroceso de esta manera, y luego dije: "Oye, no funciona así como también una solución optimizada de retroceso ".
Cuando leí el documento, mi mente inmediatamente se dirigió a: "Oh, esta es una excelente manera de agregar flujos", no "esta es una excelente manera de implementar el retroceso". Esto no debe verse como una forma de estructurar el retroceso, o al menos no lo haría. Lo estaba haciendo como una forma de secuencias bastante compuestas. Tener procedencia y recursos son realmente importantes para el lado de investigación de esto.
