Corrección de erratas PIA

4 files changed, 105 insertions, 91 deletions

diff --git a/pia/n.lyx b/pia/n.lyx
index aa223d7..db09664 100644
--- a/pia/n.lyx
+++ b/pia/n.lyx
@@ -146,12 +146,28 @@ Apuntes de clase.
 \end_layout
 
 \begin_layout Itemize
+\begin_inset ERT
+status open
+
+\begin_layout Plain Layout
+
+
+\backslash
+begin{sloppypar}
+\end_layout
+
+\end_inset
+
+
+\lang english
 Wikipedia, the Free Encyclopedia.
  
 \emph on
 Reduction Strategy
 \emph default
 .
+
+\lang spanish
  Recuperado de 
 \begin_inset Flex URL
 status open
@@ -164,6 +180,19 @@ https://en.wikipedia.org/wiki/Reduction_strategy
 \end_inset
 
  el 25 de septiembre de 2022.
+\begin_inset ERT
+status open
+
+\begin_layout Plain Layout
+
+
+\backslash
+end{sloppypar}
+\end_layout
+
+\end_inset
+
+
 \end_layout
 
 \begin_layout Itemize
diff --git a/pia/n1.lyx b/pia/n1.lyx
index af9b962..45180f6 100644
--- a/pia/n1.lyx
+++ b/pia/n1.lyx
@@ -99,12 +99,11 @@ Entscheidungsproblem
 \lang spanish
 , que pide un algoritmo para determinar si una proposición lógica se deriva
  o no de los axiomas en un sistema lógico que incluya la aritmética de Peano.
- En 1931, Gödel demuestra su 
+ En 1931, Gödel demuestra en su 
 \series bold
 teorema de incompletitud
 \series default
-, que afirma que tal sistema lógico no puede ser a la vez consistente y
- completo.
+ que tal sistema lógico no puede ser a la vez consistente y completo.
  En 1936, Alan Turing y Alonzo Church, de forma independiente, crean respectivam
 ente las 
 \series bold
@@ -453,7 +452,7 @@ programa funcional
  No hay estado ni asignaciones, ni secuenciación o repetición ya que la
  evaluación de una expresión no afecta a otras, pero los usos de estas se
  pueden simular mediante recursividad.
- Se usan funciones sentido matemático, cuyo valor devuelto depende sólo
+ Se usan funciones en sentido matemático, cuyo valor devuelto depende sólo
  de los parámetros de entrada, y se tiene 
 \series bold
 transparencia referencial
@@ -493,16 +492,15 @@ lenguajes funcionales
 \series bold
 Inferencia de tipos
 \series default
-, en el que el programador no tiene que declarar el tipo de los valores
+, con la que el programador no tiene que declarar el tipo de los valores
  en la mayoría de los casos sino que el compilador lo deduce, aunque el
  programador puede declarar el tipo para que el compilador lo compare con
  el tipo inferido.
  Esto aumenta la concisión respecto a los lenguajes en los que hay que declarar
  los tipos explícitamente, y da mayor seguridad y eficiencia respecto a
  los lenguajes con tipos dinámicos ya que evita tener que comprobar los
- tipos en tiempo de ejecución y evita errores en tiempo de ejecución cuando
- estas comprobaciones fallan, pues las comprobaciones ya se han hecho al
- compilar.
+ tipos en tiempo de ejecución y los errores que aparecen cuando estas comprobaci
+ones fallan, ya que las comprobaciones se han hecho al compilar.
 \end_layout
 
 \begin_layout Itemize
@@ -510,9 +508,9 @@ Inferencia de tipos
 \series bold
 Polimorfismo
 \series default
-, en que el tipo de los parámetros o la salida de una función dependen de
- uno o más parámetros, permitiendo una mayor reutilización del código al
- no tener que repetir algoritmos para estructuras similares.
+, con el que el tipo de los parámetros o la salida de una función dependen
+ de uno o más parámetros, permitiendo una mayor reutilización del código
+ al no tener que repetir algoritmos para estructuras similares.
 \end_layout
 
 \begin_layout Itemize
