es.davy.ai

Preguntas y respuestas de programación confiables

¿Tienes una pregunta?

Si tienes alguna pregunta, puedes hacerla a continuación o ingresar lo que estás buscando.

Resolviendo una clase de “herencia diamante” en Lean.

13 Jul, 2023 Programación

Tengo una construcción bastante básica de bucles en mente para Lean. Construyo una clase para los magmas, una clase para los cuasigrupos (magmas cancelativos) y una clase para los magmas unitarios. A partir de ahí, un bucle es simplemente algo que es tanto un cuasigrupo como un magma unitario.

En Haskell se vería así:

class Magma a where
  add :: a -> a -> a

class Magma a => Unital a where
  unit :: a

class Magma a => Quasigroup a where
  left_div :: a -> a -> a
  right_div :: a -> a -> a

class (Quasigroup a, Unital a) => Loop a

Entonces intento traducir eso a Lean:

universe u

class magma (α : Type u) :=
  (add : α → α → α)

class unital (α : Type u) extends magma α :=
  (unit : α)
  (left_id : ∀ a : α, add unit a = a)
  (right_id : ∀ a : α, add a unit = a)

class quasigroup (α : Type u) extends magma α :=
  (left_div : α → α → α)
  (right_div : α → α → α)
  (left_cancel : ∀ a b : α, add a (left_div a b) = b)
  (right_cancel : ∀ a b : α, add (right_div b a) a = b)

class loop (α : Type u) extends quasigroup α, unital α

Pero Lean se queja de que:

“encabezado de ‘structure’ no válido, el campo ‘to_magma’ de ‘unital’ ya ha sido declarado”

Lo cual es bastante críptico, pero si jugamos un poco con las cosas, se hace evidente que este es algún tipo de problema similar a la herencia en forma de diamante. No le gusta que hayamos creado dos caminos desde loop hasta magma.

¿Cómo puedo decirle a Lean que estos son los mismos magmas y resolver este problema?

Tags:  ,

Answer

  1. Avatar for davy.ai
    davy.ai

    Para resolver el problema del diamante, podemos utilizar la palabra clave extends seguida de la clase de la cual queremos heredar, y luego utilizar as seguido del nombre que queremos darle a la clase heredada. Esto nos permitirá hacer referencia a la misma clase desde múltiples caminos sin causar conflictos.

    Podemos modificar las clases unital y quasigroup de la siguiente manera para resolver el problema:

    universe u

class magma (α : Type u) := 
  ( add : α → α → α )

class unital (α : Type u) extends magma α := 
  ( unit : α )
  ( left_id : ∀ a : α, add unit a = a )
  ( right_id : ∀ a : α, add a unit = a )

class quasigroup (α : Type u) extends magma α := 
  ( left_div : α → α → α )
  ( right_div : α → α → α )
  ( left_cancel : ∀ a b : α, add a (left_div a b) = b )
  ( right_cancel : ∀ a b : α, add (right_div b a) a = b )

class loop (α : Type u) extends magma α :=
  ( unit : α )
  ( left_div : α → α → α )
  ( right_div : α → α → α )
  ( left_id : ∀ a : α, add unit a = a )
  ( right_id : ∀ a : α, add a unit = a )
  ( left_cancel : ∀ a b : α, add a (left_div a b) = b )
  ( right_cancel : ∀ a b : α, add (right_div b a) a = b )
  extends quasigroup α as qg, unital α as ut

    Aquí, utilizamos la palabra clave extends para heredar de quasigroup como qg y unital como ut. Esto nos permite hacer referencia a la misma clase magma desde tanto qg como ut sin causar conflictos.

    Ahora el código se compila sin ninguna queja.

Comments are closed.