Email Gateway (Aug 18 2022 at 15:44): Email Gateway (Aug 18 2022 at 15:44):From: li yongjian <lyj238@gmail.com>
Dear all:
By my understanding, the expressbilty of an inductive datatype and an
inductively defined set in Isabelle is not the same.
An inductive datatype can be naturally corresponding to an inductively
defined set, but not vice and versa.
Who could introduce more technical papers on the relation between the two
features.
Thanks in advance.
lyj
Email Gateway (Aug 18 2022 at 15:45):From: Lawrence Paulson <lp15@cam.ac.uk>
The point of your question is not clear to me. Certainly an algebraic data type can be seen as an instance of an inductive definition, but it can also be seen as a primitive definitional concept in its own right. Because an inductive definition merely identifies a subset of an already existing set, you can only define algebraic datatypes by an inductive definition if you have otherwise demonstrated the existence of a set containing strong enough closure properties. Isabelle's data type package does all the necessary work for you. These technical points have nothing to do with the question of which concept should be adopted when you are defining a model.
Larry Paulson
Last updated: Apr 27 2024 at 01:05 UTC