Email Gateway (Aug 22 2022 at 20:31): Email Gateway (Aug 22 2022 at 20:31):From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
Hello,
Given a function f::’a=>’b, I would like to express that f is computable, i.e., there exists an algorithm which computes f. Is there any reference to something like computable::(‘a=>’b)=>bool in Isabelle/HOL?
Kind Regards,
José M.
Email Gateway (Aug 22 2022 at 20:31):From: Alexander Krauss <krauss@in.tum.de>
Dear José,
Given a function f::’a=>’b, I would like to express that f is computable, i.e., there exists an algorithm which computes f. Is there any reference to something like computable::(‘a=>’b)=>bool in Isabelle/HOL?
AFAIK, there is no well-established standard definition. However, there
is some material in the AFP that treats the concept of computablility,
e.g. the entry "Universal_Turing_Machine", which defines a notion of
computability.
In general, for concrete data types 'a, and 'b, one can define a model
of computation such as recursive functions or turing machines and obtain
a notion of computability. However, this is not immediately clear for
arbitrary polymorphic 'a and 'b, since one at least has to say how to
map these types into whatever the model of computation uses as its
input/output language. This mapping may not exist for arbitrary types
such as function types. So a general notion of computability must be
based on some notion of a type being finitely encodable (e.g., via some
type class).
Here, Isabelle/HOL differs notably from constructive type theories,
where "function = executable function = program" unless you go into "Prop".
Alex
Email Gateway (Aug 22 2022 at 20:31):From: Lawrence Paulson <lp15@cam.ac.uk>
Please allow me to advertise the AFP entry HereditarilyFinite (defining hf, the type of hereditarily finite sets). Therein is defined the type class finitary, consisting of all types that can be injected into hf. And hf can be put into bijection with the set of natural numbers. So given the notion of computability for the natural numbers, you can quickly obtain computability for all those other types.
Larry
Email Gateway (Aug 22 2022 at 20:31):From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
Thank you for the suggestions.
Kind Regards,
José M.
Sent from my iPhone
Last updated: May 07 2024 at 01:07 UTC