Competing versions and consensus

[kabirkbr]

Ben 17/02/2021 / Slack

A new grounded type T would need to be associated w/ some procedure F_T for validating whether some entity E is an instance of type T. The question is then what is the process for validating that a new procedure F1_T is equivalent to F_T, i.e. is also a correct validator for checking that E is an instance of T. This ultimately would need some decentralized consensus mechanism -- like, if there is a population of 10000 theorem-prover nodes, then 10 could be randomly selected to check whether F1 T is provably equivalent to F_T . If F1_T passes this decentralized check then it is entered into the blockchain that F1_T works for validating type T as well.

[kabirkbr]

[kabirkbr]

Ben, 17/02/2021 / Slack:

This decentralized proof mechanism could leverage ProofGold https://proofgold.org/ which is the latest improvement of Qeditas. https://qeditas.org/.

[...] Proofgold is the project of Chad Brown who is a grad student of Josef Urban, who is Zar's PhD supervisor ... [...] So anyway I think decentralized mechanisms for dealing w/ grounded types and their groundings are possible, though we don't need to implement them in this iteration... [...]

[kabirkbr]

Alexey, 17/02/2021 / Slack:

I don’t see how it can work in practice. Apparently, it can work in some cases, e.g. a jpeg-file has a certain format, and an attempt to decode it can lead to success or failure, so the decoder can be the validator of JPEGType. However, in such cases, the file/data structure can be described in dependent types directly, and it may be more efficient than achieving consensus for the validators provable equivalence (and if the validator code should be available for proving equivalence, what restrictions will it implementation have?). In other cases, it’s not a matter of data format, but data interpretation. How can we validate that some sequence of bytes is an OCT or MRT image? How can we validate that it is a character string or just a binary string?

[kabirkbr]

Ben, 17/02/2021 / Slack:

"How can we validate that it is a character string or just a binary string?"

==> There would have to be some set of agreed-upon encodings for character strings as bit strings. Each encoding agreed-on for this purpose would be referenced in the blockchain (i.e. the hashcode of the location of the description of the encoding would be stored in the blockchain). To add a new encoding to the list of agreed-on encodings for character strings as bit strings, would be a democratic governance actions. If x% of network members sign a petition to have encoding Z added to the list, then a vote gets done, and if y% vote yes then encoding Z is added to the list (as memorialized in the blockchain).

"if the validator code should be available for proving equivalence, what restrictions will it implementation have?"

==> For Proofgold see https://proofgold.org/ihol.html for a sketch, there is also a technical paper on the site

[kabirkbr]

Alexey, 17/02/2021 / Slack:

i.e. the hashcode of the location of the description of the encoding

yeah, so that’s what I meant - that type providers should refer to globally accessible groundings; this somewhat contradicts to no.1 and 2 (extendability and competing version requirements), or at least needs some clarifications.

[kabirkbr]

Kabir 17/02/2021 / Slack:

type providers should refer to globally accessible groundings

if i understand correctly what you mean by 'globally accessible groundings', can we think of some sort of middle way -- where we have a small subset of grounded types (something like hardcoded 'string', 'number', 'bool' of Idris, but allow all there rest to be defined in a decentralized manner if they are based on that?

[ ... e.g. if i remember correctly ...] OpenCog uses externally stored NN models to ground inferences within Atomspace or something into that direction... Suppose we put these models on SNet. Would we call them grounded / reflecting real-world semantics? How would we type-describe them in a formally verifiable way?

[kabirkbr]

Alexey, 17/02/2021 Slack:

If we have built-in grounded types and define new types using dependent types formalism without FFIs then there should be no big problem as I mentioned, yes (of course, we will not be able to prove that a certain service always returns valid type members). And it is not a problem to treat services as type providers, I guess. In this case, using a type will mean calling a service. My concern was about introducing really new potentially conflicting types as elements of common ontology. But there are different ways to avoid this. We just need to describe this more carefully on concrete examples. Otherwise, the requirements can be interpreted differently….

[kabirkbr]

Kabir, 17/02/2021 Slack:

Actually, I would allow [economics] to solve that. In the sense, that if the tokenomic mechanism of SNet works well, then all service providers should be interested to make their services accessible and usable by others. It is a good idea to facilitate and incentive that.

But there may be some which will build a workflow of their own services some of which use exotic /novel types or all kind of stuff that ontology builders did not take into account. I do not think that it is a good idea to restrict or systemically de-incentivize them (after all, singularity should come from fast (very) innovation, right :wink:?)

And any automated matching done using AI-DSL involving OGG would have a warning attached in that the AI-DSL infrastructure doesn't have a reliable way to check if a file is actually OGG

something like that, yeah. (edited)

[kabirkbr]

Alexey 17/02/2021 Slack:

it may not be a huge issue if we consider only local types within service namespaces (i.e. each novel type constructor is wrapped into service type constructor ~ MyService getSizeT, or something like that). Then, getSizeT can be defined locally ~

getSizeT = foreign FFI_URI "sizeof_size_t uri" (IO Int)

and then if another service wants to use this type, it will either refer to MyService getSizeT, or use its own similar definition and then the equivalence of these definitions can be verified. I wouldn’t call this “multiple versions of ontology”, though. And also, if we want to unwrap some type from concrete service, then we indeed will need some global consensus on it.

[kabirkbr]

Ben 17/02/2021 Slack:

"if i understand correctly what you mean by 'globally accessible groundings', can we think of some sort of middle way -- where we have a small subset of grounded types (something like hardcoded 'string', 'number', 'bool' of Idris, but allow all there rest to be defined in a decentralized manner if they are based on that?"

==> yes

As for the "soft matching" aspect you mention, it makes sense though I hadn't been considering it in this context.

For instance, whether a sound file has .mp4 format is crisp. Whether a sound file contains pop music is fuzzy and to be softly matched.

But we could have some AI algo that is good at sound-splitting for pop music and not for opera, and to match a sound file w/ that algo one would want to soft-evaluate how much that sound file meets the criterion of "pop. music"