资 源 简 介
A Scala package providing bijective Goedel numberings (ranking/unranking bijections to N) for members of a Term Algebra with an infinite supply of variables and functions symbols.
The algorithms, using a generalized Cantor bijection between N and N^k (known to be polynomial in size of the representations) ensure that:
a unique syntactically valid term is associated to each natural number
a unique natural number is associated to each syntactically valid term
either way, the bitsize of the representation of the output is proportional (up to a small constant) to the bitsize of the representation of the output
For instance, terms like:
F3(v3,F2(v2,F1(v1,v0,F1),F2),F3)
F3(v3,F2(v2,F1(v1,v0,v0),F1(v1,v0,v0)),F2(v2,F1(v1,v0,v0),F1(v1,v0,v0)))
are uniquely associated to Goedel numbers like
1166589096937670191 and
781830310066286008864372141041
of comparable representation size.
