Quelle Zippy_Paper.thy

Sprache: Isabelle

✐‹creator "Kevin Kappelmann"›
section ‹Zippy Paper Guide›
theory Zippy_Paper
imports
Pure
begin

paragraph ‹Summary›
text ‹Guide for the preprintcite‹zippy››

text ‹
▪ General Information
▪ Unfortunately, employing the polymorphic record extension mechanism described in the paper
hits severe performance problems of the Poly/ML compiler.
To get around minute-long compilation times, all data fields of the zipper have to be
instantiated in one go rather than by repeated instantiation of polymorphic fields,
cf. @{file "Zippy/Instances/zippy_instance_base.ML"}.
Relevant issue on GitHub: https://github.com/polyml/polyml/issues/213

▪ Section 2
▪ Nodes @{file "Gen_Zippers/Zippers5/Alternating_Zippers/Instances/Nodes/node.ML"}

▪ Section 2.1
▪ Categories and Arrows
@{file "ML_Typeclasses/Gen_Typeclasses/Typeclasses_1/Categories/category.ML"}

▪ Morphs
▪ Morphism Base @{file "Gen_Zippers/Zippers5/Morphs/morph_base.ML"}
▪ Morphisms @{file "Gen_Zippers/Zippers5/Morphs/morph.ML"}

▪ Zippers
▪ Zipper Morphs @{file "Gen_Zippers/Zippers5/Zippers/zipper_morphs.ML"}
▪ Zipper Data @{file "Gen_Zippers/Zippers5/Zippers/zipper_data.ML"}
▪ Zipper @{file "Gen_Zippers/Zippers5/Zippers/zipper.ML"}

▪ Linked Zippers
▪ Linked Zipper Morphs @{file "Gen_Zippers/Zippers5/Linked_Zippers/linked_zipper_morphs.ML"}
▪ Linked Zippers @{file "Gen_Zippers/Zippers5/Linked_Zippers/linked_zipper.ML"}

▪ Alternating Zippers
▪ Alternating Zipper Morphs
@{file "Gen_Zippers/Zippers5/Alternating_Zippers/alternating_zipper_morphs.ML"}
▪ Alternating Zippers
@{file "Gen_Zippers/Zippers5/Alternating_Zippers/alternating_zipper.ML"}
▪ Alternating Zipper Product
@{file "Gen_Zippers/Zippers5/Alternating_Zippers/pair_alternating_zipper.ML"}

▪ Section 2.1.1
▪ Monads
@{file "ML_Typeclasses/Gen_Typeclasses/Typeclasses_1/typeclass_base.ML"}

▪ Kleisli Category
@{file "ML_Typeclasses/Gen_Typeclasses/Typeclasses_1/Categories/category_instance.ML"}

▪ Generating Alternating Zippers from Node Zippers
▪ Extending the Alternating Zipper
@{file "Gen_Zippers/Zippers5/Alternating_Zippers/Instances/Nodes/alternating_zipper_nodes.ML"}
▪ Extending and Lifting the Input Zippers
@{file "Gen_Zippers/Zippers5/Zippers/extend_zipper_context.ML"}

▪ Generating Node Zippers
@{file "Gen_Zippers/Zippers5/Alternating_Zippers/Instances/Nodes/alternating_zipper_nodes_simple_zippers.ML"}

▪ Section 2.2
▪ Lenses @{file "ML_Typeclasses/Gen_Typeclasses/Typeclasses_1/Lenses/lens.ML"}

