Restricted Species

Type Constructor

Usage

import from Integer;
CharacteristicSpecies(n: Integer)(L: LabelType):
CombinatorialSpecies L == RestrictedSpecies (List, n)(L) add;

Description

A species constructor to restrict a given species.

According to [BLL98, p. 30], each species F gives rise canonically to an enumerable family (F_n)_n≥0 of species defined by setting for each n ∈ ℕ,

{
F[U], if cardU = n,
Fn[U] = ∅, otherwise.

(13)

The species F_n is said to be the species F restricted to n .

The constructor RestrictedSpecies takes a species F and a natural number n and constructs a species G that is concentrated on the cardinality n, i. e., G_k[U] = ∅ for kn and any set U. In other words RestrictedSpecies constructs F_n from F.

127⟨dom: RestrictedSpecies 127⟩≡   (55)
RestrictedSpecies(
    F: SPECIES,
    n: Integer
)(L: LabelType): CombinatorialSpecies L == F L add {
        Rep == F L;
        nn: I == machine n;
        import from Rep;
        ⟨implementation: RestrictedSpecies 128a⟩
}

Defines:
RestrictedSpecies, used in chunks 129b, 640, and 655.

Uses CombinatorialSpecies 71, I 47, Integer 66, LabelType 62, and SPECIES 55.

128a⟨implementation: RestrictedSpecies 128a⟩≡ (127) 128b ⊳
structures(s: SetSpecies L): Generator % == generate {
if #s = nn then for r in structures(s)$Rep repeat yield per r;
}

Uses Generator 617 and SetSpecies 117.

128b⟨implementation: RestrictedSpecies 128a⟩+≡ (127) ⊲128a 128c ⊳
isomorphismTypes(s: SetSpecies L): Generator % == generate {
if #s = nn then for r in isomorphismTypes(s)$Rep repeat yield per r;
}

Uses Generator 617 and SetSpecies 117.

128d⟨implementation: RestrictedSpecies 128a⟩+≡ (127) ⊲128c 129a ⊳
isomorphismTypeGeneratingSeries: OrdinaryGeneratingSeries == {
term(coefficient(isomorphismTypeGeneratingSeries$F(L), nn), nn);
}

Uses OrdinaryGeneratingSeries 311.

129b⟨implementation: RestrictedSpecies 128a⟩+≡ (127) ⊲129a
import from String, Symbol, List SpeciesExpression;
expression: SpeciesExpression == apply(- "RestrictedSpecies",
[expression$F(L), leaf n]);

Uses RestrictedSpecies 127, SpeciesExpression 430, and String 65.

8.6 Restricted Species