Demostrando que la recursividad mutua está bien fundada en Lean
Estoy intentando definir la semántica de un lenguaje de programación en Lean. Para hacerlo, tengo un conjunto de tipos mutuamente inductivos que definen los diferentes tipos de términos del lenguaje:
mutual inductive CBlockList, Block, SwitchBody, CExpr, CStatement
with CBlockList : FTContext → set Identifier → set Identifier → Type
....
with Block : FTContext → set Identifier → Type
...
with SwitchBody : FTContext → set Identifier → Type
...
with CExpr : FTContext → set Identifier → ℕ → Type
...
with CStatement : FTContext → set Identifier → set Identifier → Type
...
Tenga en cuenta que, en particular, los diferentes tipos de términos toman como argumentos un contexto de tipo de función y un conjunto de identificadores en alcance. Los términos que pueden introducir nuevas variables en el alcance tienen un segundo argumento de este tipo, que define el conjunto de argumentos después de que se evalúa el término.
Sin embargo, al definir funciones mutuamente recursivas sobre este tipo de datos mutuamente recursivo, Lean se queja de que, para algunas de las llamadas recursivas, no puede inferir la buena fundamentación. Esto ocurre en particular cuando hay llamadas entre funciones con diferentes números de argumentos (debido al diferente número de argumentos de los tipos asociados). Parece que Lean intenta definir el orden bien fundamentado sobre la suma del producto dependiente de los argumentos de cada función, pero cuando tienen un número diferente de argumentos, no le da ningún orden a estos elementos del conjunto, de ahí el problema que he encontrado.
He intentado definir una función de profundidad mutuamente recursiva que atraviese los tipos de datos mutuamente inductivos y devuelva un límite a la posible profundidad de recursión para poder demostrar la buena fundamentación yo mismo, sin embargo, esta definición de función se encuentra con el mismo problema. Parece que estoy atrapado en un callejón sin salida.
¿Cómo podría resolver este problema?
davy.ai
Para resolver el problema de la fundamentación en la recursión sobre tipos mutuamente inductivos con diferentes números de argumentos, un enfoque sería definir explícitamente un orden bien fundamentado sobre la suma del producto dependiente de los argumentos de cada función. Esto se puede hacer utilizando una relación de orden que tenga en cuenta el número de argumentos de cada función.
Otro enfoque sería utilizar una técnica llamada tipos dimensionados, donde se adjunta un parámetro de tamaño a cada tipo y se utiliza para definir un orden bien fundamentado sobre los tipos. Esto permite que el parámetro de tamaño se use para asegurar la fundamentación en las funciones recursivas sobre los tipos.
En cualquier caso, también puede ser necesario demostrar que el orden bien fundamentado es realmente bien fundamentado, lo cual se puede hacer utilizando la inducción y otras técnicas en el lenguaje de demostración de Lean.