▪ Section 3
▪ We implemented a generalisation of the state monad that also allows the state type to change
during computation. Such states are not monads but (Atkey) indexed monads.
▪ Atkey Indexed Monads @{file "ML_Typeclasses/Gen_Typeclasses/Typeclasses_1/itypeclass_base.ML"}
▪ Indexed State Monad @{file "ML_Typeclasses/Gen_Typeclasses/Typeclasses_1/State/istate.ML"}
▪ State Monad @{file "ML_Typeclasses/Gen_Typeclasses/Typeclasses_1/State/istate.ML"}
▪ Antiquotations
▪ Sources
@{file "ML_Typeclasses/Antiquotations/ML_Eval_Antiquotation.thy"}
@{file "ML_Typeclasses/Antiquotations/ML_Args_Antiquotations.thy"}
@{file "Antiquotations/ML_IMap_Antiquotation.thy"}
▪ Example Configuration and Follow-Up ML-Code Generation
@{file "Gen_Zippers/Zippers5/Morphs/ML_Morphs.thy"}

▪ Section 4. We highlight the differences/extensions to the paper description
▪ The zipper uses an additional "action cluster" layer that sits between a goal cluster and
an action. Action clusters collect related actions, e.g. one could create an action cluster for
classical reasoners, one for simplification actions, etc. This gives the search tree some more
structure but is not strictly necessary (it is thus omitted in the paper).

▪ Adding Actions @{file "Zippy/Actions/zippy_paction_mixin_base.ML"}
▪ Action nodes do not store a static cost and action but, more generally,
an "action with priority" (paction) that dynamically computes a priority, action pair.
▪ Action clusters store a "copy" morphism such that actions generating new children can move
their action siblings to the newly created child while updating their siblings' goal focuses
(since the number and order of goals may have changed in the new child).

▪ Adding Goals @{file "Zippy/Goals/zippy_goals_mixin_base.ML"}
▪ Goal Clusters @{file "Zippy/Goals/Base/zippy_goal_clusters.ML"}
▪ Goal Cluster @{file "Zippy/Goals/Base/zippy_goal_cluster.ML"}
▪ Goal Focus @{file "Zippy/Goals/Base/zippy_goal_focus.ML"}
▪ Union Find @{file "Union_Find//imperative_union_find.ML"}

▪ Lifting Tactics
▪ Lifting Isabelle Tactics to Zippy Tactics @{file "Zippy/Tactics/Base/zippy_ztactic.ML"}
▪ Lifting Zippy Tactics to Actions @{file "Zippy/Instances/zippy_instance_tactic.ML"}

▪ The Basic Search Tree Model @{file "Zippy/Instances/zippy_instance_base.ML"}
Since there are is always exactly one goal clusters node, we do not use lists for the topmost layer.
▪ List Zipper @{file "Gen_Zippers/Zippers5/Zippers/Instances/list_zipper.ML"}

▪ Adding Failure and State @{file "Zippy/Instances/Zippy_Instance_Pure.thy"}
▪ Option Monad and Transformers
@{file "ML_Typeclasses/Gen_Typeclasses/Typeclasses_1/typeclass_base_instance.ML"}

▪ Adding Positional Information
▪ Extending the Alternating Zipper @{file "Zippy/Positions/zippy_positions_mixin_base.ML"}
▪ Alternating (Global) Position Zipper
@{file "Gen_Zippers/Zippers5/Alternating_Zippers/Instances/alternating_global_position_zipper.ML"}

▪ Running a Search
▪ Postorder Depth-First Enumeration for Zippers
@{file "Gen_Zippers/Zippers5/Zippers/Utils/df_postorder_enumerate_zipper.ML"}
▪ Postorder Depth-First Enumeration for Alternating Zippers
@{file "Gen_Zippers/Zippers5/Alternating_Zippers/Utils/df_postorder_enumerate_alternating_zipper.ML"}
▪ Runs @{file "Zippy/Runs/zippy_run_mixin.ML"}

▪ Retrieving Theorems from the Tree
@{file "Zippy/Goals/Lists/zippy_lists_goals_results_top_meta_vars_mixin.ML"}

▪ Final example usages can be found here
@{file "Zippy/Instances/Zip/Examples/Zip_Examples.thy"}.
›

end

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet am 2026-06-10) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.