Aufgabe

Gegeben 2 positive ganze Zahlen sind nund k, wobei der n > kAusgang die Anzahl von Surjektionen aus einem Satz von nunterscheidbaren Elementen in einen Satz von kunterscheidbaren Elementen.

Definition

Eine Funktion f: S → T heißt Surjektion, wenn für jedes t everyT s∈S gilt, so dass f (s) = t.

Beispiel

Wann n=3und k=2, ist die Ausgabe 6, da es 6Einwände von {1,2,3}bis gibt {1,2}:

1. 1↦1, 2↦1, 3↦2
2. 1↦1, 2↦2, 3↦1
3. 1↦1, 2↦2, 3↦2
4. 1↦2, 2↦1, 3↦1
5. 1↦2, 2↦1, 3↦2
6. 1↦2, 2↦2, 3↦1

Testfälle

n k output
5 3 150
8 4 40824
9 8 1451520

Referenz

• OEIS A019538

Wertung

Das ist Code-Golf . Kürzeste Antwort in Bytes gewinnt.

Es gelten Standardlücken .

Gelee , 5 4 Bytes

ṗṬML

Dies ist eine O (k ⁿ ) Brute-Force-Lösung.

Probieren Sie es online!

Wie es funktioniert

ṗṬML  Main link. Left argument: k. Right argument: n.

ṗ     Cartesian power; yield the list of all n-tuples over {1, ..., k}.
      Each tuple represents a (not necessarily surjective) function from
      {1, ..., n} to {1, ..., k}.
 Ṭ    Apply the "untruth" atom to each tuple.
      Ṭ maps a list of indices to an array with 1's at those indices, and exactly
      as many zeroes as needed to build the array.
      Examples:
           [1, 2, 3, 3, 3] -> [1, 1, 1]
           [1, 3, 5]       -> [1, 0, 1, 0, 1]
           [2, 6, 2, 4, 4] -> [0, 1, 0, 1, 0, 1]
  M   Yield all indices of maximal elements, i.e., all indices of [1] * k.
   L  Take the length.

Haskell , 48 Bytes

s(_,1)=1
s(1,_)=0
s(m,n)=n*(s(m-1,n-1)+s(m-1,n))

Probieren Sie es online!

Warum zählt der Widerspruch s(m,n)=n*s(m-1,n-1)+n*s(m-1,n)?

Um nBilder zu sammeln , kann ich entweder

• Drücke eine Singleton- [m]Kreation in eine der nGrenzen, die n-1Gruppen umgeben
• oder fügen Sie meine neue min eine der nbereits vorhandenen Gruppen von[1..m-1]

Haskell , 38 Bytes

m#n|n<2=1|m<2=0|o<-m-1=n*(o#(n-1)+o#n)

Probieren Sie es online!

Mager , 66 Bytes

def s:_->nat->nat|(m+1)(n+1):=(n+1)*(s m n+s m(n+1))|0 0:=1|_ _:=0

Probieren Sie es online!

Beweis der Richtigkeit

Probieren Sie es online!

Erläuterung

Lassen Sie uns die Funktion entgolfen:

def s : nat->nat->nat
| (m+1) (n+1) := (n+1)*(s m n + s m (n+1))
| 0     0     := 1
| _     _     := 0

Die Funktion wird durch Mustervergleich und Rekursion definiert, die beide eine integrierte Unterstützung haben.