@@ -520,9 +518,9 @@ Polimorfismo
 \series bold
 Evaluación perezosa
 \series default
-, en que no se evalúa un argumento hasta que se necesita, evaluando después
- de sustituirlo en la definición de la función, aunque guardando el valor
- evaluado por eficiencia.
+, no evaluando un argumento hasta que se necesita, evaluando después de
+ sustituirlo en la definición de la función, aunque guardando el valor evaluado
+ por eficiencia.
  Esto es en contraposición a la tradicional 
 \series bold
 evaluación ansiosa
@@ -600,7 +598,7 @@ notación lambda
 \end_inset
 
 .
- Esto se conoce como 
+ A esto se le llama 
 \series bold
 currificación
 \series default
diff --git a/pia/n2.lyx b/pia/n2.lyx
index e33a41d..b67ba71 100644
--- a/pia/n2.lyx
+++ b/pia/n2.lyx
@@ -299,6 +299,37 @@ idénticos
 \end_layout
 
 \begin_layout Standard
+Para reducir el uso de paréntesis, consideramos que la aplicación tiene
+ máxima prioridad y es asociativa por la izquierda, la abstracción se extiende
+ lo más lejos posible y 
+\begin_inset Formula $\to$
+\end_inset
+
+ y 
+\begin_inset Formula $=$
+\end_inset
+
+ tienen el máximo alcance.
+ Además, si 
+\begin_inset Formula $x_{1},\dots,x_{n}$
+\end_inset
+
+ son variables y 
+\begin_inset Formula $M$
+\end_inset
+
+ es un término, la sintaxis 
+\begin_inset Formula $\lambda x_{1}\,x_{2}\,\dots\,x_{n}.M$
+\end_inset
+
+ equivale a 
+\begin_inset Formula $\lambda x_{1}.\lambda x_{2}.\dots\lambda x_{n}.M$
+\end_inset
+
+.
+\end_layout
+
+\begin_layout Standard
 Si 
 \begin_inset Formula $x$
 \end_inset
@@ -405,11 +436,11 @@ donde
 \begin_inset Formula $x\notin\text{FV}(M)$
 \end_inset
 
-, la última regla se puede simplificar como 
-\begin_inset Formula $(\lambda y.M)[N/x]=\lambda y.(M[N/x])$
+, en la última regla se puede omitir 
+\begin_inset Formula $[z/y]$
 \end_inset
 
- y esta sustitución es 
+ y la sustitución es 
 \series bold
 válida
 \series default
@@ -500,6 +531,12 @@ reducciones
  que la reducibilidad es reflexiva y transitiva, y que dos términos son
  iguales si se pueden conectar por una cadena finita de reducciones hacia
  un lado u otro.
+ La igualdad es 
+\series bold
+extensional
+\series default
+, de modo que si dos funciones son iguales, al aplicarlas a los mismos parámetro
+s se obtienen resultados iguales.
 \end_layout
 
 \begin_layout Standard
@@ -515,74 +552,16 @@ cálculo lambda impuro
 \series default
  permite también constantes predefinidas sin definir estas como términos,
  como números o funciones sobre estos.
-\end_layout
-
-\begin_layout Standard
-Para reducir el uso de paréntesis, consideramos que la aplicación tiene
- máxima prioridad y es asociativa por la izquierda, la abstracción se extiende
- lo más lejos posible y 
-\begin_inset Formula $\to$
-\end_inset
-
- y 
-\begin_inset Formula $=$
-\end_inset
-
- tienen el máximo alcance.
- Además, si 
-\begin_inset Formula $x_{1},\dots,x_{n}$
-\end_inset
-
- son variables y 
-\begin_inset Formula $M$
-\end_inset
-
- es un término, la sintaxis 
-\begin_inset Formula $\lambda x_{1}\,x_{2}\,\dots\,x_{n}.M$
-\end_inset
-
- equivale a 
-\begin_inset Formula $\lambda x_{1}.\lambda x_{2}.\dots\lambda x_{n}.M$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Standard
-\begin_inset Note Note
-status open
-
-\begin_layout Plain Layout
-La igualdad es 
+ Se añaden 
 \series bold
