Zadanie
Biorąc pod uwagę 2 dodatnie liczby całkowite, n
i k
gdzie n > k
wypisuje liczbę wypukłości z zestawu n
wyróżnialnych elementów do zestawu k
wyróżnialnych elementów.
Definicja
Funkcja f: S → T nazywa się odrzuceniem, jeżeli dla każdego t∈T istnieje s∈S takie, że f (s) = t.
Przykład
Kiedy n=3
i k=2
, dane wyjściowe są 6
, ponieważ istnieją 6
przypuszczenia od {1,2,3}
do {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
Przypadki testowe
n k output
5 3 150
8 4 40824
9 8 1451520
Odniesienie
Punktacja
To jest golf golfowy . Najkrótsza odpowiedź w bajtach wygrywa.
code-golf
arithmetic
set-theory
Leaky Nun
źródło
źródło
Odpowiedzi:
Galaretka ,
54 bajtówJest to O (K n ) roztworu brute force.
Wypróbuj online!
Jak to działa
źródło
Haskell , 48 bajtów
Wypróbuj online!
Dlaczego liczy się obrzucenie
s(m,n)=n*s(m-1,n-1)+n*s(m-1,n)
?w celu zebrania
n
zdjęć mogę to zrobić[m]
stworzenie singletona w dowolną zn
granic otaczającychn-1
grupym
do dowolnej zn
już istniejących grup[1..m-1]
Haskell , 38 bajtów
Wypróbuj online!
źródło
Lean , 66 bajtów
Wypróbuj online!
Dowód poprawności
Wypróbuj online!
Wyjaśnienie
Odholfujmy funkcję:
Funkcja jest zdefiniowana przez dopasowanie wzorca i rekurencję, które mają wbudowane wsparcie.
Definiujemy
s(m+1, n+1) = (n+1) * (s(m, n) + s(m, n+1)
is(0, 0) = 1
, które pozostawiają otwarte,s(m+1, 0)
is(0, n+1)
oba są zdefiniowane jako0
ostatni przypadek.Lean zastosowania składnia lamdba rachunek, tak
s m n
jests(m, n)
.Teraz dowód poprawności: stwierdziłem to na dwa sposoby:
Pierwszym z nich jest to, co się naprawdę dzieje: bijection pomiędzy
[0 ... s(m, n)-1]
i przypuszczeniami z[0 ... m-1]
na[0 ... n-1]
.Drugim jest to, jak zwykle się mówi, to
s(m, n)
jest liczebność przypuszczeń z[0 ... m-1]
na[0 ... n-1]
.Lean używa teorii typów jako podstawy (zamiast teorii mnogości). W teorii typów każdy obiekt ma swój nieodłączny typ.
nat
jest rodzajem liczb naturalnych, a wyrażenie, które0
jest liczbą naturalną, wyraża się jako0 : nat
. Mówimy, że0
jest to typowenat
inat
ma to0
jako mieszkaniec.Twierdzenia (stwierdzenia / twierdzenia) są również typami: ich mieszkaniec jest dowodem zdania.
def
: Wprowadzimy definicję (ponieważ bijection jest tak naprawdę funkcją, a nie tylko propozycją).correctness
: nazwa definicji∀ m n
: dla każdegom
in
(Lean automatycznie wywnioskuje, że ich typ jestnat
, z powodu tego, co następuje).fin (s m n)
to rodzaj liczb naturalnych, który jest mniejszy niżs m n
. Aby stworzyć mieszkańca, podaje się liczbę naturalną i dowód, że jest ona mniejsza niżs m n
.A ≃ B
: bijection między typemA
a typemB
. Mówienie bijection jest mylące, ponieważ w rzeczywistości trzeba zapewnić funkcję odwrotną.{ f : fin m → fin n // function.surjective f }
rodzaj przypuszczeń odfin m
dofin n
. Ta składnia buduje podtyp na podstawie typufin m → fin n
, tj. Typu funkcji odfin m
dofin n
. Składnia jest następująca{ var : base type // proposition about var }
.λ m
:∀ var, proposition / type involving var
to tak naprawdę funkcja, która przyjmujevar
dane wejściowe, więcλ m
wprowadza dane wejściowe.∀ m n,
jest na krótką rękę∀ m, ∀ n,
nat.rec_on m
: wykonaj rekursję w dnium
. Aby zdefiniować coś dlam
, zdefiniuj rzecz dla,0
a następnie daj rzecz dlak
, zbuduj rzecz dlak+1
. Można zauważyć, że jest to podobne do indukcji i rzeczywiście jest to wynikiem korespondencji Church-Howard . Składnia jest następującanat.rec_on var (thing when var is 0) (for all k, given "thing when k is k", build thing when var is "k+1")
.Hej, robi się to długo i jestem tylko na trzeciej linii
correctness
...źródło
J , 19 bajtów
Wypróbuj online!
Wyjaśnienie
źródło
-/@(^~*]!0{])]-i.
R , 49 bajtów
Wypróbuj online!
Implementuje jedną z formuł autorstwa Mario Catalani:
lub na przemian:
co daje taką samą liczbę bajtów w R.
źródło
Python 2 ,
56 5350 bajtówWypróbuj online!
-3 bajty dzięki H.PWiz.
-3 bajty dzięki Dennisowi.
n<k
nie wszystkok
można zmapować, nie ma żadnych przypuszczeń.n/k and
zajmuje się tym.f(0,0)=1
daje nam jedyną niezerową skrzynkę podstawową, której potrzebujemy.1/k or
osiąga to.źródło
Rubinowy , 46 bajtów
Wypróbuj online!
Standardowe podejście rekurencyjne ...
źródło
Brain-Flak , 142 bajty
Wypróbuj online!
Wykorzystuje to standardową formułę włączenia / wyłączenia.
W tej chwili nie mogę napisać pełnego wyjaśnienia, ale oto wyjaśnienie wysokiego poziomu:
źródło
Pari / GP , 38 bajtów
Wypróbuj online!
Korzystając z formuły Vladimira Kruchinina z OEIS:
źródło
Łuska , 7 bajtów
Wypróbuj online!
Wyjaśnienie
źródło
JavaScript (Node.js) , 43 bajty
Wypróbuj online!
źródło
05AB1E , 10 bajtów
Wypróbuj online!
Wyjaśnienie
źródło