RA2016: Funciones recursivas generales en Isabelle/HOL

En la segunda parte de la clase de hoy del curso de Razonamiento automático se ha estudiado cómo definir en Isabelle/HOL funciones recursivas que no son primitiva recursiva y cómo demostrar propiedades de dichas funciones. Como ejemplo, se ha usado la función de Ackerman.

La teoría con las soluciones de los ejercicios es la siguiente

chapter {* Tema 4: Razonamiento por casos y por inducción *}

theory T4b
imports Main 
begin

section {* Recursión general. La función de Ackermann *}

text {* 
  El objetivo de esta sección es mostrar el uso de las definiciones
  recursivas generales y sus esquemas de inducción. Como ejemplo se usa la
  función de Ackermann (se puede consultar información sobre dicha función en
  http://en.wikipedia.org/wiki/Ackermann_function).

  Definición.  La función de Ackermann se define por
    A(m,n) = n+1,             si m=0,
             A(m-1,1),        si m>0 y n=0,
             A(m-1,A(m,n-1)), si m>0 y n>0
  para todo los números naturales. 

  La función de Ackermann es recursiva, pero no es primitiva recursiva. 
*}

fun ack :: "nat ⇒ nat ⇒ nat" where
  "ack 0       n       = n+1" 
| "ack (Suc m) 0       = ack m 1" 
| "ack (Suc m) (Suc n) = ack m (ack (Suc m) n)"

-- "Ejemplo de evaluación"
value "ack 2 3" (* devuelve 9 *)

text {*
  Esquema de inducción correspondiente a una función:
  · Al definir una función recursiva general se genera una regla de
    inducción. En la definición anterior, la regla generada es
    ack.induct: 
       ⟦⋀n. P 0 n; 
        ⋀m. P m 1 ⟹ P (Suc m) 0;
        ⋀m n. ⟦P (Suc m) n; P m (ack (Suc m) n)⟧ ⟹ P (Suc m) (Suc n)⟧
       ⟹ P a b
*}

text {*
  Ejemplo de demostración por la inducción correspondiente a una función:
  Demostrar que para todos m y n, A(m,n) > n.
*} 

-- "La demostración detallada es"
lemma "ack m n > n"
proof (induct m n rule: ack.induct)
  fix n
  show "ack 0 n > n" by simp
next
  fix m 
  assume "ack m 1 > 1"
  then show "ack (Suc m) 0 > 0" by simp
next  
  fix m n
  assume "n < ack (Suc m) n" and 
         "ack (Suc m) n < ack m (ack (Suc m) n)"
  then show "Suc n < ack (Suc m) (Suc n)" by simp
qed

text {*
  Comentarios sobre la demostración anterior:
  · (induct m n rule: ack.induct) indica que el método de demostración
    es el esquema de recursión correspondiente a la definición de 
    (ack m n).
  · Se generan 3 casos:
    1. ⋀n. n < ack 0 n
    2. ⋀m. 1 < ack m 1 ⟹ 0 < ack (Suc m) 0
    3. ⋀m n. ⟦n < ack (Suc m) n; 
              ack (Suc m) n < ack m (ack (Suc m) n)⟧
             ⟹ Suc n < ack (Suc m) (Suc n)
*}

-- "La demostración automática es"
lemma "ack m n > n"
by (induct m n rule: ack.induct) auto

end

chapter {* Tema 4: Razonamiento por casos y por inducción *}

theory T4b

imports Main

begin

section {* Recursión general. La función de Ackermann *}

text {*

El objetivo de esta sección es mostrar el uso de las definiciones

recursivas generales y sus esquemas de inducción. Como ejemplo se usa la

función de Ackermann (se puede consultar información sobre dicha función en

http://en.wikipedia.org/wiki/Ackermann_function).

Definición. La función de Ackermann se define por

A(m,n) = n+1, si m=0,

A(m-1,1), si m>0 y n=0,

A(m-1,A(m,n-1)), si m>0 y n>0

para todo los números naturales.

La función de Ackermann es recursiva, pero no es primitiva recursiva.

fun ack :: "nat ⇒ nat ⇒ nat" where

"ack 0 n = n+1"

| "ack (Suc m) 0 = ack m 1"

| "ack (Suc m) (Suc n) = ack m (ack (Suc m) n)"

-- "Ejemplo de evaluación"

value "ack 2 3" (* devuelve 9 *)

text {*

Esquema de inducción correspondiente a una función:

· Al definir una función recursiva general se genera una regla de

inducción. En la definición anterior, la regla generada es

ack.induct:

⟦⋀n. P 0 n;

⋀m. P m 1 ⟹ P (Suc m) 0;

⋀m n. ⟦P (Suc m) n; P m (ack (Suc m) n)⟧ ⟹ P (Suc m) (Suc n)⟧

⟹ P a b

text {*

Ejemplo de demostración por la inducción correspondiente a una función:

Demostrar que para todos m y n, A(m,n) > n.

-- "La demostración detallada es"

lemma "ack m n > n"

proof (induct m n rule: ack.induct)

fix n

show "ack 0 n > n" by simp

fix m

assume "ack m 1 > 1"

then show "ack (Suc m) 0 > 0" by simp

fix m n

assume "n < ack (Suc m) n" and

"ack (Suc m) n < ack m (ack (Suc m) n)"

then show "Suc n < ack (Suc m) (Suc n)" by simp

qed

text {*

Comentarios sobre la demostración anterior:

· (induct m n rule: ack.induct) indica que el método de demostración

es el esquema de recursión correspondiente a la definición de

(ack m n).

· Se generan 3 casos:

1. ⋀n. n < ack 0 n

2. ⋀m. 1 < ack m 1 ⟹ 0 < ack (Suc m) 0

3. ⋀m n. ⟦n < ack (Suc m) n;

ack (Suc m) n < ack m (ack (Suc m) n)⟧

⟹ Suc n < ack (Suc m) (Suc n)

-- "La demostración automática es"

lemma "ack m n > n"

by (induct m n rule: ack.induct) auto

end

Se puede imprimir o compartir con