-extensional
-\series default
-, de modo que si dos funciones son iguales, dan el mismo resultado para
- todos los parámetros.
- 
-\begin_inset Note Comment
-status open
-
-\begin_layout Plain Layout
-Poner esto cuando se defina 
-\begin_inset Quotes cld
-\end_inset
-
-dar el mismo resultado
-\begin_inset Quotes crd
-\end_inset
-
-
-\end_layout
 
+\begin_inset Formula $\delta$
 \end_inset
 
-
-\end_layout
-
-\end_inset
-
-
+-reducciones
+\series default
+, en las que una expresión en que intervienen constantes se sustituye por
+ su valor según reglas específicas a dichas constantes.
 \end_layout
 
 \begin_layout Standard
@@ -782,7 +761,7 @@ Propiedad del diamante:
 \end_layout
 
 \begin_layout Enumerate
-Si un término es normalizable, se puede llegar a su forma normal por el
+Si un término es normalizable, se puede llevar a su forma normal por el
  orden de reducción normal.
 \end_layout
 
diff --git a/pia/n3.lyx b/pia/n3.lyx
index 54b8cc9..b15577f 100644
--- a/pia/n3.lyx
+++ b/pia/n3.lyx
@@ -97,7 +97,7 @@ y escribimos
 \begin_inset Formula $\mathtt{if}\,i\,\mathtt{then}\,t\,\mathtt{else}\,e\coloneqq\mathtt{cond}\,i\,t\,e$
 \end_inset
 
-, así como 
+, 
 \begin_inset Formula $a\land b\coloneqq\mathtt{and}\,a\,b$
 \end_inset
 
@@ -457,7 +457,7 @@ pues
 \end_inset
 
 , 
-\begin_inset Formula ${\bf Y}\,f=\lambda x.(f({\bf Y}\,f)x)=\lambda x.E[{\bf Y}\,f/F]$
+\begin_inset Formula ${\bf Y}\,f=f({\bf Y}\,f)=\lambda x.E[{\bf Y}\,f/F]$
 \end_inset
 
 .
@@ -511,19 +511,27 @@ ligaduras paralelas
 \end_inset
 
 Una ligadura 
-\begin_inset Formula $x=E$
+\begin_inset Formula $x=\lambda b_{1}\,\dots\,b_{n}.E$
 \end_inset
 
  se puede sustituir por 
-\begin_inset Formula $x\,b_{1}\,\dots\,b_{n}=E\equiv x=\lambda b_{1}\,\dots\,b_{n}.E$
+\begin_inset Formula $x\,b_{1}\,\dots\,b_{n}=E$
+\end_inset
+
+, 
+\begin_inset Formula $x={\bf Y}(\lambda x.E)$
 \end_inset
 
-, por 
-\begin_inset Formula $\mathtt{rec\ }x=E\equiv x={\bf Y}(\lambda x.E)$
+ por 
+\begin_inset Formula $\mathtt{rec\ }x=E$
+\end_inset
+
+ y 
+\begin_inset Formula $x={\bf Y}(\lambda x\,b_{1}\,\dots\,b_{n}.E)$
 \end_inset
 
- o por 
-\begin_inset Formula $\mathtt{rec\ }x\,b_{1}\,\dots\,b_{n}=E\equiv x={\bf Y}(\lambda x\,b_{1}\,\dots\,b_{n}.E)$
+ por 
+\begin_inset Formula $\mathtt{rec\ }x\,b_{1}\,\dots\,b_{n}=E$
 \end_inset
 
 , donde los