advancedresearch
Specify the path semantics more clearly
It is clear what is f[g] = h or f[g_0 × g_1 → g_n] = h, but what are [:] and [g] x?
By the way, using the concatenative algebra (semantics) the first two expressions can be written as
f g = g,g h
f g_n = g_0,g_1 h
This way the symmetry also becomes more visible.
Where was it unclear? The tutorial?
[g] x is a sub-type, e.g. y : [g] x can be written g(y) = x.
[:] true is a sub-type of a type, e.g. bool : [:] true which is equal to bool : [true] true which can be written true(bool) = true. This is an atomic function (it is defined for only one value).
and [:] means a sub-type of the type declaration bool x bool -> bool, which defines some output for some input.
f[g] = h can also be written f : [[g]] h. See https://github.com/advancedresearch/path_semantics/blob/master/papers-wip/paths-as-function-sub-types.pdf
Thanks.
true(bool) = true
Are true on the left and true on the right the same?
Yes, they are the same. true returns itself, but only if the argument is bool.
What does true return if the argument is not bool ?? That should be clarified.
@pcarbonn That's a good question! true does not return if the argument is not bool.
However, this has never been expressed anywhere in path semantics as far as I know, but something similar has been expressed for normal functions in the definition of the existential path (codomain). There is no analogue of the existential path for atomic functions yet, but now we might need to introduce one.
@pcarbonn I have been thinking about this today and this is how far I got:
In general, it is undecidable problem. This is because an existential path requires a type. It can not give you an answer if the input is without context. I think this is a very important insight, so thanks for pointing this out.
Luckily, it is not an undecidable problem in all type systems.
In cumulative type hierarchies, all types, such as bool or nat, has the type type_0, which is often just written type. The type_0 has the type type_1, and so on, such that type_n has type type_n+1. In these systems, one can "lift" the existential path up, such that it has the type:
∃true : type -> bool
(∃true)(bool) = true
(∃true)(_) = false
This will return true for bool and false for other types.
In general for the cumulative type hierarchy:
∃type_n : type_n+2 -> bool
(∃type_n)(type_n+1) = true
(∃type_n)(_) = false