Sintaxis y Semantica 2: Tres formas de definir que significa tu codigo

El post anterior definio la sintaxis: el conjunto de cosas que se permite escribir. Los ADTs definen una gramatica. El pattern matching la desestructura. Pero nada de eso responde la verdadera pregunta: que significa el codigo?

Esa pregunta tiene nombre. Se llama semantica. Y hay exactamente tres formas formales de responderla.

Estos tres enfoques fueron desarrollados independientemente por diferentes investigadores entre finales de los 1960 y principios de los 1980. Lo notable no es que existan; es que los programadores los usan los tres a diario sin haber aprendido jamas sus nombres.

Semantica operacional: match como reglas de reduccion

#

Origen: Gordon Plotkin (1981), construyendo sobre el trabajo previo de Robin Milner. La idea es simple: definir el significado de un programa describiendo como se ejecuta, paso a paso, una reduccion a la vez.

Si alguna vez has escrito una expresion match que evalua un arbol de expresiones, has escrito semantica operacional. Cada brazo del match es una regla de reduccion. Cada llamada recursiva es un paso. La notacion formal se ve asi:

────────────────── (E-Num)
Num(n) => n

     e1 => v1    e2 => v2    v3 = v1 + v2
──────────────────────────────────────────── (E-Add)
             Add(e1, e2) => v3

Ahora mira el codigo. En Rust:

fn eval(expr: &Expr) -> f64 {
    match expr {
        Expr::Num(n) => *n,                       // E-Num
        Expr::Add(l, r) => eval(l) + eval(r),     // E-Add
        Expr::Mul(l, r) => eval(l) * eval(r),     // E-Mul
    }
}

En Scala:

def eval(expr: Expr): Double = expr match {
  case Num(n)      => n                    // E-Num
  case Add(l, r)   => eval(l) + eval(r)    // E-Add
  case Mul(l, r)   => eval(l) * eval(r)    // E-Mul
}

Estas no son analogias. Cada brazo del match es literalmente una regla de reduccion traducida de notacion matematica a codigo ejecutable. Los comentarios no son decorativos; son referencias directas a las reglas formales de arriba.

Hay un bonus. Tanto Rust como Scala requieren matching exhaustivo. Si agregas una nueva variante al enum Expr y olvidas manejarla, el compilador rechaza tu codigo. Esto es verificacion de totalidad: el compilador esta demostrando que tu semantica operacional esta definida para cada entrada posible. No para la mayoria de las entradas. Para todas.

Semantica denotacional: funciones como objetos matematicos

#

Origen: Dana Scott y Christopher Strachey (finales de los 1960-70s). En vez de describir como se ejecuta un programa, la semantica denotacional describe que denota un programa: un valor en un dominio matematico.

La intuicion central es desarmantemente simple: una funcion pura es un mapeo matematico. La funcion fn add(x: i64, y: i64) -> i64 no simplemente computa la suma; denota la funcion matematica + sobre enteros. Sin efectos secundarios, sin estado oculto, sin diferencia entre el programa y su significado.

Esto se pone interesante con las type classes. Una implementacion de trait define que significan las operaciones abstractas para un tipo concreto. Cuando escribes una instancia de Monoid, estas proporcionando una denotacion, una interpretacion matematica especifica de empty y combine:

trait Monoid {
    fn empty() -> Self;
    fn combine(self, other: Self) -> Self;
}

impl Monoid for i64 {
    fn empty() -> i64 { 0 }
    fn combine(self, other: i64) -> i64 { self + other }
}
// This IS a denotation: ⟦i64 under Monoid⟧ = (0, +)

trait Monoid[A] {
  def empty: A
  def combine(x: A, y: A): A
}

given Monoid[Long] with {
  def empty = 0L
  def combine(x: Long, y: Long) = x + y
}
// This IS a denotation: ⟦Long under Monoid⟧ = (0, +)

La notacion de doble corchete ⟦...⟧ es estandar en semantica denotacional. Significa “el significado de.” Cuando escribes impl Monoid for i64, estas diciendo: el significado de i64 bajo la interpretacion Monoid es la estructura algebraica (0, +). Cambia la implementacion y cambias la denotacion. Misma sintaxis, diferente semantica.

Scala lleva esto mas lejos. Un for-comprehension es semantica denotacional para la secuenciacion con efectos. for { a <- getUser; b <- getOrders(a) } yield b denota la composicion de dos computaciones con efectos en un contexto monadico. La sintaxis describe la forma; la instancia de Monad proporciona el significado.

Rust tiene su propia version. Los traits From e Into definen morfismos semanticos, transformaciones que preservan significado entre tipos. impl From<String> for UserId dice: existe un mapeo bien definido de cadenas a identificadores de usuario. La conversion no es accidental; es una relacion semantica declarada.

