Tugas
Diberikan 2 bilangan bulat positif n
dan k
, di mana n > k
, mengeluarkan jumlah dugaan dari satu set n
elemen yang dapat dibedakan menjadi satu set k
elemen yang dapat dibedakan.
Definisi
Fungsi f: S → T disebut surjeksi jika untuk setiap t∈T ada s suchS sehingga f (s) = t.
Contoh
Kapan n=3
dan k=2
, outputnya adalah 6
, karena ada 6
dugaan dari {1,2,3}
ke {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
testcases
n k output
5 3 150
8 4 40824
9 8 1451520
Referensi
Mencetak gol
Ini adalah kode-golf . Jawabannya terpendek dalam byte menang.
Celah standar berlaku.
code-golf
arithmetic
set-theory
bocor Nun
sumber
sumber
Jawaban:
Jelly ,
54 byteIni adalah solusi brute force O (k n ) .
Cobalah online!
Bagaimana itu bekerja
sumber
Haskell , 48 byte
Cobalah online!
Mengapa surjection diperhitungkan
s(m,n)=n*s(m-1,n-1)+n*s(m-1,n)
?untuk memanen
n
gambar, saya juga bisa[m]
ciptaan singleton ke salah satun
batas di sekitarn-1
kelompokm
ke salah satun
grup yang sudah ada[1..m-1]
Haskell , 38 byte
Cobalah online!
sumber
Lean , 66 byte
Cobalah online!
Bukti kebenaran
Cobalah online!
Penjelasan
Mari kita ungolf fungsinya:
Fungsi ini ditentukan oleh pencocokan pola dan rekursi, yang keduanya memiliki dukungan bawaan.
Kami mendefinisikan
s(m+1, n+1) = (n+1) * (s(m, n) + s(m, n+1)
dans(0, 0) = 1
, yang meninggalkan terbukas(m+1, 0)
dans(0, n+1)
, keduanya didefinisikan0
oleh kasus terakhir.Lean menggunakan sintaks kalkulus lamdba, begitu
s m n
jugas(m, n)
.Sekarang, bukti kebenaran: Saya menyatakannya dalam dua cara:
Yang pertama adalah apa yang sebenarnya terjadi: bijection antara
[0 ... s(m, n)-1]
dan surjections dari[0 ... m-1]
ke[0 ... n-1]
.Yang kedua adalah bagaimana biasanya dinyatakan, bahwa
s(m, n)
adalah kardinalitas dari surjections dari[0 ... m-1]
ke[0 ... n-1]
.Lean menggunakan teori tipe sebagai fondasinya (bukan teori himpunan). Dalam teori tipe, setiap objek memiliki tipe yang melekat padanya.
nat
adalah jenis bilangan asli, dan pernyataan yang0
merupakan bilangan alami dinyatakan sebagai0 : nat
. Kami mengatakan bahwa itu0
adalah tipenat
, dan yangnat
memiliki0
sebagai penduduk.Proposisi (pernyataan / pernyataan) juga tipe: penghuninya adalah bukti proposisi.
def
: Kami akan memperkenalkan definisi (karena bijection benar-benar fungsi, bukan hanya proposisi).correctness
: nama definisi∀ m n
: untuk setiapm
dann
(Lean secara otomatis menyimpulkan bahwa tipenya adalahnat
, karena apa yang berikut).fin (s m n)
adalah jenis bilangan alami yang lebih kecil daris m n
. Untuk membuat penghuni, orang memberikan nomor alami dan bukti bahwa itu lebih kecil daris m n
.A ≃ B
: bijection antara jenisA
dan jenisnyaB
. Mengatakan bijection menyesatkan, karena seseorang harus menyediakan fungsi terbalik.{ f : fin m → fin n // function.surjective f }
jenis surjections darifin m
kefin n
. Sintaks ini membangun subtipe dari tipefin m → fin n
, yaitu tipe fungsi darifin m
hinggafin n
. Sintaksnya adalah{ var : base type // proposition about var }
.λ m
:∀ var, proposition / type involving var
benar-benar fungsi yang dibutuhkanvar
sebagai input, jadiλ m
perkenalkan input.∀ m n,
adalah kependekan dari∀ m, ∀ n,
nat.rec_on m
: lakukan rekursi padam
. Untuk menentukan sesuatu untukm
, menentukan hal untuk0
dan kemudian memberikan hal untukk
, membangun hal untukk+1
. Orang akan melihat bahwa ini mirip dengan induksi, dan memang ini adalah hasil dari korespondensi Gereja-Howard . Sintaksnya adalahnat.rec_on var (thing when var is 0) (for all k, given "thing when k is k", build thing when var is "k+1")
.Heh, ini semakin lama dan aku hanya di baris ketiga
correctness
...sumber
J , 19 byte
Cobalah online!
Penjelasan
sumber
-/@(^~*]!0{])]-i.
R , 49 byte
Cobalah online!
Menerapkan salah satu formula oleh Mario Catalani:
atau secara bergantian:
yang menghasilkan jumlah byte yang sama dalam R.
sumber
Python 2 ,
56 5350 byteCobalah online!
-3 byte terima kasih kepada H.PWiz.
-3 byte terima kasih kepada Dennis.
n<k
tidak semuak
bisa dipetakan maka tidak ada dugaan.n/k and
urus ini.f(0,0)=1
memberi kita satu-satunya case base bukan nol yang kita butuhkan.1/k or
mencapai ini.sumber
Ruby , 46 byte
Cobalah online!
Pendekatan rekursif standar ...
sumber
Brain-Flak , 142 byte
Cobalah online!
Ini menggunakan rumus inklusi-pengecualian standar.
Saya tidak bisa menulis penjelasan lengkap saat ini, tapi inilah penjelasan tingkat tinggi:
sumber
Pari / GP , 38 byte
Cobalah online!
Menggunakan rumus oleh Vladimir Kruchinin di OEIS:
sumber
Sekam , 7 byte
Cobalah online!
Penjelasan
sumber
JavaScript (Node.js) , 43 byte
Cobalah online!
sumber
05AB1E , 10 byte
Cobalah online!
Penjelasan
sumber