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

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.

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.

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

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?

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.

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.

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.

For instance, a deep embedding of untyped λ-calculus.

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

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.

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!

You definitely need some deep embedding of your computational model to compute Kolmogorov complexitity.

Beware that the library linked develops what they call *synthetic computability*, i.e. they cannot prove internally that what they do is computable.

They rely on the metatheoretical property that all CIC functions are computable instead.

I don't know whether it's possible to develop a synthetic version of Kolmogorov complexity, but naturally I'd doubt it.

Because CIC functions are quotiented by too many equational rules, you have to be wary when extracting intensional content.

For instance, CIC is incompatible with a strong form of continuity (https://www.cs.bham.ac.uk/~mhe/papers/escardo-xu-inconsistency-continuity.pdf)

@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.

Nope, because you'd need a proof that the internal term reflects the external term, and that'd still be an external property.

In particular, as soon as you go higher-order you'd need some form of parametricity.

@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.

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.

Depends what you exactly mean... everything function written in Coq (without axioms) can be executed, indeed.

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

(and vice versa)

Last updated: Jan 29 2023 at 01:02 UTC