Semantica axiomatica: invariantes impuestas por el compilador

#

Origen: Tony Hoare (1969), construyendo sobre Robert Floyd (1967). La idea: definir el significado no por ejecucion o denotacion, sino por lo que se garantiza que es verdadero antes, durante y despues de que un fragmento de codigo se ejecute. Esto es logica de Hoare: {P} C {Q}. Si la precondicion P se cumple antes del comando C, entonces la postcondicion Q se cumple despues.

Todo el modelo de ownership de Rust es semantica axiomatica.

El borrow checker impone precondiciones (no puedes tener referencias mutables con alias), postcondiciones (los recursos asignados se liberan cuando termina el ownership), e invariantes (los datos son validos para su tipo declarado, siempre). Nunca escribes estos axiomas explicitamente. El compilador los conoce.

Pero puedes codificar axiomas personalizados en el sistema de tipos. Considera NonZeroU32:

// Axiomatic: NonZeroU32 encodes the precondition IN THE TYPE
fn divide(n: u32, d: std::num::NonZeroU32) -> u32 {
    n / d.get()  // No runtime check needed -- the invariant is axiomatic
}

La precondicion “el divisor no es cero” no es un comentario, no es una verificacion en tiempo de ejecucion, no es una esperanza. Es un tipo. El llamador debe demostrar la precondicion construyendo un NonZeroU32, que solo puede crearse a partir de un valor verificado como distinto de cero. El axioma se impone antes de que la funcion sea siquiera invocada.

El patron type-state lleva esto mas lejos, codificando invariantes de maquinas de estado en tiempo de compilacion:

struct Door<State> { _state: std::marker::PhantomData<State> }
struct Locked;
struct Unlocked;

impl Door<Locked> {
    fn unlock(self) -> Door<Unlocked> { /* ... */ }
}

impl Door<Unlocked> {
    fn open(&self) { /* ... */ }
    // Cannot call open() on Door<Locked> -- the compiler enforces the axiom
}

No puedes llamar open() en una puerta bloqueada. No por una verificacion en tiempo de ejecucion. Porque el sistema de tipos lo hace sintacticamente imposible. El axioma “solo las puertas desbloqueadas pueden abrirse” esta codificado en el parametro de tipo, y el compilador rechaza cualquier programa que lo viole.

Scala aborda esto de manera diferente. Donde Rust codifica axiomas estructuralmente, Scala ofrece contratos explicitos al estilo Hoare via require y ensuring:

def divide(n: Long, d: Long): Long = {
  require(d != 0, "divisor must be nonzero")  // Precondition
  n / d
} ensuring { result =>                         // Postcondition
  result * d + (n % d) == n
}

Mecanismo diferente, mismo marco formal. Rust impone axiomas en tiempo de compilacion a traves de tipos. Scala los establece explicitamente como contratos en tiempo de ejecucion. Ambos son semantica axiomatica.

El puente: pattern matching como funcion de interpretacion

#

Estos tres enfoques pueden parecer separados, pero convergen en un lugar: el pattern matching.

Un ADT define la gramatica: que formas existen. Los brazos del match definen la semantica: que significa cada forma. Juntos, la expresion match ES la funcion de interpretacion: el puente formal de la sintaxis a la semantica, escrito ⟦.⟧ : Sintaxis -> Semantica.

Aqui esta, hecho explicito:

Interpretation function ⟦.⟧:
  ⟦Num(n)⟧    = n              (syntax -> value)
  ⟦Add(l,r)⟧  = ⟦l⟧ + ⟦r⟧ (compositional)
  ⟦Mul(l,r)⟧  = ⟦l⟧ * ⟦r⟧

Cada funcion eval que escribes para un arbol de expresiones es esta funcion. El enum Expr es tu sintaxis. El cuerpo del match es tu semantica. La firma de funcion fn eval(expr: &Expr) -> f64 es la firma de tipo de la funcion de interpretacion. Has estado escribiendo semantica formal todo este tiempo.

Asi es como se mapean todos los constructos:

Lo que viene despues

#

Estos tres marcos no son mutuamente excluyentes. Un solo codebase usa los tres simultaneamente. Tu match es operacional. Tus funciones puras son denotacionales. Tus restricciones de tipo son axiomaticas. El lenguaje no te obliga a elegir; los superpone.

Pero hay una tension escondida dentro de esta superposicion. Cuando quieres agregar una nueva variante a tu enum y una nueva operacion sobre el, uno de estos enfoques tiene que ceder. Esa tension tiene nombre, y el siguiente post la examina: el Expression Problem.