En matemáticas, S2S es la teoría monádica de segundo orden con dos sucesoras. Es una de las teorías decidibles naturales más expresivas conocidas, con muchas teorías decidibles interpretables en S2S. Su decidibilidad fue demostrada por Rabin en 1969. [1]
Los objetos de primer orden de S2S son cadenas binarias finitas. Los objetos de segundo orden son conjuntos arbitrarios (o predicados unarios) de cadenas binarias finitas. S2S tiene funciones s → s 0 y s → s 1 en cadenas, y predicado s ∈ S (equivalentemente, S ( s )), lo que significa que la cadena s pertenece al conjunto S .
Algunas propiedades y convenciones:
Debilitaciones de S2S: El S2S débil (WS2S) requiere que todos los conjuntos sean finitos (nótese que la finitud se puede expresar en S2S usando el lema de König ). S1S se puede obtener al requerir que '1' no aparezca en cadenas, y WS1S también requiere finitud. Incluso WS1S puede interpretar la aritmética de Presburger con un predicado para potencias de 2, ya que los conjuntos se pueden usar para representar números binarios ilimitados con adición definible.
Complejidad de decisiones
S2S es decidible, y cada uno de S2S, S1S, WS2S, WS1S tiene una complejidad de decisión no elemental correspondiente a una pila de exponenciales que crece linealmente. Para el límite inferior, basta con considerar Σ 1 1 WS1S oraciones. Se puede utilizar un único cuantificador de segundo orden para proponer un cálculo aritmético (u otro), que se puede verificar utilizando cuantificadores de primer orden si podemos probar qué números son iguales. Para esto, si codificamos adecuadamente los números 1.. m , podemos codificar un número con representación binaria i 1 i 2 ... i m como i 1 1 i 2 2 ... i m m , precedido por un resguardo. Al fusionar la prueba de resguardos y reutilizar los nombres de las variables, el número de bits es lineal en el número de exponenciales. Para el límite superior, utilizando el procedimiento de decisión (a continuación), las oraciones con alternancia de cuantificadores k -veces se pueden decidir en el tiempo correspondiente a la exponenciación k + O (1) veces de la longitud de la oración (con constantes uniformes).
Axiomatización
WS2S se puede axiomatizar a través de ciertas propiedades básicas más un esquema de inducción. [3]
S2S puede axiomatizarse parcialmente por:
(1) ∃! s ∀ t ( t 0 ≠ s ∧ t 1 ≠ s ) (cadena vacía, denotada por ε; ∃! s significa "hay un único s ")
(2) ∀ s , t ∀ i ∈{0,1} ∀ j ∈{0,1} ( si = tj ⇒ s = t ∧ i = j ) (el uso de i y j es una abreviatura; para i = j , 0 no es igual a 1)
(3) ∀ S ( S (ε) ∧ ∀ s ( S ( s ) ⇒ S ( s 0) ∧ S ( s 1))⇒ ∀ s S (s)) ( inducción )
(4) ∃ S ∀ s ( S ( s ) ⇔ φ( s )) ( S no libre en φ)
(4) es el esquema de comprensión sobre fórmulas φ, que siempre se cumple para lógica de segundo orden. Como es habitual, si φ tiene variables libres no mostradas, tomamos la clausura universal del axioma. Si la igualdad es primitiva para predicados, también se añade extensionalidad S = T ⇔ ∀ s ( S ( s ) ⇔ T ( s )). Puesto que tenemos comprensión, la inducción puede ser un enunciado único en lugar de un esquema.
La axiomatización análoga de S1S es completa. [4] Sin embargo, para S2S, la completitud está abierta (a partir de 2021). Si bien S1S tiene uniformización, no existe una función de elección definible por S2S (incluso permitiendo parámetros) que, dado un conjunto no vacío S, devuelva un elemento de S , [5] y los esquemas de comprensión se amplían comúnmente con varias formas del axioma de elección . Sin embargo, (1)-(4) es completo cuando se extiende con un esquema de determinación para ciertos juegos de paridad . [6]
S2S también puede axiomatizarse mediante Π 1 3 oraciones (usando la relación de prefijo en cadenas como primitiva). Sin embargo, no es finitamente axiomatizable, ni puede axiomatizarse mediante Σ 1 3 oraciones incluso si agregamos un esquema de inducción y un conjunto finito de otras oraciones (esto se deduce de su conexión con Π 1 2 -CA 0 ).
Para cada k finito , la teoría monádica de segundo orden (MSO) de grafos contables con ancho de árbol ≤ k (y una descomposición de árbol correspondiente) es interpretable en S2S (ver el teorema de Courcelle ). Por ejemplo, la teoría MSO de árboles (como grafos) o de grafos en serie-paralelos es decidible. Aquí (es decir, para un ancho de árbol acotado), también podemos interpretar el cuantificador de finitud para un conjunto de vértices (o aristas), y también contar vértices (o aristas) en un conjunto módulo un entero fijo. Permitir grafos incontables no cambia la teoría. Además, a modo de comparación, S1S puede interpretar grafos conexos de ancho de camino acotado .
Por el contrario, para cada conjunto de grafos con un ancho de árbol ilimitado, su teoría MSO existencial (es decir, Σ 1 1 ) es indecidible si permitimos predicados tanto en vértices como en aristas. Por lo tanto, en cierto sentido, la decidibilidad de S2S es la mejor posible. Los grafos con un ancho de árbol ilimitado tienen menores de cuadrícula grandes, que se pueden usar para simular una máquina de Turing .
Por reducción a S2S, la teoría MSO de órdenes contables es decidible, como lo es la teoría MSO de árboles contables con sus órdenes Kleene–Brouwer . Sin embargo, la teoría MSO de ( , <) es indecidible. [7] [8] La teoría MSO de ordinales <ω 2 es decidible; la decidibilidad para ω 2 es independiente de ZFC (asumiendo Con(ZFC + cardinal débilmente compacto )). [9] Además, un ordinal es definible usando lógica monádica de segundo orden sobre ordinales si y solo si se puede obtener a partir de cardinales regulares definibles por adición y multiplicación de ordinales. [10]
S2S es útil para la decidibilidad de ciertas lógicas modales, y la semántica de Kripke conduce naturalmente a árboles.
S2S+U (o simplemente S1S+U) es indecidible si U es el cuantificador no acotado — U X Φ( X ) sólo si Φ( X ) se cumple para algún X finito arbitrariamente grande . [11] Sin embargo, WS2S+U, incluso con cuantificación sobre caminos infinitos, es decidible, incluso con subfórmulas S2S que no contienen U. [12]
Un conjunto de cadenas binarias es definible en S2S si y solo si es regular (es decir, forma un lenguaje regular ). En S1S, un predicado (unario) sobre conjuntos es definible (sin parámetros) si y solo si es un lenguaje ω-regular . Para S2S, para fórmulas que usan sus variables libres solo en cadenas que no contienen un 1, la expresividad es la misma que para S1S.
Para cada fórmula S2S φ( S 1 ,..., S k ), (con k variables libres) y árbol finito de cadenas binarias T , φ( S 1 ∩T,..., S k ∩T) se puede calcular en un tiempo lineal en | T | (véase el teorema de Courcelle ), pero como se señaló anteriormente, la sobrecarga se puede iterar exponencialmente en el tamaño de la fórmula (más precisamente, el tiempo es ).
Para S1S, cada fórmula es equivalente a una fórmula Δ 1 1 y a una combinación booleana de fórmulas aritméticas Π 0 2. Además, cada fórmula S1S es equivalente a la aceptación por parte de un ω-autómata correspondiente de los parámetros de la fórmula. El autómata puede ser un autómata de paridad determinista: un autómata de paridad tiene una prioridad entera para cada estado y acepta si y solo si la prioridad más alta vista infinitamente a menudo es impar (alternativamente, par).
Para S2S, utilizando autómatas de árbol (abajo), cada fórmula es equivalente a una fórmula Δ 1 2 . Además, cada fórmula S2S es equivalente a una fórmula con solo cuatro cuantificadores, ∃ S ∀ T ∃ s ∀ t ... (asumiendo que nuestra formalización tiene tanto la relación de prefijo como las funciones sucesoras). Para S1S, tres cuantificadores (∃ S ∀ s ∃ t ) son suficientes, y para WS2S y WS1S, dos cuantificadores (∃ S ∀ t ) son suficientes; la relación de prefijo no es necesaria aquí para WS2S y WS1S.
Sin embargo, con variables libres de segundo orden, no todas las fórmulas S2S se pueden expresar en aritmética de segundo orden a través de solo Π 1 1 recursión transfinita (ver matemáticas inversas ). RCA 0 + (esquema) {τ: τ es una oración S2S verdadera} es equivalente a (esquema) {τ: τ es una oración Π 1 3 demostrable en Π 1 2 -CA 0 }. [13] [14] Sobre una teoría base, los esquemas son equivalentes a (esquema sobre k ) ∀ S ⊆ω ∃α 1 <...<α k L α 1 ( S ) ≺ Σ 1 ... ≺ Σ 1 L α k (S) donde L es el universo construible (ver también ordinal contable grande ). Debido a la inducción limitada, Π 1 2 -CA 0 no prueba que todas las afirmaciones Π 1 3 S2S verdaderas (según el procedimiento de decisión estándar) sean realmente verdaderas, aunque cada una de esas oraciones sea demostrable Π 1 2 -CA 0 .
Además, dados conjuntos de cadenas binarias S y T , los siguientes son equivalentes:
(1) T es S2S definible a partir de algún conjunto de cadenas binarias en tiempo polinomial computable a partir de S .
(2) T se puede calcular a partir del conjunto de posiciones ganadoras para algún juego cuyo pago es una combinación booleana finita de Π 0 2 ( S ) conjuntos.
(3) T se puede definir a partir de S en μ-cálculo aritmético (fórmulas aritméticas + lógica de mínimo punto fijo )
(4) T está en el mínimo β-modelo (es decir, un ω-modelo cuya contraparte teórica de conjuntos es transitiva ) que contiene a S y satisface todas las Π 1 3 consecuencias de en Π 1 2 -CA 0 .
Para (3)⇒(2), defina un juego en el que el jugador 1 intenta demostrar que el elemento deseado s está dentro del punto menos fijo. El jugador 1 etiqueta gradualmente los elementos que incluyen s con números racionales, con la intención de que correspondan a las etapas ordinales de la inducción monótona (cualquier ordinal contable es integrable en ). El jugador 2 juega elementos con etiquetas estrictamente descendentes (y puede pasar) y gana si la secuencia es infinita o el jugador 2 gana el último juego auxiliar. En el juego auxiliar, el jugador 1 intenta demostrar que el último elemento elegido por el jugador 2 es un paso inductivo válido utilizando elementos con etiquetas más pequeñas. Ahora bien, si s no está en el punto menos fijo, entonces el conjunto de etiquetas está mal fundado, o un paso inductivo es incorrecto, y (usando monotonía) esto puede ser recogido por el jugador 2. (Si el jugador 1 juega una etiqueta más pequeña fuera del punto menos fijo, el jugador 2 puede usarla (abandonando el juego auxiliar), de lo contrario (usando monotonía) el jugador 2 puede usar una estrategia de juego auxiliar que asume que el conjunto de etiquetas más pequeñas en el juego original será igual al punto menos fijo).
Para (4)⇒(3), utilizamos la inducción monótona para construir un segmento inicial de la jerarquía construible por encima de un número real dado r . Esto funciona siempre que cada ordinal α se identifique por alguna propiedad expresable apropiadamente de α de modo que podamos codificar α por un número natural y continuar. Ahora, supongamos que construimos L α (r) y el paso inductivo (que utiliza L α (r) como parámetro) permite examinar L β (r). Si aparece un nuevo hecho Σ 1 (L(r),∈,r) entre α y β, podemos usarlo para etiquetar α y continuar. De lo contrario, obtenemos las cadenas elementales Σ 1 anteriores cuya longitud corresponde a la profundidad de anidamiento de las definiciones inductivas monótonas.
Para la equivalencia de RCA 0 + S2S con {Π 1 3 φ: Π 1 2 -CA 0 ⊢φ}, para cada k la determinabilidad posicional con k prioridades es demostrable en Π 1 2 -CA 0 , mientras que el resto (en términos de demostrar oraciones S2S) se puede hacer en una teoría de base débil. Por el contrario, RCA 0 + S2S nos da un esquema de determinabilidad que da existencia de puntos mínimos fijos (por una modificación de (3)⇒(2) anterior e incluso sin requerir posicionalidad; ver la referencia). A su vez, su existencia (usando (4)⇒(3)) da las cadenas elementales Σ 1 deseadas.
Además del modelo estándar (que es el único modelo MSO para S1S y S2S), existen otros modelos para S1S y S2S, que utilizan algunos en lugar de todos los subconjuntos del dominio (ver semántica de Henkin ).
Para cada S ⊆ω, los conjuntos recursivos en S forman un submodelo elemental del modelo S1S estándar, y lo mismo para cada colección no vacía de subconjuntos de ω cerrados bajo unión de Turing y reducibilidad de Turing. [16]
Esto se desprende de la recursividad relativa de los conjuntos definibles S1S más la uniformización:
- φ( s ) (como una función de s ) se puede calcular a partir de los parámetros de φ y los valores de φ( s ′ ) para un conjunto finito de s ′ (con su tamaño limitado por el número de estados en un autómata determinista para φ).
- Un testigo para ∃ S φ( S ) se puede obtener eligiendo k y un fragmento finito de S ′ de S , y extendiendo repetidamente S ′ de modo que la prioridad más alta durante cada extensión sea k y que la extensión se pueda completar en S satisfaciendo φ sin alcanzar prioridades superiores a k (estas solo se permiten para el S ′ inicial ). Además, al utilizar lexicográficamente las opciones menos cortas, existe una fórmula S1S φ' tal que φ'⇒φ y ∃ S φ( S ) ⇔∃! S φ'( S ) (es decir, uniformización; φ puede tener variables libres que no se muestran; φ' depende solo de la fórmula φ).
El modelo mínimo de S2S consiste en todos los lenguajes regulares en cadenas binarias. Es un submodelo elemental del modelo estándar, por lo que si un conjunto de árboles definibles sin parámetros de S2S no está vacío, entonces incluye un árbol regular. Un lenguaje regular también puede ser tratado como un árbol binario infinito completo etiquetado {0,1} (identificado con predicados en cadenas). Un árbol etiquetado es regular si puede obtenerse desenrollando un grafo dirigido finito etiquetado por vértice con un vértice inicial; un ciclo (dirigido) en el grafo alcanzable desde el vértice inicial da un árbol infinito. Con esta interpretación y codificación de árboles regulares, cada oración S2S verdadera ya puede ser demostrable en aritmética de funciones elementales . Son los árboles no regulares los que pueden requerir comprensión no predicativa para la determinación (abajo). Existen modelos no regulares (es decir, que contienen lenguajes no regulares) de S1S (y presumiblemente de S2S) (con y sin la parte estándar de primer orden) con una relación de satisfacción computable. Sin embargo, el conjunto de conjuntos recursivos de cadenas no forma un modelo de S2S debido a fallas de comprensión y determinación.
La prueba de decidibilidad es mostrando que cada fórmula es equivalente a la aceptación por un autómata de árbol no determinista (ver autómata de árbol y autómata de árbol infinito ). Un autómata de árbol infinito comienza en la raíz y se mueve hacia arriba del árbol, y acepta si y solo si cada rama del árbol acepta. Un autómata de árbol no determinista acepta si y solo si el jugador 1 tiene una estrategia ganadora, donde el jugador 1 elige un par permitido (para el estado actual y la entrada) de nuevos estados ( p 0 , p 1 ), mientras que el jugador 2 elige la rama, con la transición a p 0 si se elige 0 y p 1 en caso contrario. Para un autómata co-no determinista, todas las elecciones son del jugador 2, mientras que para determinista, (p 0 ,p 1 ) está fijado por el estado y la entrada; y para un autómata de juego, los dos jugadores juegan un juego finito para establecer la rama y el estado. La aceptación en una rama se basa en estados vistos infinitamente a menudo en la rama; Los autómatas de paridad son suficientemente generales aquí.
Para convertir las fórmulas en autómatas, el caso base es fácil, y el no determinismo da cierre bajo cuantificadores existenciales, por lo que solo necesitamos cierre bajo complementación. Usando la determinación posicional de los juegos de paridad (que es donde necesitamos la comprensión impredicativa), la no existencia de una estrategia ganadora del jugador 1 da una estrategia ganadora del jugador 2 S , con un autómata de árbol co-no determinista que verifica su solidez. El autómata puede entonces volverse determinista (que es donde obtenemos un aumento exponencial en el número de estados), y por lo tanto la existencia de S corresponde a la aceptación por parte de un autómata no determinista.
Determinación: Demostrablemente en ZFC , los juegos de Borel están determinados , y la prueba de determinación para combinaciones booleanas de fórmulas Π 0 2 (con parámetros reales arbitrarios) también da una estrategia aquí que depende solo del estado actual y la posición en el árbol. La prueba es por inducción sobre el número de prioridades. Suponga que hay k prioridades, siendo k la prioridad más alta , y que k tiene la paridad correcta para el jugador 2. Para cada posición (posición del árbol + estado), asigne el ordinal α menor (si lo hay) de modo que el jugador 1 tenga una estrategia ganadora con todas las posiciones de prioridad k ingresadas (después de uno o más pasos) (si las hay) que tengan etiquetas <α. El jugador 1 puede ganar si la posición inicial está etiquetada: Cada vez que se alcanza un estado de prioridad k , el ordinal se reduce y, además, entre las disminuciones, el jugador 1 puede usar una estrategia para k -1 prioridades. El jugador 2 puede ganar si la posición no está etiquetada: por la determinación de k -1 prioridades, el jugador 2 tiene una estrategia que gana o entra en un estado de prioridad k no etiquetado , en cuyo caso el jugador 2 puede volver a utilizar esa estrategia. Para hacer que la estrategia sea posicional (por inducción en k ), al jugar el juego auxiliar, si dos estrategias posicionales elegidas conducen a la misma posición, continúe con la estrategia con el α más bajo, o para la misma posición inicial α (o para el jugador 2) más baja (de modo que podamos cambiar una estrategia un número finito de veces).
Determinización de autómatas: Para la determinización de autómatas de árboles co-no deterministas, basta con considerar ω-autómatas, tratar la elección de rama como entrada, determinizar el autómata y utilizarla para el autómata de árbol determinista. Nótese que esto no funciona para autómatas de árboles no deterministas ya que la determinización para ir a la izquierda (es decir, s → s 0) puede depender del contenido de la rama derecha; en contraste con el no determinismo, los autómatas de árboles deterministas ni siquiera pueden aceptar conjuntos precisamente no vacíos. Para determinizar un ω-autómata no determinista M (para co-no determinista, tome el complemento, notando que los autómatas de paridad deterministas están cerrados bajo complementos), podemos utilizar un árbol Safra con cada nodo almacenando un conjunto de estados posibles de M , y la creación y eliminación de nodos en función de alcanzar estados de alta prioridad. Para más detalles, véase [17] o [18] .
Decidibilidad de la aceptación: La aceptación por parte de un autómata de paridad no determinista del árbol vacío corresponde a un juego de paridad en un grafo finito G . Utilizando la determinabilidad posicional (también llamada sin memoria) anterior, esto se puede simular mediante un juego finito que termina cuando llegamos a un bucle, con la condición ganadora basada en el estado de mayor prioridad en el bucle. Una optimización inteligente da un algoritmo de tiempo cuasipolinomial , [19] que es un tiempo polinomial cuando el número de prioridades es lo suficientemente pequeño (lo que ocurre comúnmente en la práctica).
Teoría de árboles: Para la decidibilidad de la lógica MSO en árboles (es decir, grafos que son árboles), incluso con finitud y cuantificadores de conteo modulares para objetos de primer orden, podemos incrustar árboles contables en el árbol binario completo y usar la decidibilidad de S2S. Por ejemplo, para un nodo s , podemos representar a sus hijos por s 1, s 01, s 001, y así sucesivamente. Para árboles incontables, podemos usar el teorema de Shelah-Stup (abajo). También podemos agregar un predicado para un conjunto de objetos de primer orden que tienen cardinalidad ω 1 , y el predicado para cardinalidad ω 2 , y así sucesivamente para cardinales regulares infinitos. Los grafos de ancho de árbol acotado son interpretables usando árboles, y sin predicados sobre aristas esto también se aplica a grafos de ancho de camarilla acotado .
Extensiones de árbol de teorías monádicas: Por el teorema de Shelah-Stup, [20] [21] si un modelo relacional monádico M es decidible, entonces también lo es su contraparte de árbol. Por ejemplo, (módulo de elección de formalización) S2S es la contraparte de árbol de {0,1}. En la contraparte de árbol, los objetos de primer orden son secuencias finitas de elementos de M ordenados por extensión, y una M -relación P i se mapea a P i '( vd 1 ,..., vd k ) ⇔ P i ( d 1 ,..., d k ) con P i ' falso en caso contrario ( d j ∈ M , y v es una secuencia (posiblemente vacía) de elementos de M ). La prueba es similar a la prueba de decidibilidad S2S. En cada paso, un autómata (no determinista) obtiene una tupla de M objetos (posiblemente de segundo orden) como entrada, y una fórmula M determina qué transiciones de estado están permitidas. El jugador 1 (como se muestra arriba) elige un mapeo hijo⇒estado que está permitido por la fórmula (dado el estado actual), y el jugador 2 elige el hijo (del nodo) para continuar. Para presenciar el rechazo por parte de un autómata no determinista, para cada (nodo, estado) elija un conjunto de pares (hijo, estado) de manera que para cada elección, al menos uno de los pares sea alcanzado, y de manera que todos los caminos resultantes conduzcan al rechazo.
Combinando una teoría monádica con una teoría de primer orden: el teorema de Feferman–Vaught se extiende/aplica de la siguiente manera. Si M es un modelo MSO y N es un modelo de primer orden, entonces M sigue siendo decidible en relación con un oráculo (Teoría( M ), Teoría( N )) incluso si M se aumenta con todas las funciones M → N donde M se identifica con sus primeros objetos, y para cada s ∈ M usamos una copia disjunta de N , con el lenguaje modificado en consecuencia. Por ejemplo, si N es ( ,0,+,⋅), podemos afirmar ∀(función f ) ∀ s ∃ r ∈ N s f ( s ) + N s r = 0 N s . Si M es S2S (o más generalmente, la contraparte de árbol de algún modelo monádico), los autómatas ahora pueden usar N -fórmulas, y por lo tanto convertir f : M → N k en una tupla de M conjuntos. La disyunción es necesaria ya que de lo contrario para cada N infinito con igualdad, el S2S extendido o simplemente WS1S es indecidible. Además, para una teoría T (posiblemente incompleta) , la teoría T M de M -productos de T es decidible en relación con un oráculo (Teoría( M ), T ), donde un modelo de T M usa un modelo disjunto arbitrario N s de T para cada s ∈ M (como arriba, M es un modelo MSO; Teoría( N s ) puede depender de s ). La prueba es por inducción sobre la complejidad de la fórmula. Sea v s la lista de N s variables libres, incluyendo f ( s ) si la función f es libre. Por inducción, se demuestra que v s sólo se utiliza a través de un conjunto finito de N fórmulas con | v s | variables libres. Por lo tanto, podemos cuantificar todos los resultados posibles utilizando N (o T ) para responder lo que es posible, y dada una lista de posibilidades (o restricciones), formular una oración correspondiente en M .
Codificación en extensiones de S2S: Cada predicado decidible en cadenas puede ser codificado (con codificación y decodificación de tiempo lineal) para la decidibilidad de S2S (incluso con las extensiones anteriores) junto con el predicado codificado. Demostración: Dado un autómata de árbol infinito no determinista, podemos particionar el conjunto de árboles binarios etiquetados finitos (que tienen etiquetas sobre las que el autómata puede operar) en un número finito de clases tales que si un árbol binario infinito completo puede estar compuesto de árboles de la misma clase, la aceptación depende solo de la clase y el estado inicial (es decir, el estado en el que el autómata ingresa al árbol). (Obsérvese una similitud aproximada con el lema de bombeo ). Por ejemplo (para un autómata de paridad), asigne árboles a la misma clase si tienen el mismo predicado que dado initial_state y el conjunto Q de pares (state, lowest_priority_reached) devuelve si el jugador 1 (es decir , no determinismo) puede forzar simultáneamente que todas las ramas correspondan a elementos de Q. Ahora, para cada k , elija un conjunto finito de árboles (aptos para codificación) que pertenezcan a la misma clase para los autómatas 1- k , con la elección de clase consistente a lo largo de k . Para codificar un predicado, codifique algunos bits usando k = 1, luego más bits usando k = 2, y así sucesivamente.
Referencia adicional: Weyer, Mark (2002). "Decidibilidad de S1S y S2S". Autómatas, lógicas y juegos infinitos . Apuntes de clase en informática. Vol. 2500. Springer. págs. 207–230. doi :10.1007/3-540-36387-4_12. ISBN.
978-3-540-00388-5.
