Buenas noches, no me queda claro que define la función ATOMS, no comprendo el conjunto 2^AT, tampoco es clara la formalización del ERP para PROP, las clases de openfing me lee las diapositivas, alguien que me ayude a comprender mejor esto? Gracias!
Hola Diego, el conjunto 2^AT es el conjunto potencia o conjunto de
partes de AT. O sea, es el conjunto de todos los subconjuntos de AT.
Seguramente ya viste este concepto, quizás con otra notación, en cursos
anteriores de matemáticas.
La función ATOMS: PROP -> 2^AT lo que hace es recibir un elemento de
PROP y retornar un elemento de 2^AT (esto es un subconjunto de AT). O
sea que la función toma una fórmula de PROP y devuelve el conjunto de
fórmulas atómicas que aparecen en ella. Te recomiendo que intentes
calcular el resultado de la función ATOMS, paso a paso, para un par de
fórmulas y así terminar de entender cómo funciona.
Respecto a la formalización del ERP para PROP, primero quería aclararte
que, si bien lo tienen que entender, no es algo que típicamente aparezca
en el práctico ni en las evaluaciones. Así que sugiero que intentes
entender conceptualmente qué está pasando, sin preocuparte demasiado por
los detalles de cómo se arma la formalización, porque en general eso no
se pregunta.
El ERP (informalmente) dice que si tenemos una definición libre de un
conjunto inductivo, podemos definir funciones recursivas sobre ese
conjunto. Por ejemplo, los naturales se definen así:
i. 0 ∈ N
ii. Si n ∈ N, entonces n+1 ∈ N
El ERP para esta definición lo que dice es que si damos ecuaciones con
esta pinta:
F(0) = ...
F(n+1) = ... F(n) ... n ...
entonces estamos definiendo correctamente una función.
El problema es que eso con puntitos no es una expresión matemática
formal. Para decir "En F(n+1) puedo usar una expresión que llame
recursivamente a F pero sólo en n y puede usar el valor de n para
calcular el resultado" definimos una función fₛ que recibe un natural
(el n) y un valor del codominio (el valor de la función en el elemento
"anterior"):
fₛ : N x B -> B
Para el caso base, simplemente damos un elemento del codominio:
f₀ ∈ B
Dado esto, el ERP dice que hay una única función que cumple estas
ecuaciones:
F(0) = f₀
F(n+1) = fₛ(n,F(n))
Para PROP es la misma idea. Las reglas de definición de PROP tienen 2
casos bases (pᵢ y ⊥) y unos cuantos casos inductivos, pero la idea es la
misma. Revisa la formalización del ERP para PROP a la luz de lo que te
comento más arriba a ver si queda más claro. Si no, volvé a preguntar
por acá o si podés venir lo vemos en la clase de consulta de hoy.
Saludos,
--
Juan Diego Campo
Instituto de Computación
Facultad de Ingeniería - UdelaR
partes de AT. O sea, es el conjunto de todos los subconjuntos de AT.
Seguramente ya viste este concepto, quizás con otra notación, en cursos
anteriores de matemáticas.
La función ATOMS: PROP -> 2^AT lo que hace es recibir un elemento de
PROP y retornar un elemento de 2^AT (esto es un subconjunto de AT). O
sea que la función toma una fórmula de PROP y devuelve el conjunto de
fórmulas atómicas que aparecen en ella. Te recomiendo que intentes
calcular el resultado de la función ATOMS, paso a paso, para un par de
fórmulas y así terminar de entender cómo funciona.
Respecto a la formalización del ERP para PROP, primero quería aclararte
que, si bien lo tienen que entender, no es algo que típicamente aparezca
en el práctico ni en las evaluaciones. Así que sugiero que intentes
entender conceptualmente qué está pasando, sin preocuparte demasiado por
los detalles de cómo se arma la formalización, porque en general eso no
se pregunta.
El ERP (informalmente) dice que si tenemos una definición libre de un
conjunto inductivo, podemos definir funciones recursivas sobre ese
conjunto. Por ejemplo, los naturales se definen así:
i. 0 ∈ N
ii. Si n ∈ N, entonces n+1 ∈ N
El ERP para esta definición lo que dice es que si damos ecuaciones con
esta pinta:
F(0) = ...
F(n+1) = ... F(n) ... n ...
entonces estamos definiendo correctamente una función.
El problema es que eso con puntitos no es una expresión matemática
formal. Para decir "En F(n+1) puedo usar una expresión que llame
recursivamente a F pero sólo en n y puede usar el valor de n para
calcular el resultado" definimos una función fₛ que recibe un natural
(el n) y un valor del codominio (el valor de la función en el elemento
"anterior"):
fₛ : N x B -> B
Para el caso base, simplemente damos un elemento del codominio:
f₀ ∈ B
Dado esto, el ERP dice que hay una única función que cumple estas
ecuaciones:
F(0) = f₀
F(n+1) = fₛ(n,F(n))
Para PROP es la misma idea. Las reglas de definición de PROP tienen 2
casos bases (pᵢ y ⊥) y unos cuantos casos inductivos, pero la idea es la
misma. Revisa la formalización del ERP para PROP a la luz de lo que te
comento más arriba a ver si queda más claro. Si no, volvé a preguntar
por acá o si podés venir lo vemos en la clase de consulta de hoy.
Saludos,
--
Juan Diego Campo
Instituto de Computación
Facultad de Ingeniería - UdelaR
Se entendió mejor con esas aclaraciones, voy a volver a leer las notas teniendo en cuenta los comentarios, gracias!
Me olvidé de comentar que no estoy de acuerdo en que "las clases de
openfing te leen las diapositivas". Te sugiero que mires los videos con
atención, que seguramente te van a ayudar a entender los temas del
curso.
Por ejemplo, en la clase 5 a partir del minuto 14 se explica con un
ejemplo la función ATOMS, lo que no está en las diapos. Fijate si esa
explicación te ayuda también a entender cómo funciona esta función.
Saludos,
--
Juan Diego Campo
Instituto de Computación
Facultad de Ingeniería - UdelaR
openfing te leen las diapositivas". Te sugiero que mires los videos con
atención, que seguramente te van a ayudar a entender los temas del
curso.
Por ejemplo, en la clase 5 a partir del minuto 14 se explica con un
ejemplo la función ATOMS, lo que no está en las diapos. Fijate si esa
explicación te ayuda también a entender cómo funciona esta función.
Saludos,
--
Juan Diego Campo
Instituto de Computación
Facultad de Ingeniería - UdelaR