Tarea
Dados 2 enteros positivos n
y k
, donde n > k
, emiten el número de extracciones de un conjunto de n
elementos distinguibles a un conjunto de k
elementos distinguibles.
Definición
Una función f: S → T se llama surjection si por cada t∈T hay s∈S tal que f (s) = t.
Ejemplo
Cuando n=3
y k=2
, la salida es 6
, ya que hay 6
extracciones de {1,2,3}
a {1,2}
:
1↦1, 2↦1, 3↦2
1↦1, 2↦2, 3↦1
1↦1, 2↦2, 3↦2
1↦2, 2↦1, 3↦1
1↦2, 2↦1, 3↦2
1↦2, 2↦2, 3↦1
Casos de prueba
n k output
5 3 150
8 4 40824
9 8 1451520
Referencia
Puntuación
Este es el código de golf . La respuesta más corta en bytes gana.
Se aplican lagunas estándar .
code-golf
arithmetic
set-theory
Monja permeable
fuente
fuente
Respuestas:
Jalea ,
54 bytesEsta es una solución de fuerza bruta O (k n ) .
Pruébalo en línea!
Cómo funciona
fuente
Haskell , 48 bytes
Pruébalo en línea!
¿Por qué es el recuento de surjection
s(m,n)=n*s(m-1,n-1)+n*s(m-1,n)
?para cosechar
n
imágenes, puedo[m]
creación singleton en cualquiera de losn
límites que rodeann-1
gruposm
en cualquiera den
los grupos ya existentes de[1..m-1]
Haskell , 38 bytes
Pruébalo en línea!
fuente
Lean , 66 bytes
Pruébalo en línea!
Prueba de corrección
Pruébalo en línea!
Explicación
Dejemos de ungolf la función:
La función se define por la coincidencia de patrones y la recursividad, que tienen soporte incorporado.
Definimos
s(m+1, n+1) = (n+1) * (s(m, n) + s(m, n+1)
ys(0, 0) = 1
, que deja abiertos(m+1, 0)
ys(0, n+1)
, los cuales se definen como0
el último caso.Lean utiliza la sintaxis de cálculo lamdba, por lo que
s m n
es asís(m, n)
.Ahora, la prueba de corrección: lo dije de dos maneras:
El primero es lo que realmente está sucediendo: una biyección entre
[0 ... s(m, n)-1]
y las sobrejeturas de[0 ... m-1]
sobre[0 ... n-1]
.El segundo es cómo se suele decir, que
s(m, n)
es la cardinalidad de las sobreyecciones de[0 ... m-1]
sobre[0 ... n-1]
.Lean utiliza la teoría de tipos como base (en lugar de la teoría de conjuntos). En la teoría de tipos, cada objeto tiene un tipo inherente.
nat
es el tipo de números naturales, y la declaración que0
es un número natural se expresa como0 : nat
. Decimos que0
es de tiponat
, y quenat
tiene0
como habitante.Las proposiciones (declaraciones / aserciones) también son tipos: su habitante es una prueba de la proposición.
def
: Vamos a introducir una definición (porque una biyección es realmente una función, no solo una proposición).correctness
: el nombre de la definición∀ m n
: por cadam
yn
(Lean infiere automáticamente que su tipo esnat
, debido a lo que sigue).fin (s m n)
es el tipo de números naturales que es menor ques m n
. Para hacer un habitante, uno proporciona un número natural y una prueba de que es más pequeño ques m n
.A ≃ B
: biyección entre el tipoA
y el tipoB
. Decir bijection es engañoso, ya que uno realmente tiene que proporcionar la función inversa.{ f : fin m → fin n // function.surjective f }
El tipo de sobrejeciones defin m
afin n
. Esta sintaxis crea un subtipo a partir del tipofin m → fin n
, es decir, el tipo de funciones desdefin m
hastafin n
. La sintaxis es la siguiente{ var : base type // proposition about var }
.λ m
:∀ var, proposition / type involving var
es realmente una función que tomavar
como entrada, por lo queλ m
introduce la entrada.∀ m n,
es abreviatura de∀ m, ∀ n,
nat.rec_on m
: hacer recursividad enm
. Para definir algo param
, definir la cosa para0
y luego dar la cosa parak
, construir la cosa parak+1
. Uno notaría que esto es similar a la inducción, y de hecho esto es el resultado de la correspondencia entre la Iglesia y Howard . La sintaxis es la siguientenat.rec_on var (thing when var is 0) (for all k, given "thing when k is k", build thing when var is "k+1")
.Je, esto se está haciendo largo y solo estoy en la tercera línea de
correctness
...fuente
J , 19 bytes
Pruébalo en línea!
Explicación
fuente
-/@(^~*]!0{])]-i.
R , 49 bytes
Pruébalo en línea!
Implementa una de las fórmulas de Mario Catalani:
o alternativamente:
que produce el mismo número de bytes en R.
fuente
Python 2 ,
56 5350 bytesPruébalo en línea!
-3 bytes gracias a H.PWiz.
-3 bytes gracias a Dennis.
n<k
no todosk
pueden ser mapeados, entonces no hay sobrejeturas.n/k and
se encarga de esto.f(0,0)=1
nos da el único caso base distinto de cero que necesitamos.1/k or
logra esto.fuente
Ruby , 46 bytes
Pruébalo en línea!
Enfoque recursivo estándar ...
fuente
Brain-Flak , 142 bytes
Pruébalo en línea!
Esto usa la fórmula estándar de inclusión-exclusión.
No puedo escribir una explicación completa en este momento, pero aquí hay una explicación de alto nivel:
fuente
Pari / GP , 38 bytes
Pruébalo en línea!
Usando la fórmula de Vladimir Kruchinin en OEIS:
fuente
Casco , 7 bytes
Pruébalo en línea!
Explicación
fuente
JavaScript (Node.js) , 43 bytes
Pruébalo en línea!
fuente
05AB1E , 10 bytes
Pruébalo en línea!
Explicación
fuente