задача
Дано 2 натуральных числа n
и k
, где n > k
, выведите количество сюрпризов из набора n
различимых элементов в набор k
различимых элементов.
Определение
Функция f: S → T называется сюръекцией, если для каждого t∈T существует s∈S, такое что f (s) = t.
пример
Когда n=3
и k=2
, вывод 6
, так как есть 6
сюрпризы от {1,2,3}
до {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
Ссылка
счет
Это код-гольф . Кратчайший ответ в байтах побеждает.
Применяются стандартные лазейки .
code-golf
arithmetic
set-theory
Пропитанная монахиня
источник
источник
Ответы:
Желе ,
54 байтаЭто решение для грубой силы O (k n ) .
Попробуйте онлайн!
Как это устроено
источник
Haskell , 48 байтов
Попробуйте онлайн!
Почему подсчет сюрпризов
s(m,n)=n*s(m-1,n-1)+n*s(m-1,n)
?для того, чтобы собирать
n
изображения, я могу либо[m]
творение в любую изn
границ окружающихn-1
группm
в любую изn
уже существующих групп[1..m-1]
Haskell , 38 байт
Попробуйте онлайн!
источник
Lean , 66 байт
Попробуйте онлайн!
Доказательство правильности
Попробуйте онлайн!
объяснение
Давайте раскроем функцию:
Функция определяется сопоставлением с образцом и рекурсией, оба из которых имеют встроенную поддержку.
Мы определяем
s(m+1, n+1) = (n+1) * (s(m, n) + s(m, n+1)
иs(0, 0) = 1
, который оставляет открытым,s(m+1, 0)
иs(0, n+1)
, оба из которых определены0
в последнем случае.Постные использует синтаксис lamdba исчисления, так
s m n
этоs(m, n)
.Теперь доказательство правильности: я сформулировал это двумя способами:
Первый - это то, что на самом деле происходит: биекция между
[0 ... s(m, n)-1]
и наложения[0 ... m-1]
на[0 ... n-1]
.Второй, как обычно говорят, это
s(m, n)
кардинальность выводов[0 ... m-1]
на[0 ... n-1]
.Lean использует теорию типов в качестве своей основы (вместо теории множеств). В теории типов каждый объект имеет свойственный ему тип.
nat
тип натуральных чисел, а утверждение, которое0
является натуральным числом, выражается как0 : nat
. Мы говорим , что0
это типаnat
, иnat
имеет0
как житель.Предложения (утверждения / утверждения) также являются типами: их обитатель является доказательством предложения.
def
Мы собираемся ввести определение (потому что биекция - это действительно функция, а не просто суждение).correctness
: название определения∀ m n
: для каждогоm
иn
(Lean автоматически делает вывод, что их типnat
, из-за того, что следует).fin (s m n)
это тип натуральных чисел, который меньше, чемs m n
. Чтобы сделать обитателя, нужно предоставить натуральное число и доказательство того, что оно меньше, чемs m n
.A ≃ B
: биекция между типомA
и типомB
. Сказать, что биекция вводит в заблуждение, поскольку на самом деле нужно предоставить обратную функцию.{ f : fin m → fin n // function.surjective f }
тип сюрпризов отfin m
доfin n
. Этот синтаксис создает подтип из типаfin m → fin n
, то есть типа функций изfin m
вfin n
. Синтаксис есть{ var : base type // proposition about var }
.λ m
:∀ var, proposition / type involving var
действительно функция, которая принимаетvar
в качестве входных данных, поэтомуλ m
вводит ввод.∀ m n,
это сокращение для∀ m, ∀ n,
nat.rec_on m
: сделать рекурсию наm
. Чтобы определить что-то дляm
, определите вещь для,0
а затем с учетом вещиk
, построить вещь дляk+1
. Можно заметить, что это похоже на индукцию, и на самом деле это результат переписки Чёрча-Говарда . Синтаксис естьnat.rec_on var (thing when var is 0) (for all k, given "thing when k is k", build thing when var is "k+1")
.Хех, это становится длинным, и я только на третьей линии
correctness
...источник
J , 19 байт
Попробуйте онлайн!
объяснение
источник
-/@(^~*]!0{])]-i.
R , 49 байт
Попробуйте онлайн!
Реализует одну из формул Марио Каталани:
или поочередно:
что дает тот же счетчик байтов в R.
источник
Python 2 ,
56 5350 байтПопробуйте онлайн!
-3 байта благодаря H.PWiz.
-3 байта благодаря Деннису.
n<k
не всеk
можно отобразить, то нет никаких сюрпризов.n/k and
заботится об этом.f(0,0)=1
дает нам единственный ненулевой базовый случай, который нам нужен.1/k or
добивается этого.источник
Рубин , 46 байт
Попробуйте онлайн!
Стандартный рекурсивный подход ...
источник
Brain-Flak , 142 байта
Попробуйте онлайн!
При этом используется стандартная формула включения-исключения.
Я не могу написать полное объяснение в настоящее время, но вот объяснение высокого уровня:
источник
Пари / ГП , 38 байт
Попробуйте онлайн!
Используя формулу Владимира Кручинина на OEIS:
источник
Шелуха , 7 байт
Попробуйте онлайн!
объяснение
источник
JavaScript (Node.js) , 43 байта
Попробуйте онлайн!
источник
05AB1E , 10 байтов
Попробуйте онлайн!
объяснение
источник