Loading [MathJax]/jax/output/HTML-CSS/jax.js
Saltar al contenido principal
Library homepage
 

Text Color

Text Size

 

Margin Size

 

Font Type

Enable Dyslexic Font
LibreTexts Español

B.5: Inducción estructural

( \newcommand{\kernel}{\mathrm{null}\,}\)

Template:MathJaxZach

Hasta el momento hemos utilizado la inducción para establecer resultados sobre todos los números naturales. Pero un principio correspondiente se puede usar directamente para probar resultados sobre todos los elementos de un conjunto definido inductivamente. Esto a menudo se llama inducción estructural, porque depende de la estructura de los objetos definidos inductivamente.

Generalmente, una definición inductiva viene dada por (a) una lista de elementos “iniciales” del conjunto y (b) una lista de operaciones que producen nuevos elementos del conjunto a partir de los antiguos. En el caso de términos agradables, por ejemplo, los objetos iniciales son las letras. Solo tenemos una operación: las operaciones son Inclusoo(s1,s2)=[s1s2] puedes pensar en los\Nat propios números naturales como dados por una definición inductiva: el objeto inicial es0, y la operación es la función sucesorax+1.

Para probar algo sobre todos los elementos de un conjunto definido inductivamente, es decir, que cada elemento del conjunto tiene una propiedadP, debemos:

  1. Demostrar que los objetos iniciales tienenP

  2. Demostrar que para cada operacióno, si los argumentos tienenP, también lo hace el resultado.

Por ejemplo, para probar algo sobre todos los términos agradables, demostraríamos que es cierto sobre todas las letras, y que es cierto sobre[s1s2] siempre que sea ciertos1 es2 individualmente.

ProposiciónB.5.1

El número de[ es igual al número de] en cualquier término agradablet.

Prueba. Utilizamos inducción estructural. Los términos agradables se definen inductivamente, con letras como objetos iniciales y las operacioneso para construir nuevos términos agradables a partir de los antiguos.

  1. El reclamo es cierto para cada letra, ya que el número de[ en una letra por sí mismo es0 y el número de] en ella también lo es0.

  2. Supongamos que el número de[ ins1 es igual al número de], y lo mismo es cierto paras2. El número de[ ino(s1,s2), es decir[s1s2], in, es la suma del número de[ ins1 ys2. El número de] ino(s1,s2) es la suma del número de] ins1 ys2. Así, el número de[ ino(s1,s2) es igual al número de] ino(s1,s2).

ProblemaB.5.1

Demostrar por inducción estructural que ningún término agradable comienza con].

Demos otra prueba por inducción estructural: un segmento inicial apropiado de una cadenat de símbolos es cualquier cadenas que concuerde cont símbolo por símbolo, leído desde la izquierda, pero quet sea más largo. Entonces, e.g.,[a es un segmento inicial apropiado de[ab], pero tampoco lo son[b (no están de acuerdo en el segundo símbolo) ni[ab] (tienen la misma longitud).

ProposiciónB.5.2

Cada segmento inicial adecuado de un buen términot tiene más que[]'s.

Prueba. Por inducción ent:

  1. tes una letra por sí misma: Entonces not tiene segmentos iniciales adecuados.

  2. t=[s1s2]por algunos buenos términoss1 ys2. Sir es un segmento inicial adecuado det, hay una serie de posibilidades:

    1. res solo[: Entoncesr tiene uno[ más que lo hace].

    2. res[r1 donder1 es un segmento inicial apropiado des1: Ya ques1 es un término agradable, por hipótesis de inducción,r1 tiene[ más de] y lo mismo es cierto para[r1.

    3. res[s1 o[s1: Por el resultado anterior, el número de[ y] ens1 son iguales; por lo tanto, el número de[ in[s1 o[s1 es uno más que el número de].

    4. res[s1r2 donder2 es un segmento inicial apropiado des2: Por hipótesis de inducción,r2 contiene[ más de]. Por el resultado anterior, el número de[ y de] ins1 son iguales. Entonces el número de[ in[s1r2 es mayor que el número de].

    5. res[s1s2: Por el resultado anterior, el número de[ y] ens1 son iguales, y lo mismo paras2. Entonces hay uno[s1s2 más[ adentro de lo que hay].


This page titled B.5: Inducción estructural is shared under a CC BY license and was authored, remixed, and/or curated by Richard Zach et al. (Open Logic Project) .

Support Center

How can we help?