This is a spinoff of my attempt to capture the notion of 'explicit bijection' at https://mathoverflow.net/a/323827.

I wonder whether it is possible to formalize the idea that an algorithm computing a map $f:A\to B$ between two finite sets does not 'know' or 'use' a description of $B$.

Let me give two examples to illustrate what I mean. Let $A$ be the set of binary words of length $n$.

For the first example, let $f$ be the map corresponding to the following algorithm:

- let $w=w_1\dots w_n$ be the binary word
- let $i=1$
- for $l$ in $w$, reading the word left to right:
- if $l=1$ increase $i$ by one
- otherwise write down $i$, and set $i=1$

- write down $i$.

That is, the word $1$ is mapped to $2$ and the word $0$ is mapped to $1,1$. In general, this algorithm associates (bijectively) to each binary word of length $n$ a composition of $n+1$. So $B$ is the set of integer compositions of $n+1$, but it seems (to me) that the algorithm does not use this fact.

For the second example, let $f$ be the map corresponding to the following algorithm:

- let $w=w_1\dots w_n$ be the binary word
- let $k=\sum_{i=1}^n 10^{(n-i)w_i}$
- sort the integer compositions of $n+1$ into lexicographic order and write down the $k$-th.

It is not hard to see that the two maps coincide. However, I would (like to) say that the second algorithm uses the fact that $B$ is the set of integer compositions of $n+1$.