Rafael Garcia Leiva (Aug 09 2020 at 17:54): Rafael Garcia Leiva (Aug 09 2020 at 17:54):Hi, given
Require Import String.
Definition f1 := fun n : nat => n + 1.
I know how to print the length of a string with:
Compute length "hello"%string.
and how to print a string with the definition of a function:
Print f1.
but I cannot figure out how to compute the length of a definition. I have tried:
Compute length (Print f1)%string.
But it does not work. Any help will be greatly appreciated. Thanks
Yannick Zakowski (Aug 09 2020 at 18:20):Hi Rafael. I think you are misunderstanding a bit the nature of the objects being manipulated.
When you write
Definition f1 := fun n : nat => n + 1.
You are defining a term in the Gallina language, which is a statically typed purely functional language with a (very) fancy type system. You may find its documentation here: https://coq.github.io/doc/v8.12/refman/language/core/index.html
Similarly, the function length, which fully qualified is Coq.Strings.String.length is a function in this language whose type is string -> nat, i.e. that can only be applied to a term of type string such as "hello".
In contrast, Compute and Print are completely different: they are not part of the Gallina language but instead is what is called a "Vernacular command". They are meta object if you will.
As such, when you write Compute length "hello", it should really be understood as running the Vernacular command "Compute" on the Gallina term length "hello". This makes sense, because length "hello" is well-typed.
But Print f1, running the Vernacular command "Print" on the Gallina term f1 displays a message indeed, but does not produce a "Gallina" string. As such, it makes no sense to try to run length (Print f1).
If you want to compute the "length" of an object, you need to define a Gallina function that converts elements of this type to a nat according to some interpretation of length that you chose, very much in the way the Coq.Strings.String.length does for elements of type string. But it is not possible to do this universally inside of Gallina (or to be more precise, something doing it polymorphically would be a constant function).
Hope it helps.
Rafael Garcia Leiva (Aug 09 2020 at 18:41):Yannick Zakowski said:
Many thanks for your help! Now it is clear I cannot mix this Gallina and Vernacular commands.
But it is not possible to do this universally inside of Gallina (or to be more precise, something doing it polymorphically would be a constant function).
Is that a theorem? That is, is it impossible to know the length of an arbitrary expression in lambda calculus? Or is it a limitation of Coq?
I am more familiar with defining functions using Turing machines, and computing the length of a Turing machine is a very common operation. I was wondering if in Coq you can do the same.
Thanks for your help.
Yannick Zakowski (Aug 09 2020 at 18:49):Is that a theorem? That is, is it impossible to know the length of an arbitrary expression in lambda calculus? Or is it a limitation of Coq?
It is a theorem, related to what is called "parametricity". Intuitively, polymorphic functions are extremely constraint in what they can do because they must perform without being able to introspect their argument. The following famous paper by Philip Wadler introduces the concept very clearly: https://people.mpi-sws.org/~dreyer/tor/papers/wadler.pdf
Yannick Zakowski (Aug 09 2020 at 18:51):I haven't worked with Turing machines in a long time, but I would say that intuitively indeed computational models based on variations of the lambda calculus are much less prone to introspection than Turing Machine. Someone more qualified than myself may have a more principal remark on the matter?
Rafael Garcia Leiva (Aug 09 2020 at 19:00):Yannick Zakowski said:
It is a theorem, related to what is called "parametricity". Intuitively, polymorphic functions are extremely constraint in what they can do because they must perform without being able to introspect their argument. The following famous paper by Philip Wadler introduces the concept very clearly: https://people.mpi-sws.org/~dreyer/tor/papers/wadler.pdf
Many thanks for the reference. I'll try to read the paper!
Anyway, I am only interested in computing the length of functions from nat to nat. Maybe that helps.
Pierre-Marie Pédrot (Aug 09 2020 at 19:24):Anyway, I am only interested in computing the length of functions from nat to nat. Maybe that helps.
What does that even mean? A function in axiom-free CIC is a black box, the only thing you know what to do with is internally to apply it.
Pierre-Marie Pédrot (Aug 09 2020 at 19:25):Maybe you could give a bit of context of why you want to do this. If you're trying to do computability, you need to pick a more intensional representation for computable functions.
Pierre-Marie Pédrot (Aug 09 2020 at 19:26):For instance, a deep embedding of untyped λ-calculus.
Karl Palmskog (Aug 09 2020 at 19:30):for the record, lots of computability theory (including encoding of Turing machines in Gallina) has been done in Coq here: https://github.com/uds-psl/coq-library-undecidability
Rafael Garcia Leiva (Aug 09 2020 at 19:32):Pierre-Marie Pédrot said:
Maybe you could give a bit of context of why you want to do this. If you're trying to do computability, you need to pick a more intensional representation for computable functions.
Many thanks for the interest. I am trying to approximate the concept of Kolmogorov complexity of an arbitrary string. Assuming a string s encoded as a natural number n, and a function f that given as input m produces n, that is, f(m) = n, I would like to know the length of the definition of 'f' as an approximation of the Kolmogorov complexity of n. Then, I will compute the length of a compressed version (using a standard compressor) of the definition of 'f' as a way to assess the quality of the approximation.
Best regards.
Rafael Garcia Leiva (Aug 09 2020 at 19:33):Karl Palmskog said:
for the record, lots of computability theory (including encoding of Turing machines in Gallina) has been done in Coq here: https://github.com/uds-psl/coq-library-undecidability
Cool! Thanls!
Pierre-Marie Pédrot (Aug 09 2020 at 20:13):You definitely need some deep embedding of your computational model to compute Kolmogorov complexitity.
Pierre-Marie Pédrot (Aug 09 2020 at 20:14):Beware that the library linked develops what they call synthetic computability, i.e. they cannot prove internally that what they do is computable.
Pierre-Marie Pédrot (Aug 09 2020 at 20:14):They rely on the metatheoretical property that all CIC functions are computable instead.
Pierre-Marie Pédrot (Aug 09 2020 at 20:15):I don't know whether it's possible to develop a synthetic version of Kolmogorov complexity, but naturally I'd doubt it.
Pierre-Marie Pédrot (Aug 09 2020 at 20:16):Because CIC functions are quotiented by too many equational rules, you have to be wary when extracting intensional content.
Pierre-Marie Pédrot (Aug 09 2020 at 20:17):For instance, CIC is incompatible with a strong form of continuity (https://www.cs.bham.ac.uk/~mhe/papers/escardo-xu-inconsistency-continuity.pdf)
Karl Palmskog (Aug 09 2020 at 20:23):@Pierre-Marie Pédrot but then couldn't one "lift" the synthetic computability results in MetaCoq? For example, if one proved all MetaCoq-pCUIC functions are computable (I guess this hasn't been done), then just apply that theorem to all the stuff in the library.
Pierre-Marie Pédrot (Aug 09 2020 at 20:28):Nope, because you'd need a proof that the internal term reflects the external term, and that'd still be an external property.
Pierre-Marie Pédrot (Aug 09 2020 at 20:29):In particular, as soon as you go higher-order you'd need some form of parametricity.
Paolo Giarrusso (Aug 10 2020 at 00:59):@Rafael Garcia Leiva > Anyway, I am only interested in computing the length of functions from nat to nat. Maybe that helps.
Then at least lambda calculus and Turing machines are equally expressive. At higher order, that breaks down (despite Church-Turing), exactly because of what @Yannick Zakowski points out: in lambda calculi you cannot introspect the code a function argument, unlike with Turing-machines. And that's why the "length" of a function argument becomes uncomputable.
Rafael Garcia Leiva (Aug 10 2020 at 13:03):Paolo Giarrusso said:
Rafael Garcia Leiva > Anyway, I am only interested in computing the length of functions from nat to nat. Maybe that helps.
Then at least lambda calculus and Turing machines are equally expressive. At higher order, that breaks down (despite Church-Turing), exactly because of what Yannick Zakowski points out: in lambda calculi you cannot introspect the code a function argument, unlike with Turing-machines. And that's why the "length" of a function argument becomes uncomputable.
Thanks for the answer.
I am assuming that every function that you define with lambda calculus is computable. Is it still the case at the higher order implemented by Coq? Thanks.
Paolo Giarrusso (Aug 11 2020 at 03:46):Depends what you exactly mean... everything function written in Coq (without axioms) can be executed, indeed.
Paolo Giarrusso (Aug 11 2020 at 08:18):But not every higher-order problem that can be solved by a Coq program can be solved by a TM, IIUC: https://cstheory.stackexchange.com/a/1118/989
Paolo Giarrusso (Aug 11 2020 at 08:18):(and vice versa)
Last updated: Oct 13 2024 at 01:02 UTC