Resumen

Queremos formalizar el álgebra de Kleene concurrente usando el asistente de pruebas Isabelle, y mostrar que los shuffle languages son modelos de esa álgebra.

Bibliografía y librerías

• En este artículo se define el álgebra.

• La teoría Regular Sets ya tiene la concatenación de lenguajes, y varios lemas super útiles.

• Ya hay semianillos y reticulados completos en la librería estándar.

• La teoría List ya tiene definida la operación de mezcla (es esta, shuffles).

• Acá está eso mismo definido, pero en 'matemática normal no Isabelle'.

• Ya hay librerías de quantales y álgebras de Kleene en el proof archive. Además, ya hay concurrent kleene algebra, que está definida en una parte de la entrada de communicating concurrent Kleene algebras.

Observaciones 'ahorratiempo'

• Las mezclas de ab y cd son {abcd, acbd, acdb cabd, cdab, cadb}.

• El 1 de la interpretación con shuffle languages es {ε}.

• Es importante el requisito de que leq sea el orden de un reticulado completo porque los lenguages regulares pueden ser infinitos.

• El artículo de Hoare es super claro con las definiciones, y están todas bien ordenaditas en dos partes: el apéndice A, y la sección que los define. Después la parte de los modelos es mucho más 'pesada', y no incluye definiciones relevantes para los shuffle languages.

• Lo único que parece que todavía no hay en el proof archive es definiciones que relacionen a las álgebras de Kleene concurrentes y los shuffle languages.

• El paper no pone una ecuación para "composition distributes over arbitrary suprema", así que no estoy seguro de haber elegido una interpretación correcta (elegí una parecida a la que usa Struth en su módulo de quantales).

Puntos dudosos y/o flojos

• Puse que el supremo era la menor cota superior como hipótesis/assumption del un locale en vez de importar e instanciar la clase complete_lattice.

• Puse la operación de supremado y el órden parcial inducido de un semianillo idempotente como argumentos de sus locales, que está bastante feo.

Puntos flojos corregidos

• Ahora los semianillos y las operaciones con lenguajes salen todas de módulos estándar importados debidamente.

• Arreglé las irregularidades con la notación que usaba para 'parchar' la ambiguedad de las expresiones.

• Ahora el supremo es un supremo de verdad.