Notación para el tipo de función dependiente

Question

Muy a menudo (realmente, muy a menudo), al declarar el tipo de una función, encuentro que falta la notación matemática común. Y deseo una forma de expresar el tipo con mayor precisión.

Supongamos que tenemos un conjunto $X$ y hay alguna función $f$ que toma un subconjunto (no vacío) de $X$ y lo asigna a un elemento de ese subconjunto. Utilizando la notación común, podríamos introducir $f$ como $f \colon 2^X \to X$ . Pero sabemos más. Sabemos que la aplicación de $f$ debe devolver un elemento del argumento.

Utilizando una notación inventada, podríamos escribir $f \colon (A \colon 2^X) \to A$ , dando el nombre $A$ al argumento de la función, y reutilizándolo como tipo del codominio.

Así que las preguntas son:

1. ¿Existe alguna convención aceptada para expresar estos tipos dependientes?
2. Suponiendo que no, ¿la notación propuesta es legible e intuitiva? Personalmente, la encuentro confusa, ya que se parece un poco a $f\colon A \to A$ .

Answer 1

Creo que básicamente estás buscando las anotaciones $$\sum_{x \in X} Y_x \qquad \prod_{x \in X} Y_x.$$ El primero es el conjunto de todos los pares ordenados $(x,y)$ tal que $x \in X$ y $y \in Y_x$ . Esto último significa el conjunto de todas las formas de asignar a cada elemento $x \in X$ un elemento correspondiente de $Y_x$ .

Por ejemplo, una función $f$ que asigna cada subconjunto no vacío de $X$ a un elemento de ese subconjunto podría denotarse $$f \in \prod_{A\in \mathcal{P}_{\neq 0}(X)}A.$$

Algunos lo llaman "teoría de tipos", pero en realidad es sólo teoría de conjuntos.

Answer 2

Si este tipo de funciones se da muchas veces en tu contexto puedes decir lo siguiente:

Dada una familia ${\cal F}$ de subconjuntos no vacíos de $X$ una función $f:\>{\cal F}\to X$ Satisfaciendo a $f(A)\in A$ para todos $A\in{\cal F}$ se llama función de elección .

Answer 3

En la escritura matemática, no es común pensar en propiedades como la que describes como parte del tipo de la función. La notación $f:Y\to Z$ se utiliza esencialmente sólo para denotar el dominio y el codominio de una función (o tal vez una "función parcial"), sin ninguna información adicional.

Si la entrada debe ser un subconjunto no vacío, y no has dejado muy claro que estás permitiendo funciones parciales, entonces no puedes escribir $f:2^X\to X$ ya que eso permitiría un subconjunto vacío como entrada.

Dependiendo de lo que quieras hacer con funciones de este tipo, una forma de expresar tu idea en lenguaje matemático podría ser algo así "Que $f:2^X-\{\emptyset\}\to X$ satisfacer $f(A)\in A$ para todos $A\in2^X-\{\emptyset\}$ ."

Hay muchas variantes de anotación/redacción, pero eso debería darte algunas ideas/ayudarte a acotar lo que te gustaría decir.

Answer 4

Esta respuesta se basa en la respuesta de goblin, sus comentarios y mi experiencia reciente.

Notación del producto

Una función $f \colon A \to B$ es una forma de asignar a cada elemento de $A$ (el dominio) un elemento de $B$ (el codominio). También podemos pensar en esta función como un subconjunto de tuplas $f \subseteq A \times B$ que tiene la propiedad de que cada elemento de $A$ aparece exactamente una vez como primera entrada (izquierda). Utilizando $\prod$ como cuantificador del producto (cartesiano), podemos escribirlo como

$$f \in \prod_{a \in A} \{a\} \times B,$$

o utilizando la notación de índice

$$f \in \prod_{a \in A} B_a.$$

Con esta notación, podemos formular codominios más precisos para cada $a$ por ejemplo, para el caso general en el que $C \colon A \to 2^B$ mapas cada uno $a$ a un subconjunto de $B$ $$f \in \prod_{a \in A} C(a)_a,$$ lo que es más preciso que afirmar $f \colon A \to B$ .

Familias indexadas

Familias indexadas son básicamente los mismos que la notación del producto anterior, simplemente utilizando una notación diferente. Utilizando una familia indexada, podemos escribir $$f = (B_a)_{a \in A},$$ que significa lo mismo que $$f \in \prod_{a \in A} B_a.$$ Obsérvese que ambas anotaciones contienen la misma información: $a \in A$ y $B_a$ .

Cuando se utiliza una familia indexada, la aplicación de la función suele escribirse como $f_a$ en lugar de $f(a)$ pero como ambos significan lo mismo, son formalmente intercambiables. Aunque esto pueda resultar inesperado para algunos lectores.

Notación de la función exponencial como caso especial

Partiendo de la notación del producto $$f \in \prod_{a \in A} B_a,$$ podemos eliminar el índice $a$ si el codominio no depende del valor concreto de $a$ : $$f \in \prod_{a \in A} B.$$ Si reescribimos el producto anterior en forma exponencial, llegamos a la notación de función exponencial (más o menos) común $$f \in B^A.$$