21 Nov
2010
21 Nov
'10
10 p.m.
On 21/11/2010 8:33 PM, wren ng thornton wrote:
On 11/20/10 6:33 AM, Ketil Malde wrote:
I guess this makes [X] an exponential type, although I don't remember seeing that term :-)
Nope. (a->b) is the exponential type, namely |a->b| = |b|^|a|.
[_] is just a solution to the recursive equation [x] = 1 + x*[x].
So that [X] correspond to the 'type' 1/(1-X). This is sometimes called the 'asterate' in other contexts, since it corresponds to the Kleene star. The nice thing about the 'asterate' is that it exists for many many semi-rings -- and one can use it as a replacement for both 'minus' and 'exact division' in the Gaussian Elimination algorithm. Jacques