# Tag Info

You can show $|L|^i$ is a tight upper bound by using the following language: $L = \{ ab,aab,aaab,\ldots,a^kb \mid k \geq 1 \}.$ Any concatenation gives a new string. For a lower bound, I can suggest the following unary language: $U = \{a,aa,aaa,\ldots,a^k \mid k \geq 1 \}$. Then, $U^i = \{ a^i,a^{i+1},\ldots,a^{ki} \}$ and so $|U^i| = i|U|-... 8 I know it can be done 'elegantly' in a dependently typed system. But, from a classical point of view, the resulting definitions seem extremely alien. Can you explain what you mean by "alien"? It seems to me that you formalize the concept of finite set in precisely the same way in type theory and in set theory. In set theory, you proceed by defining the ... 5 If$L$is any finite code (that is, if$L^*$is a free monoid of basis$L$), then$|L^i| = |L|^i$. This is the case in particular if$L$is a prefix code: no word of$L$is a proper prefix of another word of$L$. The lower bound is$i|L| - i$(a slight improvement over the suggested$i|L| - i + 1$). It is obtained for$L = \{1, a, a^2, \ldots, a^{k-1}\}$. ... 5 Let me see if I can add anything useful to Neel's answer. The "design space" for finite sets is much larger constructively that it is classically because various definitions of "finite" need not agree constructively. Various definitions in type theory give slightly different concepts. Here are some possibilities. Kuratowski finite sets ($K$-finite) can be ... 4 When$p^q>3k$, then there is an easy randomized algorithm for this problem (with error probability zero and polynomial expected running time). The algorithm prints "IMPOSSIBLE" if there is$i$such that$B|w_i$has more than$n-|w_i|$rows that consist entirely of zeroes. Otherwise, the algorithm prints "POSSIBLE". It then chooses uniformly random ... 2 One reason for this is that one can first define a cryptosystem having a small finite message space, and then on top of that, construct another cryptosystem that can handle longer message spaces. This is a very reasonable modular design methodology. A couple of examples: given a block cipher with a finite message space, one can use a block cipher mode (... 1 We, of course, want our message space,$\mathcal{M}\$, to be able to include messages of arbitrary size. I am not familiar with the details of Stinson's definition of a cryptosystem, but I would not be surprised if it is set up to be scaleable, iterable, or chainable using other constructions. Your concern is warranted, but there are a couple of things to ...