¿Qué significa "monotonicidad" en el contexto de la mutabilidad?

8

Estoy leyendo el lenguaje de programación Rust y encontré el siguiente pasaje:

Recuerde que escribir en una estructura no es una operación atómica, y muchas funciones como vec.push()pueden reasignarse internamente y causar un comportamiento inseguro, por lo que incluso la monotonicidad puede no ser suficiente para justificar UnsafeCell

Simplemente apareció de la nada en el libro y he tenido dificultades en línea tratando de encontrar lo que significa exactamente en este contexto. Demasiada información es sobre el concepto de "monotonicidad" de las funciones matemáticas, que ya conocía, pero aparentemente no es muy útil.

Solo me pareció encontrar este artículo que habla de ello.

Ahora, además de respetar la igualdad de manera obvia, también incluyo la estipulación de que un programa funcional debe respetar la monotonía de las observaciones. ¿Qué quiero decir con esto? Debe ser que una vez que haya observado algo en un momento determinado, eso no dejará de ser evidente en el futuro. Esto es análogo a la propiedad de monotonicidad en la semántica de Kripke o Beth.

Sin embargo, esto también es bastante abstracto y tampoco estoy seguro de que hable de lo mismo.

xji
fuente

Respuestas:

5

El autor parece estar usando el mismo concepto (general) de "monotonicidad" que en matemáticas puras.

Usando el ejemplo de a vector, si el tamaño de una instancia particular de vectores monótono, entonces parecería razonable suponer que la ubicación de la memoria de cualquier pushelemento editado previamente no se modificará posteriormente, y por lo tanto es seguro cambiar directamente el valor de ese elemento sin tener que sincronizar con las operaciones vectorposteriores de push.

Esta suposición parece razonable por la misma razón por la que parece razonable suponer que la ubicación de la memoria de un elemento previamente insertado en una pila (no circular, basada en matriz, sin límites) cuyo tamaño está aumentando estrictamente no se verá afectada por un futuro pushoperación. Esto contrasta con una pila en la que se invocan tanto las operaciones pushcomo las popoperaciones, por lo que la ubicación de la memoria de un elemento previamente empujado puede ser "eliminada" por una popoperación, y por lo tanto disponible para ser asignada una vez más (es decir, modificada) por un pushOperación posterior .

El punto del autor es que esta suposición no es correcta, ya que incluso en una estructura de datos cuyo tamaño está aumentando estrictamente, las inserciones futuras pueden afectar elementos previamente insertados al desencadenar una reasignación interna de algún tipo que sea diferente del efecto "lógico" de la inserción .

Travis
fuente
OKAY. Parece que lo pensé demasiado. Parece que no es algo de teoría PL profunda después de todo. Adivina la forma en que se presentó repentinamente en el texto sin mucho contexto me frotó de la manera incorrecta jaja.
xji