Wir definieren s(m+1, n+1) = (n+1) * (s(m, n) + s(m, n+1)und s(0, 0) = 1, was offen lässt s(m+1, 0)und was s(0, n+1)beide als 0der letzte Fall definiert sind.

Lean verwendet, so wie es s m nist, die Lamdba-Kalkülsyntax s(m, n).

Nun zum Beweis der Richtigkeit: Ich habe es auf zwei Arten ausgedrückt:

def correctness : ∀ m n, fin (s m n) ≃ { f : fin m → fin n // function.surjective f } :=
λ m, nat.rec_on m (λ n, nat.cases_on n s_zero_zero (λ n, s_zero_succ n)) $
λ m ih n, nat.cases_on n (s_succ_zero m) $ λ n,
calc fin (s (nat.succ m) (nat.succ n))
   ≃ (fin (n + 1) × (fin (s m n + s m (n + 1)))) :
  (fin_prod _ _).symm
... ≃ (fin (n + 1) × (fin (s m n) ⊕ fin (s m (n + 1)))) :
  equiv.prod_congr (equiv.refl _) (fin_sum _ _).symm
... ≃ (fin (n + 1) × ({f : fin m → fin n // function.surjective f} ⊕
         {f : fin m → fin (n + 1) // function.surjective f})) :
  equiv.prod_congr (equiv.refl _) (equiv.sum_congr (ih n) (ih (n + 1)))
... ≃ {f // function.surjective f} : s_aux m n

def correctness_2 (m n : nat) : s m n = fintype.card { f : fin m → fin n // function.surjective f } :=
by rw fintype.of_equiv_card (correctness m n); simp

Das erste ist, was wirklich vor sich geht: eine Trennung zwischen [0 ... s(m, n)-1]und die Auswüchse von [0 ... m-1]auf [0 ... n-1].

Das zweite ist, wie gewöhnlich gesagt wird, das s(m, n)ist die Kardinalität der Surjektionen von [0 ... m-1]auf [0 ... n-1].

Lean verwendet die Typentheorie als Grundlage (anstelle der Mengenlehre). In der Typentheorie hat jedes Objekt einen Typ, der ihm inhärent ist. natist die Art der natürlichen Zahlen, und die Aussage, dass 0es sich um eine natürliche Zahl handelt, wird ausgedrückt als 0 : nat. Wir sagen, das 0ist von Typ nat, und das nathat 0als Einwohner.

Sätze (Aussagen / Behauptungen) sind ebenfalls Typen: Ihr Bewohner ist ein Beweis für den Satz.

• def: Wir werden eine Definition einführen (weil eine Bijektion wirklich eine Funktion ist, nicht nur ein Satz).

• correctness: der Name der Definition

• ∀ m n: für jedes mund n(Lean gibt automatisch an, dass es sich um einen Typ handelt nat, und zwar aus folgendem Grund).

• fin (s m n)ist die Art der natürlichen Zahlen, die kleiner als ist s m n. Um einen Einwohner zu machen, liefert man eine natürliche Zahl und einen Beweis, dass sie kleiner ist als s m n.

• A ≃ B: bijection zwischen dem Typ Aund dem Typ B. Bijektion zu sagen ist irreführend, da man tatsächlich die Umkehrfunktion bereitstellen muss.

• { f : fin m → fin n // function.surjective f }die Art der Einwände von fin mbis fin n. Diese Syntax bildet einen Untertyp aus dem Typ fin m → fin n, dh der Art der Funktionen von fin mbis fin n. Die Syntax lautet { var : base type // proposition about var }.

• λ m: ∀ var, proposition / type involving varist wirklich eine Funktion, die varals Eingabe nimmt, also λ mdie Eingabe einführt. ∀ m n,ist Abkürzung für∀ m, ∀ n,

• nat.rec_on m: Rekursion machen auf m. Um etwas zu definieren m, definieren Sie das Ding für 0und geben Sie das Ding für k, bauen Sie das Ding für k+1. Man würde bemerken, dass dies der Induktion ähnlich ist, und dies ist in der Tat ein Ergebnis der Church-Howard-Korrespondenz . Die Syntax lautet 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").

Heh, das wird lang und ich bin nur in der dritten Zeile von correctness...

J , 19 Bytes

-/@(^~*]!0{])],i.@-

Probieren Sie es online!

Erläuterung

-/@(^~*]!0{])],i.@-  Input: n (LHS), k (RHS)
                  -  Negate k
               i.@   Range [k-1, k-2, ..., 0]
             ]       Get RHS
              ,      Join, forms [k, k-1, ..., 0]
   (        )        Dyad between n (LHS), [k, k-1, ..., 0] (RHS)
           ]           Get RHS
         0{            Select value at index 0
       ]               Get RHS
        !              Binomial coefficient
    ^~                 Raise each in RHS to power of n
      *                Multiply
-/@                  Reduce from right to left using subtraction (forms alternating sum)

R , 49 Bytes

function(n,k,j=0:k)((-1)^(k-j)*j^n)%*%choose(k,j)

Probieren Sie es online!

Implementiert eine der Formeln von Mario Catalani:

T(n, k) = Sum_{j=0..k} (-1)^(k-j)*j^n*binomial(k, j)

oder alternativ:

T(n, k) = Sum_{j=0..k} (-1)^j*binomial(k, j)*(k-j)^n

das ergibt die gleiche Byteanzahl in R.

Python 2 , 56 53 50 Bytes

f=lambda n,k:n/k and(1/k or f(n-1,k-1)+f(n-1,k))*k

Probieren Sie es online!

-3 Bytes dank H.PWiz.

-3 Bytes dank Dennis.

• Wenn n<knicht alle kabgebildet werden können, gibt es keine Einwände. n/k andkümmert sich darum.
• Das Nehmen f(0,0)=1gibt uns den einzigen Grundfall ungleich Null, den wir brauchen. 1/k orerreicht dies.

Ruby , 46 Bytes

f=->n,k{k>n ?0:k+n<1?1:k*(f[n-=1,k]+f[n,k-1])}

Probieren Sie es online!

Standardrekursiver Ansatz ...

Brain-Flak , 142 Bytes

({}<({}()){({}[(())]<<>{({}({})<>)<>}{}>)}{}>)<>{<>(({}<>)<{({}[()]<([])({([{}]()({}))([{}]({}))}{}[{}])>)}{}({}<>)>)<>}<>{}{}{({}<>[{}])<>}<>

Probieren Sie es online!

Dies verwendet die Standard-Einschluss- / Ausschlussformel.

Ich kann derzeit keine vollständige Erklärung verfassen, aber hier eine allgemeine Erklärung:

# Compute k-th row of Pascal's triangle
({}<({}()){({}[(())]<<>{({}({})<>)<>}{}>)}{}>)<>

# Multiply each element by n^j (and reverse to other stack)
{<>(({}<>)<{({}[()]<([])({([{}]()({}))([{}]({}))}{}[{}])>)}{}({}<>)>)<>}

# Compute alternating sum
<>{}{}{({}<>[{}])<>}<>

Pari / GP , 38 Bytes

(n,k)->Pol(exp(x+O(x^n))-1)^k*n!\x^n%x

Probieren Sie es online!

Mit der Formel von Vladimir Kruchinin auf OEIS:

E.g.f.: (exp(x)-1)^k = sum T(n,k)x^n/n!

Schale , 7 Bytes

#`¦ḣ¹π²

Probieren Sie es online!

Erläuterung

#`¦ḣ¹π²  Inputs: n (²), implicit k (¹)
     π²  Cartesian power of [1..k] to n
#        Count if:
   ḣ¹      Range [1..k]
 `¦        Is a subset

JavaScript (Node.js) , 43 Byte

T=(n,k)=>n<k?0:k+n<1||k*(T(--n,k)+T(n,k-1))

Probieren Sie es online!

05AB1E , 10 Bytes

sLsãʒêgQ}g

Probieren Sie es online!

Erläuterung

sLsã       # Cartesian product of range(k) repeated n times
    ʒ   }  # Filter by ...
     êgQ   # Connected uniquified length == k  (every item in range(k) appears at least once)
         g # Count