\section{Introduction}\label{sec:intro}

When teaching programming, it is important to underline
that each (sub)program has a specification,
and requires a proof of actually meeting it---and that the
best way to write a program is to write its proof first.

For instance, here is a programming-by-proving exercise.
Assume that Peano numbers are known:
\begin{verbatim}
data N = Z | S N

doubleN :: N -> N
doubleN Z = Z
doubleN (S x) = S (S (doubleN x))
\end{verbatim}
The topic is binary numbers now:
\begin{verbatim}
data B = Zero | Even B | Odd B
\end{verbatim}
Their semantics is given by translation to Peano numbers:
\begin{verbatim}
value :: B -> N
value Zero = Z
value (Even x) = doubleN (value x)
value (Odd x) = S (doubleN (value x))
\end{verbatim}
The goal is to implement the successor function for the binary representation:
\begin{verbatim}
succB :: B -> B
succB Zero = _
succB (Even x) = _
succB (Odd x) = _
\end{verbatim}
and to prove it correct:
\begin{verbatim}
Lemma succ : forall b :: B : value (succB b) .=. S (value b)
Proof by induction on b :: B
...
QED
\end{verbatim}
The goal here is to derive the program
from the specification (lemma \verb|succ|)
by writing the proof (replacing the dots ``\verb|...|'')
and filling holes (underscores) in the program to make the proof work.

For instance, for case \verb|b = Odd x| of the inductive proof,
we expect the following chain of reasoning,
starting with the instantiated right-hand side of the lemma.
We already use Cyp notation for a proof by rewriting:
\begin{verbatim}
                     S (value (Odd x))
(by def value)   .=. S (S (doubleN (value x)))
(by def doubleN) .=. doubleN (S (value x))
(by IH)          .=. doubleN (value (succB x))
(by def value)   .=. value (Even (succB x))    -- P
(by def succB)   .=. value (succB (Odd x))
\end{verbatim}
Up to point $P$, all steps are straightforward.
The induction hypothesis is denoted by \verb|IH|.
From point $P$ to the final expression (the left-hand side of the lemma),
we have the creative step: \verb|succB| should have equation
\begin{verbatim}
succB (Odd x) = Even (succB x)
\end{verbatim}
to make the proof work. The all too common approach
of writing the program first, and the proof later,
is characterized as ``putting the cart before the horse''
by Dijkstra~\cite{EWD:EWD1305}. Development of the proof
is the horse that pulls forward the development of the program.

The above example exercise is taken
from the ``Fortgeschrittene Programmierung'' lecture,
taught by one of the authors (Schwarz)
in Sommersemester 2020.
Student solutions for this exercise are automatically checked
with our extension~\cite{Renz20,cyp-htwk}
of the Cyp system~\cite{cyp-tum,cyp-ethz},
integrated into Leipzig Autotool~\cite{autotool}.

In the present paper, we briefly present
our existing auto-grader for programming exercises (Section~\ref{sec:autotool}),
then summarize Cyp (Section~\ref{sec:cyp}).
We then explain the design of our extensions: holes (Section~\ref{sec:holes})
and types (Section~\ref{sec:types}).
These extensions were developed in the master's thesis~\cite{Renz20}
of one of the authors (Renz).
Finally we report on our experience of using Cyp (Section~\ref{sec:exp}).
Some implementation detail is discussed in the Appendix.

\section{Preliminaries: Auto-Grading of Programming Exercises}\label{sec:autotool}

Autotool~\cite{autotool} is an auto-grader that started out in 1999
as a CGI script written by one of the authors (Waldmann)
to assist students executing derivations in Hilbert calculus.
Since then it has grown into a system supporting different exercise types.
It consists of web front-ends for students and instructors,
a semantics back-end that does the actual grading,
and a persistence component.
Autotool's primary functionality is:

\begin{itemize}
\item The instructor configures and publishes exercises.
  The students submit solutions.
  Autotool checks solutions semantically---as opposed to just checking
  syntactically whether some known good solution was met.
  This allows for detailed error messages
  that still do not give away the correct solution.
\item Exercises can be solved during a certain time period (set by the instructor).
  For students to pass the exercise, they have to submit a correct solution
  at least once in that period. Number of submissions is unlimited,
  and experimentation is encouraged, as students will practice
  reading error messages.
\item Students can compete for and check on an (pseudonymized) leaderboard,
  ordered by size of submission, or some other problem-specific parameter.
  This motivates the search for better or more elegant solutions.
\item For some exercise types, Autotool generates
  individual problem instances for each student. This does not apply
  to the programming and proving exercises described here.
\end{itemize}

We are already using Autotool
for auto-grading of Haskell programming exercises~\cite{WaldmannWFLP17}.
An instance of an exercise is a program text with holes for terms.
The student has to fill in the holes.
The text contains an expression \verb|test :: Bool|
(without holes, of course).
Autotool will check that the submission is type-correct,
and that \verb|test| evaluates to \verb|True|.
The implementation uses the Glasgow Haskell Compiler\cite{ghc}'s API
via the Mueval library~\cite{mueval}.
For notating and evaluating tests,
we use the Leancheck library~\cite{leancheck}.

The introductory example can be framed as a program-and-test exercise
if we replace the lemma with
\begin{verbatim}
test :: Bool
test = holds 1000 $ \ (x :: B) -> value (succB x) == S (value x)
\end{verbatim}
Note the syntactic and semantic similarity.
``lambda'' takes the role of \verb|forall|.
This is exactly the point of property-based testing~\cite{DBLP:conf/icfp/ClaessenH00}.

For actually running the exercise, we add these declarations
\begin{verbatim}
{-# language DeriveGeneric, PatternSignatures #-}
import Test.LeanCheck
import Test.LeanCheck.Generic
data N = .. deriving (Eq)
data B = .. deriving (Show, Generic)
instance Listable B where tiers = genericTiers
\end{verbatim}
We need
\verb|Eq| for \verb|N| to evaluate the condition in the test,
\verb|Generic| for \verb|B| to generate test data,
and \verb|Show| for \verb|B| to print arguments for failed tests.

Type-directed generation of test cases
is an impressive showcase for the power of typeclasses in Haskell.
We make a point of including the complete source code in the exercise.
That way students can run this on their own machine,
and can also copy the approach to other code.
This would not be possible with a hidden implementation of testing.
We abhor hidden extra test cases even more.

In the above code,
it is %
sad that the natural declaration \verb|(x :: B)|
can only be written after enabling language extension \verb|PatternSignatures|,
which is deprecated, and will be replaced by \verb|ScopedTypeVariables|.
This cannot be comprehended. Where is the type variable?

\section{Preliminaries: Cyp - Check Your Proof}\label{sec:cyp}

For student exercises (and elsewhere),
testing is good, and widely used. Proving is better, but rarely done.
There seems to be a  disconnect between proving
(student writes homework proof on blackboard) and ``actual programming''
(student solves programming exercise that is auto-graded).

Cyp is a proof checker
that verifies proofs about Haskell-like programs.
It was developed by Dominik Durner and Lars Noschinski at TU Munich~\cite{cyp-tum},
and later by Dmitriy Traytel at ETH Zurich ~\cite{cyp-ethz}.
We now present the basics of Cyp by example,
and show our extensions in later sections.

Cyp was first mentioned 2014 in a report~\cite{DBLP:conf/haskell/BlanchetteHNNT14}
on teaching programming with Haskell to a large audience:
``We developed tool support for simple proofs by induction,
in the form of a lightweight proof assistant
and will integrate it into our homework submission system''.

Why not use a full proof checker, like Agda, Coq, Isabelle, PVS?
There is no publication on Cyp by the original authors,
so we have to guess a little.
A full proof checker may appear to require too much investment
of instructors' and students' time---to learn techniques and technicalities
that are perceived as ``not programming''.
Agda is perhaps closest to Haskell, but was not available widely at the time.
Also, a full proof checker may be hard to integrate in an auto-grader.

Isabelle had been used for auto-grading,
e.g., with Praktomat~\cite{praktomat16}
but that required heavy scaffolding and sandboxing
and even then, did not allow for full integration:
``we currently do not check what the students actually proved,
for that we still manually check their submission,
but this way any sorries or other problems are detected.''~\cite{Breitner16}

Cyp's design was influenced by
the Isar structured proof language~\cite{DBLP:conf/tphol/WenzelP06}
for Isabelle~\cite{DBLP:journals/fac/Nipkow89}.
The main features of Cyp are:
\begin{itemize}
\item a program is a collection of
  \begin{itemize}
  \item
  algebraic data types (ADT) (Haskell: \verb|data| declarations), and
\item
  functions defined by term rewriting system
  (Haskell: oriented equations)
  \end{itemize}
\item a specification (lemma or axiom) is an equation,
\item a proof may use term rewriting,
  extensionality for functions,
  case distinction (for the constructors of an ADT),
  and induction (following the ADT).
\end{itemize}
We give examples for Cyp's proof language.
These are sometimes incomplete but the semantics should be obvious.
Full example texts and syntax and semantics specification
are available in the source repository.
In the following, all typing judgments (\verb|:: Bool|, etc.)
are only available (and then, required) in Cyp-Leipzig.
We discuss typing in Section~\ref{sec:types}.

\paragraph{Proof by Rewriting.}
A sequence of steps, where each step connects two terms
by applying a rule that comes from a function definition,
or from a lemma.
\begin{verbatim}
Lemma succ_eq_plus_one: forall a :: N: S a .=. plus (S Z) a
Proof by rewriting
                    S a
  (by def plus) .=. S (plus Z a)
  (by def plus) .=. plus (S Z) a
QED
\end{verbatim}
Cyp is not fully explicit here:
the student just names the function (here, \verb|plus|).
Cyp will determine the actual rule to use (here, \verb|plus| has two rules),
and the location and direction of its application,
via pattern-matching all rules and subterms.
We guess that authors wanted to avoid extra syntax for locations.
We consider introducing syntax for naming a rule
and specifying direction.

\paragraph{Proof by Extensionality.}

Add a symbolic argument to prove equality of functions.
\begin{verbatim}
Lemma: not . not .=. id
Proof by extensionality with x :: Bool
  Show: (not . not) x .=. id x
  ...
\end{verbatim}

\paragraph{Proof by Case Analysis.}

A complete case analysis for the constructor in the root of the term.
Continuing the previous example,
\begin{verbatim}
Proof by case analysis on x :: Bool
  Case True
    Assume  AS: x .=. True
    Then Proof ...
\end{verbatim}

\paragraph{Proof by Induction.}

Structural induction on terms.
The induction hypothesis has to be written explicitly.

\begin{verbatim}
Lemma symdiff_sym: forall x :: N, y :: N: symdiff x y .=. symdiff y x
Proof by induction on x :: N generalizing y :: N
  Case Z
    For fixed y :: N
    Show: symdiff Z y .=. symdiff y Z
    Proof ... QED
 Case S x
    Fix x :: N
    Assume IH: forall y :: N: symdiff x y .=. symdiff y x
    Then for fixed y :: N
    Show: symdiff (S x) y .=. symdiff y (S x)
    Proof ... QED
QED
\end{verbatim}
Notation \verb|Proof ... QED|
is valid in our extension, see Section~\ref{sec:holes}.

\paragraph{Restrictions.}

Cyp is not a full proof checker,
but a tool to teach equational logic and structural induction.
With that goal,
it keeps both programming and proving as simple as possible,
and we do not intend to change that.
\begin{itemize}
\item Definitions are global.
  There are no \verb|let|, or \verb|where| bindings,
  and no \verb|case| or \verb|lambda| expressions.
  This allows for a straightforward application of rewrite rules.
\item Propositions (called lemmas) are equations,
  with universal quantification over their variables.
  Cyp has no propositional logic or predicate logic.
  We did introduce mandatory type declarations for variables in lemmas,
  see Section~\ref{sec:types},
  making explicit the universal quantification.
\item All proof steps have to be written down. This is in contrast to
  interactive proof assistants that fill in proof steps,
  e.g., as Isabelle does with ``\verb|by auto|''.
\end{itemize}
The next two restrictions could possibly be lifted,
as we discuss in Section~\ref{sec:conc}.
\begin{itemize}
\item Cyp programs, like Haskell programs, have no guarantee of termination.
  Still, equational reasoning for such programs
  is ``morally correct''~\cite{DBLP:conf/popl/DanielssonHJG06}.
\item The semantics of pattern matching in Cyp programs is different
  from the operational semantics of Haskell.
  If a function $f$ is defined by several equations,
  Haskell semantics is to try them one after another,
  until a matching left-hand side is found.
  In a Cyp proof by rewriting, \verb|(by def f)| is correct
  if any of the defining equations of $f$ can be used.
\end{itemize}

The following properties of Cyp allow for an easy integration
into systems for automated grading of homework:
\begin{itemize}
\item
Proof checking is pure, in the Haskell sense: it does not involve IO.
Running Cyp in an auto-grader cannot change the system state
(on the disk, in the data base), and cannot leak secrets,
so it does not require sandboxing.
\item
Proof checking is strict, in the sense of ``strong'':
any attempt to cheat, by leaving holes in the submission,
will be detected, see Section~\ref{sec:holes}.
\end{itemize}

\section{Holes}\label{sec:holes}

We mentioned earlier (Section~\ref{sec:autotool})
that we already have auto-grading for ``blueprint'' programming exercises
where students replace holes by expressions.
For auto-grading Cyp exercises, we copy that idea,
and we also allow holes in proofs.
We describe the resulting syntax and semantics.

\paragraph{Design Goals for Holes.}
The syntactic function of a hole
is that it marks the place in a problem instance
where the student has to fill in something.
See \ref{subsec:match} for details on syntactic matching.

Holes do have semantics as well:
Cyp should not reject them, but accept temporarily,
by assuming the hole can be filled,
and continue checking other parts of the proof.
This allows for incremental development.

If holes were rejected outright,
then the student would first replace
each such hole with some expression (or proof)
that is syntactically valid,
but (most probably) semantically wrong.
By accepting the hole, we relieve the student of such rote edits.

We have a similar design for our Haskell exercises:
the (expression) hole is actually \verb|undefined|,
which GHC accepts and type-checks.
(We should switch to underscore, which recent GHCs
accept with \verb|-fdefer-type-errors|.)

\paragraph{Holes for Expressions, Names of Rules, and Rewrite Steps.}
An underscore (\verb|_|) may appear instead of a sub-expression:
in the right-hand side of a function definition,
or in an equational proof.
An underscore can also be used in \verb|(by _)|
as a placeholder for the name of a lemma, axiom, or definition
to be applied in a rewrite step.
In a proof by rewriting, three dots (\verb|...|) denote any chain of rewrite steps
where neither rules nor expressions are specified.

Expression holes have type \verb|forall a. a|
(as does \verb|undefined| in Haskell) when typechecking.
When checking the validity of a chain of equations,
Cyp will assume that anything can be rewritten into a hole,
and out of a hole.

Any rewrite step $t_1$ \verb|(by _)| $t_2$ will be accepted.
Cyp will not check that there is indeed a rule that can be
substituted for the hole.

\begin{example}\label{ex:holes:rewrite}
  This is similar to one problem we used in a lecture, see Section~\ref{sec:exp}.
\begin{verbatim}
e :: T
axiom assoc: forall x :: T, y :: T, z :: T :
  times x (times y z) .=. times (times x y) z
axiom neutral_right: forall x :: T : times x e .=. x
axiom neutral_left: forall x :: T : times e x .=. x
axiom square:  forall x :: T : times x x .=. e
Lemma  : forall x :: T, y :: T : times x y .=. times y x
Proof by rewriting
                   times x y
  (by _ )      .=. times (times x y) e
  (by square)  .=. _
  (by assoc)   .=. _
  (by assoc)   .=. _
  (by assoc)   .=. times (times x (times (times y y) x)) (times y x)
  ...             .=. times y x
QED
\end{verbatim}
We expect the student to infer \verb|(by neutral_right)|
for the first rewrite step, as no other axiom matches.
Then, \verb|(by square)| can only match
if \verb|e| is rewritten to some square,
which must be guessed to be \verb|times (times y x) (times y x)|,
and a strong hint is given by the expression
that has to be reached via associativity.
From looking at \verb|(times y y)|,
the student should guess that \verb|(by square)| comes next,
and continue with the greedy approach of always simplifying when possible.
The exercise is solved by applying
\verb|neutral_left|, \verb|square|, \verb|neutral_left|.
By formulating the exercise with the given hints,
we have removed the ``group theoretic'' aspects
and reduced it to a pattern matching drill, on purpose.
\end{example}

\paragraph{Holes for Proofs.}

In proofs,
three dots (\verb|...|) denote any number of missing lemmas,
missing proofs (also sub-proofs) or missing cases
in proofs by case analysis, and proofs by induction.
In practice (see Section~\ref{sec:exp}),
we did not use exercises with missing lemmas.
For proofs by case analysis and by induction,
we did use heavily the option of giving one case nearly completely,
and leaving the other(s) for the student to fill in.

\begin{example}\label{ex:holes:proof}
  The case for constructor \verb|S| is missing in the following:
\begin{verbatim}
data N = Z | S N

plus :: N -> N -> N
plus Z y     = y
plus (S x) y = S ( plus x y )

Lemma plus_Z: forall x :: N : plus x Z .=. x
Proof by induction on x :: N
  Case Z
      Show: plus Z Z .=. Z
      Proof ... QED
  ...
QED
\end{verbatim}
\end{example}

When Cyp encounters a missing proof
it is treated as if it were correct, much like Isabelle treats \verb|sorry|.
When a proof by case analysis or by induction has a hole for missing cases,
Cyp will assume that the present cases are complete.

\section{Types}\label{sec:types}

Originally, Cyp did not have types for programs or for proofs,
except for type judgments to determine what constructors
need to be handled in proofs by case analysis and by induction.
These judgments were checked only implicitly:
if one constructor was used, all others from the same \verb|data| declaration
had to be handled as well.

Contrary to what the student should expect from Haskell,
there was no explicit type checking,
and the notation was confusing:
the type defined by \verb+data List a = Nil | Cons a (List a)+
had to appear in the proof without the type argument:
\verb|Proof by induction on List xs|.
This looks like medieval (i.e., pre-1.4) Java
and the corresponding \verb|xs :: List| is a kind-error in Haskell.

\paragraph{Types for programs.}

Cyp did not type-check the program
since it was assumed to be given by the instructor,
who could ensure correct typing by extra means
(divination, or GHC perhaps),
and the student could not change the program.

Our version of Cyp allows holes in the program
that the student can fill with arbitrary expressions.
For sanity, and for consistency with Haskell, we type-check programs.
We use the ``Typing Haskell in Haskell'' library~\cite{thih},
restricted to Cyp's Haskell subset (e.g., without type classes).
An expression hole is treated as \verb|_ :: forall a . a|.
This allows to accept programs with holes.

\paragraph{Types for lemmas.}

Cyp did not type-check proofs
since it was assumed that nothing bad could happen
when applying rules (from a program that was known to be type-correct)
to terms from goals (also type-correct).

\begin{example} This assumption, however, is wrong, as shown by the following:
\begin{verbatim}
data U = U

Lemma eek: x .=. y
Proof by case analysis on x :: U
  Case U
    Assume AS_x: x .=. U
    Then Proof by case analysis on y :: U
      Case U
        Assume AS_y: y .=. U
        Then Proof by rewriting
                       x
         (by AS_x) .=. U
         (by AS_y) .=. y
QED QED QED
\end{verbatim}
The problem is that Lemma \verb|eek|
is implicitly assumed to be polymorphic in $x$ and $y$,
while it was only proved for monomorphic $x$ and $y$ of type \verb|U|.
We can then prove \verb|False .=. True| by applying \verb|eek|.
\end{example}

We solve this problem by requiring every lemma to be explicit
about the types of its variables,
and then we type-check its proof in that context.
The problematic proof
\begin{verbatim}
data U = U

Lemma eek: forall x :: a, y :: a : x .=. y
Proof by case analysis on x :: U
...
QED
\end{verbatim}
will now get rejected, since the type (\verb|U|) of \verb|x| in the discriminant
is different from the (polymorphic) type of \verb|x| in the lemma.

\paragraph{Local names in lemmas.}
Explicit types also solve the following problem:
is \verb|e| a variable or a constant in:
\begin{verbatim}
axiom right_neutral : times x e .=. x
\end{verbatim}
In original Cyp, this \verb|e| is a local variable,
unless there is some globally defined \verb|e|,
then the name will refer to that, as in:
\begin{verbatim}
e = e  ;  axiom right_neutral : times x e .=. x
\end{verbatim}
This is inconsistent with local declarations
shadowing global declarations in Haskell.
We now write
\begin{verbatim}
axiom right_neutral : forall x :: T : times x e .=. x
\end{verbatim}
Since \verb|e| is not declared to be local in the axiom,
it is a reference to a global name.

\paragraph{Types in equational proofs.}

We check that all terms in an equational proof have identical type,
under the typing assumptions for the free variables of the lemma.

This allows to give precise and early error messages,
where otherwise the error would likely have manifested
in a more obscure way, e.g., by there not being a fitting rewrite rule.

\paragraph{Typed application of rules.}

When a rule from a lemma or from an axiom
is applied in a proof by rewriting,
Cyp determines, by syntactic matching,
what subterm $t_1$ is rewritten to what $t_2$,
and under what substitution of the lemma's variables.
We use our type-checking mechanism to see
if the variables' and the terms' types unify.

\begin{example}
Assume we proved \verb|eek| for the correct type:
\begin{verbatim}
data U = U
Lemma eek: forall x :: U, y :: U: x .=. y
Proof ... QED
\end{verbatim}
Then the following attempt to apply \verb|eek|
\begin{verbatim}
data Bool = False | True
Lemma contradiction: False .=. True
Proof by rewriting
               False
  (by eek) .=. True
QED
\end{verbatim}
will get rejected,
because we obtain the substitution
that maps \verb|x| to \verb|False|
and \verb|y| to \verb|True|
for rewriting the left- to the right-hand-side
using \verb|eek|,
and the types \verb|x :: U| and \verb|False :: Bool|
as well as the types of \verb|y :: U| and \verb|True :: Bool|
do not unify.
\end{example}

\section{Experience Report}\label{sec:exp}

Cyp, with our extensions, was being used in the
``Fortgeschrittene Programmierung'' (Advanced Programming) lecture
for Computer Science B. Sc. students in their 4th semester.
(The recent addition of typed lemmas was not available.)
The lecture follows~\cite{WaldmannWFLP17}
and was taught by one of the authors (Schwarz) in 2020.
While auto-grading for Haskell exercises was used before,
this was the first instance of using Cyp as well.
Because of Corona lock-down, the lecture was virtual.
This made auto-grading of part of homework all the more important.
(There were other homework and discussions via internet platforms,
shared documents, and audio conferencing.)

\paragraph{How Cyp was used.}
We installed GHC (with Leancheck) and Cyp in the computer pool
(on Debian GNU/Linux machines) and students logged in via SSH.
Students were also encouraged to install GHC and compile Cyp on their home computers.
The instructor used the pool installation in tutorial presentations
on BBB (Big Blue Button) conferences, on a server hosted by our department:
share the view of one terminal window,
SSH to a computer in the pool,
start \verb|tmux| and split the window,
run an editor in one half, and show GHCi or Cyp output in the other half.

While we have integrated Cyp in Autotool,
we always maintain a command line version of Cyp with identical semantics.
It can be called with one argument (a module to be checked)
or two (a blueprint module, and a solution module).

The recommended ``IDE for Cyp'' is the command
\begin{verbatim}
while (inotifywait -q *.[bc]yp); do cyp -m ex.byp ex.cyp; done
\end{verbatim}
where
\verb|ex.byp| (\underline{b}lueprint for c\underline{yp}) is the problem instance,
with the holes, downloaded from Autotool;
and \verb|ex.cyp| is the student's working file.
Each time this file is saved from inside the editor,
Cyp will check it (locally). Finally, the student uploads the solution to Autotool,
where it is checked again, and the outcome is stored.

\paragraph{Types of exercise used.}

Over 14 weeks of teaching, we posed Cyp exercises on
\begin{itemize}
\item proof by rewriting (only), cf. Example~\ref{ex:holes:rewrite}
\item proof by case analysis (and rewriting), e.g.,
  \begin{example}
\begin{verbatim}
data Bool = False | True

xor :: Bool -> Bool -> Bool
xor False False = False  ; xor False True  = True
xor True  False = True   ; xor True  True  = False

Lemma xor_sym : forall x :: Bool, y :: Bool : xor x y .=. xor y x
Proof by case analysis on x :: Bool
 Case False
   Assume  AX: x .=. False
   Then Proof by case analysis on y :: Bool
   Case False
     Assume  AY: y .=. False
     Then Proof by rewriting
                  xor x y
      (by AX) .=. _
      (by AY) .=. _
      (by AY) .=. _
      (by AX) .=. _
     QED
   Case True
     Assume  AY: y .=. True
     Then Proof by rewriting
              xor x y
      ... .=. xor y x
     QED
  QED
  ...
QED
\end{verbatim}
  \end{example}
\item proofs by induction on \dots
  \begin{itemize}
  \item
  Peano numbers, cf. Example~\ref{ex:holes:proof},
  and another on associativity and commutativity of addition,
  with implementation of addition given, and assuming
\begin{verbatim}
axiom plus_Z: plus x Z .=. x
axiom plus_S: plus x ( S y ) .=. S ( plus x y )
\end{verbatim}
\item singly linked lists:
\begin{verbatim}
len ( append xs ys ) .=. plus ( len xs ) ( len ys )
\end{verbatim}
\item binary trees, prove \verb|mirror (mirror t) .=. t|
 \item a representation of binary numbers, see Section~\ref{sec:intro}.
  \end{itemize}
\end{itemize}

\paragraph{Statistical data on auto-graded exercises.}
In total, 39 mandatory problems were assigned in Autotool,
twelve of them contained proofs in Cyp and
15 were Haskell programs with holes.

Two problems %
were given with complete solutions beforehand.
They were also used by the instructor during an online session
to demonstrate the usage of the Cyp installation in our computer pools.

Most of the problems require just one proof, some up to three.
In problems that contain more than one proof,
the first proof was sometimes given with a near-solution and the others
without further hints. %

Two problems required
proofs by rewriting,
  %
  %
  %
  %
  %
  %
  %
  %
  %
three by case analysis,
 %
  %
  %
  %
  %
  %
  %
  %
  %
and seven by induction on
Peano numbers,
  %
  %
  %
  %
binary numbers,
  %
lists,
  %
or trees.
  %
  %

Near-solutions containing only \verb|_| holes for expressions were provided for
three proofs.
The other problems contained \verb|...| holes for whole proofs.
In around half of them, the proof method (rewriting, case analysis,
induction) was required.

Some problems were given in two versions. %
On the one hand, the students have to fill holes for expressions in a Haskell
program to satisfy the specification that is tested by Leancheck.
On the other hand, they have to prove in Cyp that their code satisfies
this specification.
In these cases, the solution to the first problem should not be given
in the setting of the Cyp program.
Therefore, we use \verb|_| holes in programs in the Cyp problem
in addition to the holes in proofs.

\paragraph{Student performance  and evaluation.}

Among the 95 participants of the lecture, 71 solved at least 19
Autotool problems correctly.
Out of these 71, all solved at least two Cyp problems and most solved
at least half of all Cyp problems.

In addition to Autotool, students had to solve exercise sheets and discussed
their solutions online. Some of these problems also contained proofs.
We observed that many student solutions were given in Cyp format and had been
checked by Cyp, even if we did not explicitly require this.

During the last lecture, the instructor asked the 43 participants via
an online poll:
\emph{Did Cyp exercises in Autotool help you to understand how to write proofs?}
Out of 28 answers, 27 said yes and one said no.

Therefore, we now consider using Cyp examples and exercises
earlier in the curriculum, maybe even before a thorough introduction to the
Haskell programming language.

\section{Discussion and Conclusion}\label{sec:conc}

We discuss two topics for further development of Cyp.

\paragraph{Operational Semantics of Cyp Programs.}

An interesting connection is that
while we want to replace a property-based test by a proof of the property,
the Isabelle IDE automatically can derive and execute such a test from a lemma.

Could we do the same for Cyp, as the example from the introduction suggests?
We can certainly add \verb|deriving (Eq, Show, Generic)|
to every \verb|data| declaration,
and mechanically generate a testable property from a lemma.

But what is the relation between lemmas that are ``operationally true'' in Haskell
and lemmas that we can prove?
Cyp will accept
\begin{verbatim}
f :: Bool -> Bool ; f False = False ; f False = True
Lemma False .=. True
Proof by rewriting   False
  (by def f) .=. f False
  (by def f) .=. True
QED
\end{verbatim}
but the second proof step does not have an operational equivalent in Haskell.

We could enforce operational semantics of top-down matching.
This would complicate rule application in equational proofs,
as we have to check that earlier rules don't match.
Given this function declaration
\begin{verbatim}
f (S x) y = _
f x (S y) = _
\end{verbatim}
we cannot rewrite the expression \verb|f a (S b)| (in some equational proof)
with either rule, since \verb|a| needs to be elaborated first.
Cyp could rewrite patterns by removing cases that are covered earlier.
The second rule then comes out as \verb|f Z (S y)|.
A compiler will do this~\cite{DBLP:conf/fpca/Augustsson85}
when generating code for an abstract machine,
but Cyp generates code that must be used by students.

It seems better to avoid this problem
by enforcing that patterns of each function definition are disjoint.
Students can get the same behaviour from GHC
via \verb|-Woverlapping-patterns|.

\paragraph{Termination.}

Totality of functions is a subject of teaching.
Cyp's functions are not total.
(The previous paragraph shows that they aren't even functions.)
One reason for non-totality is incomplete patterns in function definitions,
which we could check, as GHC already does with
\verb|-Wincomplete-patterns|.
Another reason is non-termination, coming from recursion,
which is unrestricted both in Haskell and in Cyp.
\begin{itemize}
\item We could prohibit recursion altogether.
  This is a drastic measure, and then we lose the motivation for induction.
  It still can be useful, e.g., to force the student to implement
  a specification by using \verb|fold| (with given axioms),
  and not by ad-hoc recursion.
\item We could restrict recursion to those cases
  where if a well-founded monotone order of function calls
  %
  %
  can be determined by Cyp,
  %
  or is provided by the student.
  %
\end{itemize}
The Cyp-style solution would certainly be to make this
simple (no complicated order, just the subterm relation)
and explicit (annotating the decreasing argument).

\paragraph{Conclusion.}
We extended the Cyp proof checker
with a pattern matcher for program and proof terms,
and with a type checker.
This allows to auto-grade student exercises
on completing implementations and proofs of Haskell-like programs.

Cyp can be used stand-alone (on the command line),
and in our auto-grading system Autotool.
We used Cyp successfully in a lecture.

\bibliographystyle{myplainurl}


\section{Action variable for the classical two-mode Bose-Hubbard model with $0 \leq u < 1$}

We consider the single-dimer Hamiltonian $H_r$ in Eq.\ (3), with particle number $n_r=|\alpha_{1r}|^2+|\alpha_{2r}|^2$. We henceforth drop the $r$ subscripts, so that we begin from
\begin{equation}\label{Hsup1}
H = -\frac{1}{2}(\alpha^*_1\alpha_2 + \alpha^*_2\alpha_1) +\frac{U}{4}n^2+\frac{U}{4}(n_1-n_2)^2\;.
\end{equation}

As common in studies of the two-mode Bose-Hubbard model we next transform to the Schwinger representation of angular momentum,
\begin{align}
\frac{\alpha_1^*\alpha_2+\alpha_2^*\alpha_1}{2} &= L_1\nonumber\\
\frac{\alpha_1^*\alpha_2-\alpha_2^*\alpha_1}{2i} &=L_2\nonumber\\
\frac{|\alpha_1|^2-|\alpha_2|^2}{2} &=L_3\;.
\end{align}
Although more commonly introduced quantum mechanically, where it is justified by the fact that the canonical commutation relations of the bosonic creation and destruction operators reproduce the angular momentum algebra, this transformation also works classically, with the classical Poisson brackets replacing the quantum commutators. We further note that this representation implies $L_1^2+L_2^2+L_3^2\equiv (n/2)^2$. With this transformation we render (\ref{Hsup1}) into
\begin{equation}
H = -L_1 +U L_3^2+ \frac{Un^2}{4}\;.
\end{equation}

We then introduce a canonical representation of the angular momentum variables for fixed $n$:
\begin{align}
L_1 &= P\nonumber\\
L_2 &= \sqrt{(n/2)^2-P^2}\cos\phi\nonumber\\
L_3 &= \sqrt{(n/2)^2-P^2}\sin\phi\;,
\end{align}
where $\phi,P$ are a canonically conjugate pair with the finite ranges $-n/2\leq P \leq n/2$ and $-\pi < \phi \leq \pi$, $\phi =\pm\pi$ being identified so that we have a finite cylindrical phase space. (It is easy to confirm that the canonical Poisson brackets of $\phi$ and $P$ reproduce those of the angular momentum variables.) This delivers
\begin{equation}
H = -P + U[(n/2)^2-P^2]\sin^2\!\phi + Un^2/4\;.
\end{equation}
A key feature of this our final transformation is that for $0<Un<1$ all the contours of constant $H=\varepsilon$ sweep through the entire $[0,2\pi]$ range of $\phi$.

For $0<Un<1$ it can also be shown that $Un^2/4-n/2\leq\varepsilon Un^2/4+n/2$.  We therefore represent the energy in terms of the angle $\eta\in [-\pi/2,\pi/2]$ according to
\begin{equation}
\varepsilon = \frac{Un^2}{4} + \frac{n}{2}\sin\eta
\end{equation}
and express the contour of constant energy $H=\varepsilon$ in the $(\phi,P)$ phase space as
\begin{equation}
U\sin^2\phi\, P^2 + P + \frac{n}{2}\sin\eta - \frac{Un^2}{4}\sin^2\!\phi= 0\;.
\end{equation}
Solving the quadratic equation, and discarding one branch because we must have $P\geq -n/2$, gives
\begin{align}
P(\phi,\eta,n) &= \frac{1}{2U\sin^2\phi}\left(-1 + \sqrt{1 - 2Un\sin\eta\,\sin^2\phi + (Un)^2\sin^4\phi}\right)\nonumber\\
&\equiv\frac{n}{2u\sin^2\phi}\left(-1 + \sqrt{1 - 2u\sin\eta\,\sin^2\phi + u^2\sin^4\phi}\right)\equiv n X(\phi,\eta,u)\;,
\end{align}
for $u=Un$.

The area enclosed for given $\eta$ between this contour $-n/2\leq P(\eta,\phi)\leq n/2$ and the minimum energy contour $P(-\pi/2,\phi)=n/2$ is then by definition equal to $2\pi$ times our action variable $m(\varepsilon,n)$:
\begin{align}
m(\varepsilon,n) &= \frac{n}{2} - \oint\!\frac{d\phi}{2\pi}\,P\Big(\phi,\eta(\varepsilon,n),n\Big)\nonumber\\
& = n\left(\frac{1}{2}-\oint\!\frac{d\phi}{2\pi}\,X\Big(\phi,\eta(\varepsilon,n),u\Big)\right)\;.
\end{align}

Defining the new integration variable $z=\sin^2\phi$ and then integrating by parts allows us to write $m(\varepsilon,n)$ as
\begin{equation}
m = n\left(\frac{1}{2}- \frac{1}{\pi} \int^{1}_{0} dz \sqrt{\frac{1-z}{z}} \frac{uz-\sin \eta}{\sqrt{(1+iue^{i\eta}z)(1-iue^{i\eta}z)}} \right)\;.
\end{equation}
The integral over $z$ is in the general class of elliptic integrals but it does not reduce immediately to any of the three standard Legendre forms of elliptic integral. Mathematica evaluates it exactly in terms of Appell $F_1$ functions, giving a form which is manifestly real but unfamiliar and also slow to compute numerically. If instead of taking $z=\sin^2\phi$ we change variables to $\xi=\cot\phi$ we can obtain an exact evaluation in terms of incomplete elliptic integrals at infinite argument. Applying elliptic integral identities we can then reduce these to complete elliptic integrals of the three basic Legendre types, and confirm by numerical plotting that the result is exactly equal to the exact result in Appell functions. Most of our analytical results in this paper are based on this evaluation:
\begin{align}
\frac{m}{n} =&\frac{1}{2} - \frac{1}{\pi}\mathrm{Re}\left[ 2\cos\eta\frac{K\!\!\left(\frac{1-i e^{-i \eta } u}{1+ie^{i \eta }u}\right)}{\sqrt{1+i e^{i \eta } u}}+\frac{2i}{u}\sqrt{1+i e^{i \eta } u}\, E\!\!\left(\frac{1-i e^{-i \eta} u}{1+ie^{i \eta }u}\right)
 +\frac{i e^{i \eta } \left(1-i e^{-i \eta } u\right) \Pi\!\!\left(i e^{-i \eta } u|\frac{2 i u \cos  \eta }{1+ie^{i \eta } u}\right)}{\sqrt{1+i e^{i \eta } u}}\right]\;,
\end{align}
where $K(m)$, $E(m)$, and $\Pi(n|m)$ are respectively the complete elliptic integrals of the first, second, and third kinds.

This final expression is admittedly ponderous but it evaluates efficiently numerically and the complete elliptic integrals obey a number of well-known identities, so that derivatives of $m$ with respect to $\varepsilon$ can also all be evaluated exactly in terms of complete elliptic integrals. In particular the microcanonical entropy, temperature, and specific heat can all be obtained straightforwardly, because through further elliptic integral identities the derivative of $m$ with respect to $\varepsilon$ simplifies dramatically to just
\begin{equation}
\frac{\partial m}{\partial\varepsilon} = \frac{2}{\pi}
\frac{K\!\!\left(
	1-\frac{1-i e^{-i \eta} u} {1+ie^{i\eta}u}
	\right)}
	{\sqrt{1+i e^{i\eta}u}}\;,
\end{equation}
which is real in spite of its complex arguments because of an identity satisfied by complete elliptic integrals of the first kind.

Since $2\pi m$ is the action variable for the Bose-Hubbard dimer, $2\pi m'(\varepsilon)$ not only gives the quantum density of states in the semiclassical limit, and therefore the microcanonical entropy, but is also the period of the classical orbit at energy $\varepsilon$. $K(0)\equiv\pi/2$, so we can confirm that
\begin{equation}
\lim_{\varepsilon\to\varepsilon_\pm} \frac{\partial m}{\partial\varepsilon} = \lim_{\eta\to\pm\pi/2}\frac{\partial m}{\partial\varepsilon} = \frac{1}{\sqrt{1\mp u}}\;,
\end{equation}
which agree with the inverse Josephson frequencies of small oscillations around the ground and highest excited states.

The microcanonical temperature can be expressed in terms of complete elliptic integrals as well:
\begin{equation}
\frac{1}{k_BT} = \frac{u-\sin\eta}{2n\cos^2\eta (1-i e^{-i\eta}u)}\frac{E\!\!\left(
	1-\frac{1-i e^{-i \eta} u} {1+ie^{i\eta}u}\right)}{K\!\!\left(
	1-\frac{1-i e^{-i \eta} u} {1+ie^{i\eta}u}\right)}+\frac{\sin\eta}{2n\cos^2\eta}\;,
	\end{equation}
which is again identically real in spite of its complex arguments. The temperature is also finite at minimum and maximum energy in spite of the $1/\cos^2\eta$ factors, and finite for $n\to0$ as long as $U>0$. The limits are
\begin{equation}
k_B T_\pm = k_B T(\varepsilon_\mp) = \frac{(1\pm u)^2}{2U(1-\pm u/4)}\;.
\end{equation}

\section{Critical $Un$ for adiabatic invariance of $M$ from Bogoliubov stability analysis of the maximally excited array}

The calculation we perform to fix $u_c$ for the onset of $M$ decay is actually linear stability analysis of the maximally excited array state $\alpha_{1,r}=-\alpha_{2,r}=\sqrt{n/2}$. Since this maximally excited state has maximum $M$ value, its instability necessarily involves decrease of $M$. The reason that the stability of this very particular homogeneous state can be used to diagnose the invariance of $M$ for generic states is that the instability which we will find for the homogeneous state will turn out to be at the \emph{shortest} possible wavelengths. It is thus actually a local instability which can appear whenever even a few neighboring dimers are maximally excited. We have seen in our main text that the cases in which $M$ is adiabatically invariant, and in which it matters that $M$ is adiabatically invariant, are cases with bimodal dimer ensembles in which maximally excited dimers are not uncommon. The calculation of $u_c$ from the maximally excited state of the whole array thus shows when energy bimodality due to adiabatic invariance of $M$ becomes self-inconsistent, because above this $u_c$ threshold invariance of $M$ will lead to clusters of maximally excited dimers in which $M$ will spontaneously decay.

To perform the linear stability analysis we begin with the Hamiltonian equations of motion according to (1) from our main text, which are the two-component discrete Gross-Pitaevskii (GP) nonlinear Schr\"odinger equation
\begin{align}
i\dot{\alpha}_{1,jk} &= -\frac{J}{2} \sum_{\langle r,r^{\prime}\rangle} \alpha_{1,r^{\prime}} - \frac{\alpha_{2,r}}{2}  + U|\alpha_{1,r}|^2 \alpha_{1,r} \\
i\dot{\alpha}_{2,r} &= -\frac{J}{2} \sum_{\langle r,r^{\prime}\rangle} \alpha_{2,r^{\prime}} - \frac{\alpha_{1,r}}{2}  + U|\alpha_{2,r}|^2 \alpha_{2,r} \;,
\end{align}
where $r$ is short for the site indices $j,k$ in the 2D array.

We then linearize the above equations around the array's homogeneous maximally excited state $\alpha_{1,r}=-\alpha_{2,r}=\sqrt{n}$, which has $i\dot{\alpha}_{\sigma,r}=\nu\alpha_{\sigma,r}$ for
\begin{equation}
\nu = \frac{Un+1-J}{2}\;.
\end{equation}
Since the background about which we linearize has discrete translation symmetry in the $L\times L$ torus, we assume a discrete plane wave Ansatz
\begin{equation}
\alpha_{\sigma,jk}(t) = e^{-i\nu t}\left((-1)^\sigma\sqrt{\frac{n}{2}} + a_\sigma e^{\frac{2\pi i}{L}(p_1 j + p_2 k)}e^{-i\omega t} + b^*_\sigma e^{-\frac{2\pi i}{L}(p_1 j + p_2 k)}e^{-i\omega t}\right)
\end{equation}
for integers (discrete two-dimensional wave numbers) $\mathbf{p} = (p_1,p_2)$, linear excitation frequency $\omega(\mathbf{p})$, and infinitesimal two-component amplitudes $a_\sigma$, $b_\sigma$. Writing $u=Un$ as in the main text, this yields the time-independent Bogoliubov-de Gennes (BdG) equations
\begin{equation}
\omega \left(\begin{matrix} a_1 \\ a_2 \\ b_1 \\ b_2\end{matrix}\right) = \left(\begin{matrix} u + \mathcal{J}_\mathbf{p}-2 -\nu & \frac{1}{2} & \frac{u}{2} & 0 \\ \frac{1}{2} & u + \mathcal{J}_\mathbf{p}-2 -\nu & 0 \frac{u}{2}  \\ -\frac{u}{2} & 0 & -(u + \mathcal{J}_\mathbf{p}-2 -\nu) & -\frac{1}{2} \\ 0 & -\frac{u}{2} & -\frac{1}{2} & -(u + \mathcal{J}_\mathbf{p} -2-\nu)\end{matrix}\right)\left(\begin{matrix} a_1 \\ a_2 \\ b_1 \\ b_2\end{matrix}\right)
\end{equation}
where $\mathcal{J}_\mathbf{p} = 2J[\sin^2(\pi p_1/L)+\sin^2(\pi p_2/L)]$.

The eigenfrequencies $\omega(\mathbf{p})$ of the four-by-four matrix have the two branches $\pm \sqrt{\mathcal{J}_\mathbf{p}(\mathcal{J}_\mathbf{p} + u)}$, which is always real, and
\begin{equation}
\omega =\pm \sqrt{(1 - \mathcal{J}_\mathbf{p})(1 - u - \mathcal{J}_\mathbf{p})}
\end{equation}
which is imaginary, indicating dynamical instability, when $1-u < \mathcal{J}_\mathbf{p} < 1$. Since $\mathcal{J}_\mathbf{p}$ can always be made smaller by choosing smaller $\mathbf{p}$, the requirement for $\omega$ to be real for \emph{all} $\mathbf{p}$ is the requirement that the largest possible value $\mathcal{J}_\mathbf{p}$ is still smaller than $1-u$. The largest possible value of $\mathcal{J}_\mathbf{p}$ occurs for maximum $p_1 = p_2 = L$, giving $\mathcal{J}_\mathbf{p}\to 4J$. Thus the onset of instability, which occurs at the shortest possible wavelengths in the array, is $4J > 1- u$, so that the instability threshold is $u_c = 1-4J$ as stated in our main text. For the numerical evolutions shown in our main text we have used $J = 0.05$, giving $u_c = 0.8$.

We can confirm by numerical evolution of the array that the total dimer action $M=\sum_r m_r$ really does remain adiabatically invariant as long as the average $u<u_c$ but ceases to be invariant for average $u>u_c$. We do this by taking the initial state in which all the dimers of the array are at maximum energy ($\alpha_{2r}=-\alpha_{1r} = \sqrt{n/2}$), then adding a small random perturbation, and evolving over a long time. In Fig.\ \ref{joson_stability}a we have plotted the evolution of $M$ over time for two cases of average $u$, one just below $u_c$ and one just above it. The late-time value of $M$ is then plotted as a function of $u$ in Fig.\ \ref{joson_stability}b. The total $M$ is quite accurately conserved for $u$ below critical $u_c$, but for $u$ just above $u_c$ we see that $M$ drops substantially. (It does not necessarily decay to zero; total energy remains conserved and the single-dimer energy held in $m_r$ attains an equilibrium with the energy stored in long-wavelength sound waves in the Bose-Hubbard array.)  As explained above, the breakdown of adiabatic invariance of $M$ is due to short-wavelength instability in the array and so any small cluster of maximally excited dimers, such as tends to form if $M$ is invariant, will actually allow $M$ to decrease if $u> u_c$ in the cluster.
\begin{figure}[ht]
\centering
\includegraphics[clip=true,width=0.5\columnwidth]{FigS2.pdf}
\caption{(a) Dynamics of total dimer action variable $M$ for two representative values of $u$ below and above the critical $u_c$ for $J=0.05$. The corresponding $u_c$ is $0.8$ as marked by the vertical dotted line in (b), where the long time value $M_{\infty}$ is plotted against $u$. $M_0$ denotes the the total $M$ at $t=0$. (c-d) Final distribution of initially prepared maximally excited array of dimers in the $\varepsilon, n$ plane for $J=0.05$. Below $u_c$ the nearly uniform state remains stable, as seen in (c), while above $u_c$ it evolves into a dispersed ensemble of many different single-dimer configurations, scattered over the array.}
\label{joson_stability}
\end{figure}

\end{document}


\section{Introduction}
Throughout this paper, all spaces are separable metric spaces
and maps are
continuous
functions. Let $\N$ be the set of all nonnegative integers, i.e., $\N
=\{0,1,2,...\}$ and let $\Z$ be  the set of all integers and $\R$ the real line.

A map $h:X \to Y$  is an {\it embedding} if $h:X\to h(X)$ is a homeomorphism.
A pair $(X,T)$ is called a {\it one-sided dynamical system} (abbreviated as {\it dynamical system})  if $X$ is a separable metric space and $T:X \to X$ is any map. Moreover, if $T:X \to X$ is a
homeomorphism, i.e., invertible, then $(X,T)$ is called a {\it two-sided dynamical system}.

Reconstruction of dynamical systems from a scalar time series is a topic that has been extensively studied. The theoretical basis for methods of recovering dynamical systems on compact manifolds from one-dimensional data was studied by Takens \cite{Tak81,Tak02}.
 In 1981, Takens \cite{Tak81}, by use of Whitney's embedding theorem, proved that under some conditions of (two-sided) diffeomorphisms on a manifold, the dynamical
system can be reconstructed from the observations made with generic functions.

\begin{thm}
{\rm  (Takens' reconstruction theorem for diffeomorphisms)}  Suppose that
$M$ is a compact smooth manifold of dimension $d$. Let
$D^r(M,M)$ be the space of all $C^r$-diffeomorphisms on $M$and $C^r(M,\R)$ the set of
all $C^r$-functions $(r \geq 1)$. If $E$ is the set of all pairs $(T,f) \in D^r(M,M)\times C^r(M,\R)$
such that the delay observation map
$I_{T,f}^{(0,1,2,..,2d)}:M\to \R^{2d+1}$  defined  by
$$x \mapsto (fT^j(x))_{j=0}^{2d}$$
is an embedding, then $E$ is open and dense in $D^r(M,M)\times C^r(M,\R)$.
\end{thm}

Moreover, in 2002 Takens \cite{Tak02}, extended his theorem for
 endomorphisms on compact  smooth manifolds as follows.

\begin{thm}{\rm  (Takens' reconstruction theorem for endomorphisms)} Suppose that
$M$ is a compact smooth manifold of dimension $d$. Then there is an open dense subset ${\mathcal U}\subset {\rm End}^1(M)\times C^1(M,\R)$, where  $ {\rm End}^1(M)$ denotes the space of all $C^1$-endomorphisms on $M$, such that, whenever $(T,f)\in {\mathcal U}$, there is a map $$\pi:I_{T,f}^{(0,1,..,2d)}(M)\to M$$ with $\pi\cdot I_{T,f}^{(0,1,..,2d)}=T^{2d}$.

\end{thm}

Embeddings of two-sided dynamical systems in the two-sided shift $(\R^{\Z},\sigma)$ have been studied by many authors (e.g. see \cite{Coo15, Gut15, Gut16, GQS18, GT14, Jaw74, Lin99, LW00, Ner91, SYC91, Tak81}).

In \cite{Kat20}, we studied embeddings of one-sided dynamical systems  in the one-sided shift $(\R^{\N},\sigma)$.
 In this paper, by use of the topological methods introduced in the  paper \cite{Kat20}, we extend the above Takens' reconstruction theorems of dynamical systems on compact manifolds to  theorems of  one-sided dynamical systems for a large class of compact metric spaces.  The main results of this paper are Theorem 5.4 and Corollary 6.9.

  In this paper, we do not assume injectivity
of $T$ and  so the proofs of our results cannot any longer rely on the embedding theorems of Whitney and Menger-N\"{o}beling \cite{Eng95}.  Instead, an essential role is played by the  notion defined in Definition 2.1.  \\
\\

\section{Definitions and notations}

For a space $X$, $\dim X$ means the topological (covering)
dimension of $X$
(e.g. see \cite{Eng95}, \cite{HW41} and \cite{Nag65}).
Let $X$ be compact metric space and $Y$ a space with a complete
metric $d_Y$.
Let $C(X,Y)$ denote the space consisting of all maps $f: X \to
Y$. We equip
$C(X,Y)$ with the metric $d$ defined by $$d(f,g)=\sup_{x\in
X}d_Y(f(x),g(x)).$$
Recall that $C(X,Y)$ is a complete metric space and hence
Baire's category
theorem holds in $C(X,Y)$.

A map $g:X \to Y$ of separable metric spaces is {\it $n$-dimensional}
~$(n=0,1,2,...)$ if $\dim g^{-1}(y)\leq n$ for
each $y \in Y$.  Note that a closed map $g:X \to Y$ is 0-dimensional if and only if for any 0-dimensional subset $D$ of $Y$, $\dim g^{-1}(D)\leq 0 $ (see \cite[Hurewic's theorem (1.12.4)]{Eng95}). A map $T:X\to X$ is {\it doubly 0-dimensional} if for each closed set $A\subset X$ of dimension 0, one has $\dim T^{-1}(A) \leq 0$ and $\dim T(A)=0$.

 If
$K$ is a subset of a space $X$, then $\mathrm{cl}(K)$,
$\mathrm{bd}(K)$ and
$\mathrm{int}(K)$ denote the closure, the boundary and the
interior of
$K$ in $X$, respectively. A subset $A$ of a space $X$ is an
$F_{\sigma}$-set of
$X$ if $A$ is a countable union of closed subsets of $X$. Also,
a subset $B$ of
$X$ is a $G_{\delta}$-set of $X$ if $B$ is an intersection of
countably many  open
subsets of $X$.

An indexed family $(C_s)_{s\in S}$ of subsets of a set $X$ will by abuse  of notation also be denoted by $\{C_s\}_{s\in S}$ or $\{C_s: s\in S\}$. Hence if $\mathcal{C}=\{C_s\}_{s\in S}$ is such a family then its members $C_s$ and $C_t$ will be considered as different whenever $s\ne t$. We then put
$$\mathrm{ord}(\mathcal{C})= \sup \{\mathrm{ord}_x(\mathcal{C}): x\in X\}
\mbox{, where } \mathrm{ord}_x (\mathcal{C})=|\{s\in S|~x \in C_s\}|.$$
Note that $\mathrm{ord}(\mathcal{C})$ so defined is by  1 larger than it would be according to the usual definition, as e.g. in \cite[(1.6.6) Definition]{Eng95}.  \\

Modifying the definition of TSP in \cite{Kat20}, we define the notion of
$(k,\eta)$ trajectory-separation property for $k \in \N$ and $\eta >0$ which is very  important in this paper.

\begin{defn}
Let $T: X \to X$ be a map of a compact metric space $X$ with
$\dim X = d < \infty$ and let $k\in \N, \eta >0$. Then $T$ has the $(k,\eta)$ {\it
trajectory-separation property} $((k,\eta)$-TSP for short$)$ provided that
there is a closed set $H$ of $X$
such that \\
$(1)$ $X\setminus  H$ is a union of finitely many disjoint open sets
 of  diameter at most $\eta$,  and \\
$(2)$ $\mathrm{ord}\{T^{-p}(H)\}_{p=0}^k \leq d$.

\end{defn}

\section{reconstruction spaces of dynamical systems}

For a space $K$, we consider the (one-sided) shift $\sigma:
K^{\N} \to
K^{\N}$ which is defined by
$$\sigma (x_0,x_1,x_2,x_3....) = (x_1,x_2,x_3....), ~x_i \in
K.$$
Let $(X,T)$ and $(X',T')$ be dynamical systems.  If a map $h: X\to X'$  satisfies $hT=T'h$,
then we say that  $h: (X,T)\to (X',T')$ is a {\it morphism} of dynamical systems.

In this paper, we need the following definition from \cite{Kat20}.

\begin{defn} Let $T:X\to X$ be a map of a compact metric space $X$.\\
$(a)$ Given a set $S \subset \N$ and a map $f:X \to \R$, the map $(fT^j)_{j\in S}: X \to \R^S$ will be denoted by $I^S_{T,f}$. We call this map {\it the delay observation map at times} $j\in S$.  Note that $I_{T,f}:=I_{T,f}^{\N}:(X,T)\to (\R^{\N},\sigma)$ is a morphism of dynamical systems. We call $I_{T,f}$ the infinite delay observation map for $(T,f)$. \\
$(b)$ We say that $I_f^S$ is a {\it trajectory-embedding} if  $I_f^S(x)\neq I_f^S(y)$ whenever $T^j(x)\neq T^j(y)$ for all $j \in S$.
\end{defn}

Remark 1. $(1)$ In the statement of Theorem 1.2, the existence of such a map $\pi$ is equivalent to that $I_{T,f}^{(0,1,...,2d)}$ is a trajectory-embedding. \\
$(2)$  In the statement $(b)$ of Definition 3.1, for the case where $T:X\to X$ is injective,
$I_{f}^S$ is an embedding if and only if $I_{f}^S$ is a trajectory-embedding. \\

 Let $(X,T)$ be a dynamical system of a compact metric space $X$.
For $n\geq 1$, let $P_n(T)$ be the set of all periodic points of $T$
with period $\leq n$
 and $P(T)$ the set of all periodic points of $T$, i.e.
$$P_n(T)=\{x\in X|~\mbox{there is an}~i ~\mbox{such that}~1\leq i\leq
n~\mbox{and}~T^{i}(x)=x\} $$
$$\mbox{and}~ P(T)=\bigcup_{n\geq 1}P_n(T).$$
Two points $x$ and $y$ of $X$ are {\it trajectory-separated} for $T$ if $T^j(x)\neq T^j(y)$
for $j\in \N$. A morphism $h:(X,T)\to (X',T')$ is a {\it trajectory-monomorphism} if
 $h(x), h(y)$ are trajectory-separated for $T'$, whenever $x, y \in X$ are
  trajectory-separated for $T$.

 For $x,y \in X$, let $o_T (x)=(T^i(x))_{i\in \N}$ and $o_T (y) = (T^i(y))_{i\in \N}$ be two orbits of $T$. We say that the orbit $o_T(x)$  is
{\it eventually equivalent} to the orbit $o_T(y)$ if the orbits will be equal in the future, i.e.,
there exists an $n \in \N$ such that $T^i(x)=T^i(y)$  for each $i\geq n$. In this case, we
wright $o_T(x) \sim_e o_T(y)$. We see that this relation is an equivalence relation. So we
have the equivalence class
$$[o_T(x)]=\{o_T(y)|~ o_T(x) \sim_e o_T(y)\}$$
containing $o_T (x)$ and we put
$$[O(T)] = \{[o_T (x)]|~ x \in X\}.$$ Note that if $T:X \to X$ is injective, the function $o:X\to [O(T)]$ defined by $x \mapsto [o_T(x)]$ is bijective, i.e.,  $o: X \cong [O(T)]$.
Also, note that if $h:(X,T)\to (X',T')$ is a morphism of dynamical
systems, then $h$ induces the function $h:[O(T)] \to  [O(T')]$
defined by $h([o_T(x)])=[o_{T'}(h(x))]$ for $x\in X$. A morphism $h:(X,T)\to (X',T')$ of dynamical systems is a {\it trajectory-isomorphism} if $h$ induces the bijection $h:[O(T)] \cong  [O(T')]$.

\begin{prop}
Suppose that a morphism  $h: (X,T)\to (X',T')$ is a trajectory-monomorphism and  $h$ is surjective, i.e., $h(X)=X'$.  Then  $h$ is a trajectory-isomorphism:
$$h:[O(T)]\cong [O(T')]$$
\end{prop}

\begin{proof}
Since  $h$ is a trajectory-monomorphism, $h$ induces an injective  function from $[O(T)]$ to $[O(T')]$.
Also $h$ induces a surjective function from $[O(T)]$ onto $[O(T')]$, because that
$h$ is a surjective function.
\end{proof}

We need the definition of topological entropy and we give the definition  by Bowen \cite{Bow78}.
Let $T:X\to X$ be any map of a compact metric space $X$.
A subset $E$ of X is $(n,\epsilon)$-separated
if for any $x,y \in E$ with $x\neq y$, there is an integer $j$
 such that $0 \leq j < n$ and
$d(T^j(x),T^j(y)) \geq \epsilon$. If $K$ is any nonempty closed subset of $X$,
$s_n(\epsilon;K)$ denotes the
largest cardinality of any set $E\subset K$ which is $(n,\epsilon)$-separated.
Also we define
$$s(\epsilon;K)=\limsup_{n\to \infty}\frac{1}{n}\log s_n(\epsilon;K),$$
$$h(T;K)=\lim_{\epsilon \to 0}s(\epsilon;K).$$
It is well known that the topological entropy $h(T)$ of $T$ is equal to $h(T;X)$ (see
\cite{Bow78}).

Now, we will introduce the notion of {\it reconstruction space}  of   dynamical systems.

\begin{defn}
A compact metric space $X$ is a reconstruction space of   dynamical systems if there exists a $G_{\delta}$-dense set $E$ of $C(X,X)\times C(X,\R)$ such that for $(T,f) \in E$,  the infinite delay observation map  $$I_{T,f}:=I_{T,f}^{\N}:(X,T) \to (\R^{\N},\sigma)$$  satisfies the following conditions (1) and (2):\\
$(1)$ $I_{T,f}:[O(T)] \cong [O(\sigma_{T,f})]$, where  $\sigma_{T,f}=\sigma|I_{T,f}(X)$, and \\
$(2)$ $h(T)=h(\sigma_{T,f})$.
\end{defn}

We show that many compact metric spaces (e.g. PL-manifolds, branched manifolds, Menger manifolds, Sierpi\'nski carpet, Sierpi\'nski gasket and many fractal sets) are reconstruction spaces of dynamical systems. Our result means that almost all dynamical systems $(X,T)$ on a reconstruction space $X$ can be reconstructed from (observation) maps $f:X\to \R$ in the sense of  `eventually equivalent orbits', and so it forms a bridge between the theory of nonlinear dynamical
systems and nonlinear time series analysis.\\

\section{Trajectory-embeddings in $(\R^{\N},\sigma)$}
In this section, we study some fundamental properties of trajectory-embeddings.

\begin{prop} Let $(X,T)$ be a dynamical system and $f:X\to \R$ a map. Let  $k\in \N$ and suppose that
$I_{T,f}^{(0,1,..,k)}:X\to \R^{k+1}$ is a trajectory-embedding.
Then the following properties  $(1)$-$(3)$ hold.  \vspace{2mm}\\
$(1)$
There is the unique map  $\sigma_{T,f}^{(0,1,..,k)}: I_{T,f}^{(0,1,..,k)}(X)\to I_{T,f}^{(0,1,..,k)}(X)$ such that
 $I_{T,f}^{(0,1,..,k)}T=\sigma_{T,f}^{(0,1,..,k)}I_{T,f}^{(0,1,..,k)}$.

In other words, the  map $\sigma_{T,f}^{(0,1,..,k)}$ defined by $(fT^i(x))_{i=0}^k) \mapsto (fT^i(x))_{i=1}^{k+1}) ~ (x \in X)$ is well-defined.
And $I_{T,f}^{(0,1,..,k)}:(X,T)\to (I_{T,f}^{(0,1,..,k)}(X),\sigma_{T,f}^{(0,1,..,k)})$ is a  trajectory-isomorphism. In particular,  $I_{T,f}:=I_{T,f}^{\N}:(X,T) \to (R^{\N},\sigma)$ is a
 trajectory-monomorphism. \vspace{1mm}\\
$(2)$ Let  $p_{(0,1,..,k)}:\R^{\N} \to \R^{k+1}$ be the projection defined by $(x_i)_{i\in \N} \mapsto (x_i)_{i=0}^{k}$. Then
$p_{(0,1,..,k)}:(I_{T,f}(X),\sigma_{T,f}) \to (I_{T,f}^{(0,1,..,k)}(X),\sigma_{T,f}^{(0,1,..,k)})$ is an isomorphism of dynamical systems, i.e., $p_{(0,1,..,k)}$ is a homeomorphism.  \vspace{1mm}\\
$(3)$ $h(T)=h(\sigma_{T,f})=h(\sigma_{T,f}^{(0,1,..,k)})$.
\end{prop}

\begin{proof} We prove $(1)$.
Let $x, y\in X$ with $(fT^i(x))_{i=0}^k=(fT^i(y))_{i=0}^k$. We show that $(fT^i(x))_{i=1}^{k+1}=(fT^i(y))_{i=1}^{k+1}$.
 Since $I_{T,f}^{(0,1,..,k)}$ is  a trajectory-embedding, we see that $T^k(x)=T^k(y)$. In particular, $T^{k+1}(x)=T^{k+1}(y)$ and so $fT^{k+1}(x)=fT^{k+1}(y)$. This implies that $(fT^i(x))_{i=1}^{k+1}=(fT^i(y))_{i=1}^{k+1}$. Thus  $\sigma_{T,f}^{(0,1,..,k)}$ is well-defined. Also, since $I_{T,f}^{(0,1,..,k)}:X \to \R^{k+1}$ is a trajectory-embedding, we see that the morphism
$$I_{T,f}^{(0,1,..,k)}:(X,T)\to (I_{T,f}^{(0,1,..,k)}(X),\sigma_{T,f}^{(0,1,..,k)})$$ is a trajectory-isomorphism.

We will prove $(2)$. Note that
$p_{(0,1,..,k)}(I_{T,f}(X))=I_{T,f}^{(0,1,..,k)}(X)$. Suppose that $I_{T,f}^{(0,1,..,k)}(x)=I_{T,f}^{(0,1,..,k)}(y)~(x, y \in X)$, i.e.,
$(fT^i(x))_{i=0}^{k}=(fT^i(y))_{i=0}^{k}$. Since $I_{T,f}^{(0,1,..,k)}$ is  a trajectory-embedding, as before we see that  $T^k(x)=T^k(y)$ and so
$$I_{T,f}(x)=(fT^i(x))_{i \in \N}=(fT^i(y))_{i \in \N}=I_{T,f}(y).$$ This implies that $p_{(0,1,..,k)}: I_{T,f}(X)\to I_{T,f}^{(0,1,..,k)}(X)$ is a homeomorphism.

We prove (3).  Recall that $I_{T,f}^{(0,1,..,k)}T=\sigma_{T,f}^{(0,1,..,k)}I_{T,f}^{(0,1,..,k)}$.
By Bowen's theorem (e.g. see \cite[Theorem 7.1]{MS93}), we have
$$h(\sigma_{T,f}^{(0,1,..,k)}))\leq h(T)\leq h(\sigma_{T,f}^{(0,1,..,k)})+\sup\{h(T;(I_{T,f}^{(0,1,..,k)})^{-1}(z))|~z\in Z\}.$$
Let $z=(fT^i(x))_{i=0}^k~(x\in X)$. Since $I_{T,f}^{(0,1,..,k)}: X \to \R^{k+1}$ is a trajectory-embedding, we see that
$$T^{k}((I_{T,f}^{(0,1,..,k)})^{-1}(z))=\{T^k(x)\}$$ is a one point set, and  so $h(T;(I_{T,f}^{(0,1,..,k)})^{-1}(z))=0$. Hence
$h(T)=h(\sigma_{T,f}^{(0,1,..,k)})$. By (2), $h(T)=h(\sigma_{T,f}^{(0,1,..,k)})=h(\sigma_{T,f})$.
\end{proof}

 By Proposition 4.1 and \cite[Theorem 3.1]{Kat20}, we have the following result.

\begin{thm}
Let $X$ be a compact metric space with
$\dim X = d <
\infty$
and let $T: X \to X$ be  a doubly 0-dimensional map with $\dim
P(T) \leq 0$. Then there is a dense $G_{\delta}$-set $D$ of
$C(X,\R)$ such that for all $f \in D$,
$$I_{T,f}=T_{T,f}^{\N}:(X,T) \to (\R^{\N},\sigma)$$  satisfies the three conditions: \\
$(a)$ $I_{T,f}:[O(T)] \cong [O(\sigma_{T,f})]$, \\
$(b)$ $h(T)=h(\sigma_{T,f})$ and \\
$(c)$ if $x, y\in X$ are trajectory-separated for $T$, then
$$|\{i\in \N|~I_{T,f}(x)_i=I_{T,f}(y)_i\}|\leq 2d.$$

\end{thm}

\section{Reconstruction theorem in the one-sided shift $(\R^{\N},\sigma)$}

Let $X, Y$ be compact metric spaces and let $\varphi:X\to 2^Y\cup \{\emptyset \}$ be a set-valued function, where $2^Y$ denotes the set of all nonempty closed subsets
of $Y$. Then  $\varphi:X\to 2^Y\cup \{\emptyset \}$ is {\it upper semi-continuous} if
for any $x\in X$ and any open neighborhood $V$ of $\varphi(x)$ in $Y$, there is an open neighborhood $U$ of $x$ in $X$ such that $\varphi(x') \subset V$ for any $x'\in U$.

Let $(X,T)$ be any one-sided dynamical system.  A point $x\in X$ is a {\it chain recurrent point} of $T$ if for any $\epsilon >0$
there is a finite sequence $x=x_0,x_1,\cdots,x_m=x~(m\geq 1)$ of points of $X$ such that
$d(T(x_i),x_{i+1}) < \epsilon$  for
each $i=0,1,\cdots,m-1$.  Let $CR(T)$ be the set of all chain recurrent points of $T$. Note
that $P(T) \subset CR(T)$, $CR(T)$ is a nonempty closed subset of $X$ and the
set-valued function
$$CR : C(X,X) \to 2^X, ~~T  \mapsto  CR(T)$$
is upper semi-continuous (see \cite{BF85}).

We will define the following class 0-$\mathcal{DCR}$ of compact metric spaces.
\begin{defn}
Let 0-$\mathcal{DCR}$ be the class  of all compact metric spaces $X$ satisfying  the following two  conditions: \\
$(0$-$\mathcal{D})$ The set of  doubly 0-dimensional maps $T:X \to X$ is dense in $C(X,X)$. \\
$(0$-$\mathcal{CR})$ The set of maps $T: X \to X$ with  $\dim CR(T)=0$ is dense in $C(X,X)$.
\end{defn}

Remark 2. Note that for a compact metric space $X$, both the set  of  0-dimensional maps $T:X\to X$  and the set of maps $T:X \to X$ with  $\dim CR(T)=0$ are $G_{\delta}$-sets of $C(X,X)$ (e.g. see \cite{KOU16}). So note that if $X$ belongs to 0-$\mathcal{DCR}$,  then the set  of  all maps $T:X\to X$ such that $T$ is a 0-dimensional map with $\dim CR(T)=0$ is a dense $G_{\delta}$-set of $C(X,X)$. \\

Let $A$ be a (nonempty) closed subset of a compact metric space $X$.
Here we need the following notion:
$D(A) < \eta$  if $A$ can be decomposed into finitely many mutually disjoint closed sets $A_i$ with diam$(A_i) < \eta$ for each $i$, i.e. $A=\bigcup_i A_i$,  diam$(A_i) < \eta$, and $A_i\cap A_j=\emptyset$ for $i \neq j$. Note that $\dim A=0$ if and only if
$D(A)< \eta$ for each $\eta >0$.

Modyfying the proof of \cite[Lemma 3.11]{KM20}, we have the following.

\begin{lem} {\rm (c.f. \cite[Lemma 3.11]{KM20})}  Let $\eta >0$ and $k\in \N$.
Suppose that $T: X \to X$ is a doubly 0-dimensional map of a
compact metric space $X$
such that $\dim X = d < \infty$ and
$D(\mathrm{cl}[\cup_{p=0}^{4k} T^{-p}(P(T))]) < \eta$. Then  $T$ has $(k,\eta)$-TSP.
\end{lem}

\begin{proof}
Since $D(\mathrm{cl}[\cup_{p=0}^{4k} T^{-p}(P(T))]) < \eta$,  there is
an open cover $\mathcal{C} = \{C_i \mid
1\leq i \leq M \}$ of $X$ such that \\
$(a)$~ $\mathrm{diam} (C_i) < \eta$ for each  $1\leq i \leq M$, and \\
$(b)$~$\mathrm{bd}(C_i)\cap (\mathrm{cl}[\cup_{p=0}^{4k} T^{-p}(P(T)))])=\emptyset$ for each $1\leq i \leq M$.

Put $K=\bigcup_{i=1}^M\mathrm{bd}(C_i)$. Then by (b) there is an open neighborhood $K'$ of $K$ in $X$ such that for any point $z \in K'$, $T^t(z)\cap T^{t'}(z)=\emptyset$ for $-2k\leq t \leq 2k$.  \\
By modyfying the proof of \cite[Lemma 3.11]{KM20}, we see that
there is
an open cover  $\mathcal{C}'= \{C'_i \mid
1\leq i \leq M \}$ of $X$ such that \\
$(1)$ $ C'_i \subset C_i$ for each $1\leq i \leq M$, and \\
$(2)$ $\mathrm{ord}\{ f^{-p} (\mathrm{bd}(C'_i)) \mid 1\leq i \leq M, p=0,1,...,k \} \leq d$, and \\
 $(3)$
$\mathrm{bd}(C'_i) \cap (\mathrm{cl}[\cup_{p=0}^{4k} T^{-p}(P(T))]) = \emptyset$ for each $1\leq i \leq M$. \\

 Put $c'_1 = \mathrm{cl}(C'_1),$
$c'_i =
\mathrm{cl}(\mathrm{int} [(C'_i) \setminus (\bigcup_{j <i}C'_{j})])$
for $2 \leq i \leq M$. We define
$$H=\bigcup_{i=1}^M\mathrm{bd}(c'_i)~\mbox{and}~
U_i=\mathrm{int}(c'_i)~(i=1,2,..,M).$$
Then $H$ satisfies the desired conditions of $(k,\eta)$-TSP.
\end{proof}

\begin{lem}{\rm (A version of Borsuk's homotopy extension theorem, c.f.
\cite[(8.1)Theorem]{Bor67} and \cite[Theorem 4.1.3]{Mil01}) }
Let $X$ be a compact metric space and $M$ a closed subset of
$X$, and let maps $f', g': M \to \R^k$  satisfy $d(f',g')<\epsilon$. If $g:X\to \R^k$ is an extension of $g'$, then $f'$ has an extension $f:X \to \R^k$ such that $d(f,g)<\epsilon$.
\end{lem}

Let $X$ be any compact metric space. For each $\alpha >0$ and $S\subset \N$ a set of cardinarity $2d+1$, let   $E(\alpha;S)$ be the subset of
$C(X,X)\times C(X,\R)$ consisting of all pairs $(T,f)$ such that  $I_{T,f}^S: X \to  \R^{S}$
is an $\alpha$ {\it trajectory-embedding} (i.e., $I^S_{T,f}(x)\neq I^S_{T,f}(y)$  whenever $x,y \in X$ with $d(T^j(x),T^j(y))\geq \alpha$ for all $j\in S$).

The main theorem of this paper is the following.

\begin{mainthm} {\rm (Reconstruction theorem of dynamical systems)} Let $X$ be a
 compact metric space with $\dim X=d$. Suppose that $X$ belongs to the class 0-$\mathcal{DCR}$.Then the following assertions  $(1)-(3)$  hold.\vspace{2mm}\\
$(1)$ {\rm ($\alpha$ trajectory-embedding)}  Let  $\alpha >0$ and $S\subset \N$ a set of cardinarity $2d+1$. Then the set $E(\alpha;S)$ is a dense open set of $C(X,X)\times C(X,\R)$. \vspace{1mm}\\
$(2)$ {\rm (Trajectory-embedding)} There exists a $G_{\delta}$-dense set $E$ of $C(X,X)\times  C(X,\R)$ such that if $(T,f) \in E$, for any $S\subset \N$ of cardinality $2d+1$
 $$I_{T,f}^S: X \to  \R^{S}$$ is a trajectory-embedding.  \vspace{1mm} \\
$(3)$  {\rm (Infinite delay observation)} If $E$ is the set as in the above (2), then for any $(T,f) \in E$,
$$I_{T,f}=T_{T,f}^{\N}:(X,T) \to (\R^{\N},\sigma)$$  satisfies the following conditions: \\
\hspace*{3mm} $(a)$ $I_{T,f}:[O(T)] \cong [O(\sigma_{T,f})]$, \\
\hspace*{3mm} $(b)$ $h(T)=h(\sigma_{T,f})$ and \\
\hspace*{3mm} $(c)$ if $x, y\in X$ are trajectory-separated for $T$, then
$$|\{i\in \N|~I_{T,f}(x)_i=I_{T,f}(y)_i\}|\leq 2d.$$

In particular, $X$ is a reconstruction space of dynamical systems.
\end{mainthm}

\begin{proof}
 We prove (1). Let $\alpha >0$ and $S \subset \N$ of cardinality $2d+1$.
 For each $T\in C(X,X)$,  we put
$$L(T:\alpha,S) =$$ $$\{(x,y)\in X\times X |~d(T^{j}(x),T^{j}(y))\geq \alpha~\mbox{for}~j \in S\} \subset X\times X.$$
Recall the set
$$E(\alpha;S)=$$ $$\{(T,f)\in C(X,X)\times C(X,\R)|I_{T,f}^S(x)\neq I_{T,f}^S(y)~\mbox{for}~(x,y)\in L(T:\alpha,S) \}. $$

We will show that $E(\alpha,S)$ is an open subset of $C(X,X)\times C(X,\R)$. Let
$(T,f)\in E(\alpha,S)$. Since $L(T:\alpha,S)$ is compact, we can choose a neighborhood $K$ of $L(T:\alpha,S)$ and  $\epsilon >0$ such that for any $(x,y)\in K$,
$$d(I_{T,f}^S(x),I_{T,f}^S(y))\geq 2\epsilon.$$
Note that the $$L(\alpha,S): C(X,X)\to 2^{X\times X}\cup \{\emptyset\}, T \mapsto
L(T:\alpha,S)$$  is an upper semi-continuous set-valued function. We can choose a neighborhood $U(T)$ of $T$ in $C(X,X)$ and a neighborhood
$V(f)$ of $f\in C(X,\R)$ such that if $(T',f') \in U(T) \times V(f)$, then
$L(T':\alpha,S) \subset K$ and for $(x,y) \in K$,
$$d(I_{T',f'}^S(x), I_{T',f'}^S(y))\geq \epsilon.$$
Since $L(T':\alpha,S) \subset K$,  we see that
$I_{T',f'}^S(x)\neq I_{T',f'}^S(y)$
for $(x,y) \in L(T':\alpha,S)$. Then $(T',f') \in E(\alpha,S)$ and so
$U(T)\times V(f) \subset E(\alpha,S)$. Hence $E(\alpha,S)$ is an open set
of $C(X,X)\times C(X,\R)$.

Next, we will show that $E(\alpha,S)$ is dense in $C(X,X)\times C(X,\R)$.
 Let $(T,f) \in C(X,X)\times C(X,\R)$ and $\epsilon >0$.
 Since $f:X\to \R$ is uniformly continuous, there is a sufficiently small positive number
 $\eta >0$ such that $\eta < \alpha$ and if $x,y\in X$ with $d(x,y)<\eta$,
  then $d(f(x),f(y))<\epsilon$. Let $k=\max S$.
 By Remark 2, we can choose $T_1 \in C(X,X)$ such that  such that $T_1$ is  a
 0-dimensional map, $d(T,T_1)<\epsilon/2$ and $\dim CR(T_1)=0$.  Since  $\dim (\cup_{p=0}^{4k} T_1^{-p}(CR(T_1)))=0$, we choose a closed neighborhood $W$ of
  $\cup_{p=0}^{4k} T_1^{-p}(CR(T_1))$ in $X$ with $D(W)<\eta$. Since the set function $CR: C(X,X) \to 2^X$ is upper semi-continuous and $X$ satisfies the condition 0-$\mathcal{D}$ of Definition 5.1,
  we can choose a dubly 0-dimensional map $T_2\in C(X,X)$ such that $d(T_1,T_2)< \epsilon/2$ and $\cup_{p=0}^{4k} T_2^{-p}(CR(T_2))\subset W$. Then   $D(\cup_{p=0}^{4k} T_2^{-p}(CR(T_2))) < \eta$ and so $D(\mathrm{cl}[\cup_{p=0}^{4k} T_2^{-p}(P(T_2))]) < \eta$.  By Lemma 5.2, we see that $T_2$ has $(k,\eta)$-TSP.   Hence
there is a closed set $H$ of $X$
such that \\
$(1)$ $X\setminus  H$ is a union of finitely many disjoint open sets
 of  diameter at most $\eta$,  and \\
$(2)$ $\mathrm{ord}\{T_2^{-p}(H)\}_{p=0}^k \leq d$.

We choose a small open neighborhood $G$ of $H$ in $M$  such that \\
 $ (2')$ $\mathrm{ord}\{T_2^{-j}(G)\}_{j=0}^k \leq d.$\\
Then we may assume that $X\setminus \mathrm{cl}(G)$ is a union of  disjoint open sets
$V_i (i = 1,2,...,m)$ such that $\mathrm{cl}(V_i) \subset U_i$.
 Note that
$ \mathrm{cl}(V_i) \cap \mathrm{cl}(V_j)=\emptyset (i \neq j)$. For each $i$, take a point $t_i$ which belongs to a sufficiently
small neighborhood of $f(\mathrm{cl}(V_i))$ in $\R$ such that $t_i\neq t_j$ if $i\neq j$. We define a map
$$g': \bigcup_{i=1}^m \mathrm{cl}(V_i) \to \R$$
by $g'(\mathrm{cl}(V_i))=t_i$. Then by Lemma 5.3, we have an extension
$g: X \to \R$ of $g'$ with $d(g,f)<\epsilon$.
We will prove $(T_2,g) \in E(\alpha,S)$. Let $(x,y) \in L(T_2:\alpha,S)$. By (d'),
$$|\{j \in S|~T_2^{j}(x) \in G\}|\leq d$$ and
$$|\{j \in S|~T_2^{j}(y) \in G\}|\leq d.$$
Since $|S|=2d+1$, we can find some $j \in S$  such that $T_2^{j}(x), T_2^{j}(y) \in X\setminus G$.
Since $d(T_2^{j}(x),T_2^{j}(y)) \geq \alpha$ and $\mathrm{diam}(\mathrm{cl}(V_i)) <\eta <\alpha$ for each $i=1,2,..,m$,
there are $n, n'$ such that $n\neq n'$ and $T_2^{j}(x) \in \mathrm{cl}(V_n)$ and
$T_2^{j}(y) \in \mathrm{cl}(V_{n'})$.
Then $gT_2^{j}(x)=t_n \neq t_{n'}=gT_2^{j}(y)$.  This implies $I_{T_2,g}^S(x)\neq I_{T_2,g}^S(y) $
 and hence $$(T_2,g)\in E(\alpha,S).$$
Note that $d(T,T_2) <\epsilon$ and $d(f,g) < \epsilon$. So we see that $E(\alpha,S)$ is a dense open set of
$C(X,X)\times C(X,\R)$.

We will prove $(2)$. Let $J$ be the set of all set $S \subset \N$ of cardinality $(2d+1)$.
 Note that $J$ is a countable set. We define
$$E=\bigcap\{E(1/n,S)|~S\in J ~\mbox{and} ~n\in \N\setminus \{0\} \}.$$
Then we see that $E$ is a desired dense $G_{\delta}$-set in $C(X,X)\times C(X,\R)$.

Finally we will prove (3). Let $(T,f)\in E$. Note that if $k=2d$, then $(T,f)$ satisfies the conditions of Proposition 4.1.  Hence $$I_{T,f}:[O(T)] \cong [O(\sigma_{T,f})] ~\mbox{and}~h(T)=h(\sigma_{T,f}).$$ Let  $x, y\in X$ be trajectory-separated points for $T$. Suppose, on the contrary, that $$|\{i\in \N|~I_{T,f}(x)_i=I_{T,f}(y)_i\}|> 2d.$$ Then we can choose a set $S' \subset \{i\in \N|~I_{T,f}(x)_i=I_{T,f}(y)_i\}$ with $|S'|=2d+1$. This is a contradiction to the fact that  $I_{T,f}^{S'}$ is  a trajectory-embedding.

This completes the proof.

\end{proof}

\section{The class 0-$\mathcal{DCR}$}
In this section, we consider  the following general problem.

\begin{prob}
What kinds of  compact metric spaces belong to the class 0-$\mathcal{DCR}$ ?
\end{prob}

We will show that PL-manifolds, some branched manifolds and some fractal sets, e.g. Menger manifolds, Sierpi\'{n}ski carpet, Sierpi\'nski  gasket and dendrites, belong to the class 0-$\mathcal{DCR}$.

In \cite{KOU16} Krupski, Omiljanowski and
Ungeheuer defined the class 0-$\mathcal{CR}$ which is the family of all compact metric spaces $X$ such that the set $CR(T)$ is 0-dimensional for a generic map $T\in C(X,X)$.
They proved the following result.

\begin{thm}{\rm (\cite[Theorem 5.1]{KOU16})} If $X$ is a (compact) polyhedron, then  $X\in 0$-$\mathcal{CR}$. Moreover,  if $X$ is a compact metric space that admits an $\epsilon$-retraction $r_{\epsilon}:X\to P$ onto a polyhedron $P\subset X$ for each $\epsilon >0$ (i.e., $d(r_{\epsilon}, id_X)<\epsilon$ and $r_{\epsilon}|P=id_P$),
then $X\in 0$-$\mathcal{CR}$.
\end{thm}

Now, we will consider  the family  0-$\mathcal{D}$ of all compact metric spaces $X$ such that all doubly 0-dimensional maps on $X$ is dense in $C(X,X)$.
A map $T:X \to X$ is said to be  a {\it piecewise embedding} if there is a countable family $\{F_i\}_{i\in \N}$ of closed subsets of $X$ such that $X=\bigcup_{i\in \N} F_i$ and $T|F_i:F_i\to X$ is injective for each $i\in \N$. Note that if  a map $T:X \to X$ is a piecewise embedding, then $T$ is doubly 0-dimensional because that  $\dim T^{-1}(x)$ is a countable set for each $x \in X$ and  $$\dim T(A)=\max\{\dim T(A\cap F_i)~|~i\in \N\}\leq 0$$ for any 0-dimensional closed set $A$ of $X$ (see the countable sum theorem for dimension  \cite[Theorem 3.1.8]{Eng95}).

A (compact) $d$-dimensional  polyhedron $P~(d\geq 1)$ is  called a {\it manifold with branch structures} if $P=\bigcup_{j\in J}M_j\cup M$, where \\
$(1)$ $\{M_j\}_{j\in J}$ is a finite family of  mutually disjoint closed sets  of $P$ such that   for each $j\in J$,
$$M_j=N_j \cup_{\varphi_{\alpha}}\bigcup \{N_{j,\alpha}|\alpha \in J_j\},$$ where
 $J_j$ is a finite set, $N_j, N_{j,\alpha}~(\alpha \in J_j)$ are $d$-dimensional manifolds with boundaries, and $M_j$ is obtained from $N_j$ by attaching $N_{j,\alpha}~(\alpha \in J_j)$ via locally embedding maps $\varphi_{\alpha}: N'_{j,\alpha}  \to \partial N_j$ from a $(d-1)$-dimensional (compact) submanifold  $N'_{j,\alpha}$ of  $\partial N_{j,\alpha}$ into $\partial N_j$, i.e., $M_j$ is the quotient space of the topological sum $N_j \amalg_{\alpha\in J_j} N_{j,\alpha}$ under the identifications $ x \sim \varphi_{\alpha}(x)$ for $x\in N'_{j,\alpha}\subset \partial N_{j,\alpha}$ and  the quotient map is denoted by $q_j: N_j \amalg_{\alpha\in J_j} N_{j,\alpha} \to M_j~(=N_j \cup \bigcup\{q_j(N_{j,\alpha})|~\alpha \in J_j\})$, \\
$(2)$ $M$ is a $d$-dimensional compact manifold in $P$  with $$M\cap \bigcup\{\varphi_{\alpha}(N'_{j,\alpha})~|~ j\in J, \alpha \in J_j\}=\emptyset$$ and \\
$(3)$  $P\setminus  \bigcup\{\varphi_{\alpha}(N'_{j,\alpha})~|~ j\in J, \alpha \in J_j\}$ is a $d$-dimensional (non-compact) manifold.\\

Remark. All PL-manifolds and some branched manifolds are  manifolds with branch structures. The associated template of the well-know Lorenz attractor is a manifold with branch structures \cite{GL02}. \\

Let $K$ be a simplicial complex and let $K^{(m)}$ be the $m$-skeleton of $K$, i.e., the set of all simplexes of $K$ whose dimension are $\leq m$. For a vertex $v$ of $K^{(0)}$, let $\mathrm{St}(v,K)$ be the closed star of $v$, i.e., $\mathrm{St}(v,K)=\bigcup\{\sigma \in K|~v \in \sigma \}$. Also
let $\beta K$ denote the barycentric subdivision of $K$. Let $\Delta=<p_0,p_1,\cdots,p_n>$ and $\sigma=<v_0,v_1,...,v_n>$ be $n$-simplexes and let $J$ be the set of all sequence $\{\star\}=s_0, s_1, \cdots, s_n=\sigma$ of faces of $\sigma$ such that $s_{i-1}$ is a face of $s_i$ and $\dim s_{i-1}+1=\dim s_i$  for $i=1,2,...,n$. Then $|J|=(n+1) !$ and
$$\sigma=\bigcup\{<b(s_0),b(s_1),\cdots,b(s_n)>|~(s_0,s_1,\cdots ,s_n) \in J \},$$ where $b(s_i)$ is  the barycenter of $s_i$. Consider the {\it folding map (at barycenters)}
 $f_{\sigma}:|\beta\sigma| \to \Delta$ which is the simplicial map defined by $f_{\sigma}(b(s_i))=p_i$ for each $i=0,1,2,...,n$. Note that  $f_{\sigma}$ is a piecewise embedding.

\begin{prop}
Let $P$ be a manifold with branch structures. Then the set of all piecewise embedding maps $T: P\to P$ is dense in  $C(P,P)$. In particular, $P$ belongs to
 0-$\mathcal{DCR}$. Hence $P$ is a reconstruction space of dynamical systems.
\end{prop}

\begin{proof}  Let $\dim P=d\geq 1$. Since $P$ is a polyhedron, by Theorem 6.2, $P$ belongs to  the class
0-$\mathcal{CR}$. We will show that $P$ belongs to the class 0-$\mathcal{D}$.
Let $T\in C(P,P)$ and $\epsilon>0$. We choose a simplicial complex $K$ of $P$ such that   $\mathrm{mesh}(K)$  is sufficiently small, i.e., $\mathrm{mesh}(K)<\epsilon/2$. Take a simplicial approximation $T_1: P=|L|\to |K|$ of $T$ such that
$d(T,T_1)<\epsilon/2$, where $L$ is a subdivision of $K$.

By modifying $T_1$, we will construct a map $T'_1:|\beta L|\to P$ such that
for each $d$-simplex $s$ of $\beta L$, $T'_1|s:s\to P$ is an embedding and $d(T_1,T_1')<\epsilon$. We consider the following abstract simplicial complex $\tilde{K}$ which contains the  simplicial complex $K$ as follows: For each $0\leq k\leq d-1$, let $$J_k=\{(a_0,a_1,..,a_k)\in \N^{k+1}~|~d=k+\Sigma_{i=0}^k a_i\}.$$ For each $k$-simplex $\sigma=<v_0,v_1,...,v_k> ~(k\leq d-1)$ of $K$ and  each $(a_0,a_1,..,a_k)\in J_k$, we consider the abstract $d$-simplex
$$<v_0,v_1,...,v_k;(a_0,a_1,..,a_k)>$$  $$=<p_{(v_0,0)},p_{(v_0,1)}
,..,p_{(v_0,a_0)},p_{(v_1,0)},p_{(v_1,1)},..,p_{(v_1,a_1)},\cdots,p_{(v_k,0)},p_{(v_k,1)}..,p_{(v_k,a_k)}>$$
where we assume $v_{i}=p_{(v_i,0)}\in K^{(0)}~(i=0,1,...,k)$. In particular,
 $$<v;d>=<p_{(v,0)},p_{(v,1)},...,p_{(v,d)}>$$
 for each vertex $v \in K^{(0)}$, where $v=p_{(v,0)}$.  We define the abstract simplicial complex $\tilde{K}$ as follows:
$$\tilde{K}=K\bigcup \{s~| s ~\mbox{is a face of }<v_0,v_1,...,v_k;(a_0,a_1,..,a_k)>, 0\leq k\leq d-1, $$ $$ (a_0,a_1,..,a_k)\in J_k,
\mbox{and} <v_0,v_1,...,v_k> \in K^{(k)}\setminus K^{(k-1)}\}.$$
For each $0\leq k \leq d-1$, we put
$$A_k=\bigcup\{<v_0,v_1,...,v_k;(a_0,a_1,..,a_k)>| <v_0,v_1,...,v_k>\in K^{(k)}\setminus K^{(k-1)}, $$ $$ (a_0,a_1,..,a_k)\in J_k\}.$$

We will construct a retraction $r:|\tilde{K}|\to |K|$ such that $$r|<v_0,v_1,...,v_k;(a_0,a_1,..,a_k)>$$ is injective. Recall that $P=|K|$ is a manifold with branch structures.
So we assume that $$P= \bigcup_{j\in J}M_j \cup M, M_j=N_j \cup_{\varphi_{\alpha}}\bigcup \{N_{j,\alpha}|\alpha \in J_j\},$$
$N'_{j,\alpha}, \varphi_{\alpha}$ and $q_j$ are defined as above.

By induction on $k~(0\leq k\leq d-1)$,  we will construct $h_k:\cup_{i=0}^kA_i \to |K|$.
First we will construct a map $h_0:A_0\to |K|$ as follows.
Let $v\in K^{(0)}$.

 If $v \notin  \bigcup\{\varphi_{\alpha}(N'_{j,\alpha})~|~ j\in J, \alpha \in J_j\},$
we choose an embedding $$h_0:<v;d>(=<p_{(v,0)},p_{(v,1)},...,p_{(v,d)}>)\to P\setminus  \bigcup\{\varphi_{\alpha}(N'_{j,\alpha})~|~ j\in J, \alpha \in J_j\}$$
 with $h_0(v)=v$, because that $P\setminus  \bigcup\{\varphi_{\alpha}(N'_{j,\alpha})~|~ j\in J, \alpha \in J_j\}$ is a $d$-dimensional (non-compact) manifold.

If $v\in \varphi_{\alpha}(N'_{j,\alpha})$ for some $j\in J, \alpha \in J_j$, we choose an embedding $$h_0:<v;d> \to N_j$$  with $h_0(v)=v$, because that $N_j$ is a $d$-dimensional manifold.
So we have a map $h_0:A_0\to |K|$.

Now we assume that
$h_{k-1}:\cup_{i=0}^{k-1}A_{i}\to |K|$ have been constructed.
Let $<v_0,v_1,...,v_k>$ be a $k$-simplex of $K$.

If  $<v_0,v_1,...,v_k>$ is contained in $P\setminus  \bigcup\{\varphi_{\alpha}(N'_{j,\alpha})~|~ j\in J, \alpha \in J_j\}$, then we can choose an embedding
  $$h_k:<v_0,v_1,...,v_k;(a_0,a_1,..,a_k)> \to P\setminus  \bigcup\{\varphi_{\alpha}(N'_{j,\alpha})~|~ j\in J, \alpha \in J_j\}$$  satisfying the following conditions $(a)$ and $(b)$:\\
 $(a)$ $h_k|<v_0,v_1,...,v_k>=id$ and \\
 $(b)$
$$h_k|A_{k-1}\cap <v_0,v_1,...,v_k;(a_0,a_1,..,a_k)>= $$ $$h_{k-1}|A_{k-1}\cap <v_0,v_1,...,v_k;(a_0,a_1,..,a_k)>.$$

If $<v_0,v_1,...,v_k>$ is contained in $N_j$ for some $j\in J$ and
$$<v_0,v_1,...,v_k>\cap \bigcup\{\varphi_{\alpha}(N'_{j,\alpha})~|~ j\in J, \alpha \in J_j\}\neq \emptyset,$$
 then we choose  an embedding  $h_k:<v_0,v_1,...,v_k;(a_0,a_1,..,a_k)> \to N_j$  satisfying  $(a)$ and $(b)$ as above.

 If  $<v_0,v_1,...,v_k>$ is contained in $q_j(N_{j,\alpha})$ and  $<v_0,v_1,...,v_k>$  intersects with  $\partial N_j$,  then we choose an embedding $$h_k:<v_0,v_1,...,v_k;(a_0,a_1,..,a_k)> \to  N_j \cup q_j(N_{j,\alpha})$$ satisfying  $(a)$ and $(b)$ as above,
 because that as the assumption of the case $k-1$, we can assume that $$h_{k-1}( A_{k-1}\cap \partial<v_0,v_1,...,v_k;(a_0,a_1,..,a_k)>)$$ is contained in a $d$-dimensional manifold in $N_j \cup q_j(N_{j,\alpha})$.

By induction on $k$, we obtain $h_{d-1}$. And by use of $h_{d-1}$ we have a retraction $r:|\tilde{K}|\to |K|$ such that $r|<v_0,v_1,...,v_k;(a_0,a_1,..,a_k)>$ is injective.

Next, we will define a PL-map $\varphi: |L| \to |\tilde{K}|$ which is a piecewise embedding.
For  each $d$-simplex $\sigma$ of $L$, we consider the simplex
$$T_1(\sigma)=<v_0,v_1,...,v_k> \in K~(k\leq d).$$
For each vertex $v_i$ of $T_1(\sigma)$, we consider the face
$$T^{-1}(v_i)\cap \sigma=<w_{(i,0)},w_{(i,1)},..,w_{(i,a_i)}>=\sigma_{v_i}$$ of $\sigma$. Note that
$d=k+\Sigma_{i=0}^k a_i$ and
$$\sigma=<w_{(v_0,0)},..,w_{(v_0,a_0)},w_{(v_1,0)},..,w_{(v_1,a_1)},\cdots,w_{(v_k,0)},..,w_{(v_k,a_k)}>$$
$$\equiv \sigma_{v_0}*\sigma_{v_1}*\cdots *\sigma_{v_k}.$$
We put $$ \beta\sigma_{v_0}*\beta\sigma_{v_1}*\cdots *\beta\sigma_{v_k}=\{\tau_0*\tau_1\cdots *\tau_k|~\tau_i\in \beta\sigma_i, \dim \tau_i=a_i\}.$$
Then $ \beta\sigma_{v_0}*\beta\sigma_{v_1}*\cdots *\beta\sigma_{v_k}$ gives a subdivision of $\sigma$.
 Consider the (abstract) $d$-simplex $$\Delta_{\sigma}=<v_0,v_1,...,v_k;(a_0,a_1,..,a_k)>$$ $$=<p_{(v_0,0)},..,p_{(v_0,a_0)},p_{(v_1,0)},..,p_{(v_1,a_1)},\cdots,p_{(v_k,0)},..,p_{(v_k,a_k)}>$$
of $\tilde{K}$
 and consider the folding map
$$f_{\sigma_{v_i}}: |\beta\sigma_{v_i}| \to \Delta_{v_i}=<p_{(v_i,0)},..,p_{(v_i,a_i)}>~(\in \tilde{K})$$ defined as above.

For each  $d$-simplex $\sigma$ of $L$, we have a map
$$\varphi_{\sigma}=f_{\sigma_{v_0}}* f_{\sigma_{v_1}} \cdots * f_{\sigma_{v_k}}: $$ $$\sigma= |\beta\sigma_{v_0}*\beta\sigma_{v_1}*\cdots *\beta\sigma_{v_k}| \to \Delta_{v_0}*\Delta_{v_1}*\cdots *\Delta_{v_k}=\Delta_{\sigma} \in \tilde{K}.$$
Note that if $\dim T_1(\sigma)=d$, $\varphi_{\sigma}=T_1|\sigma$.

By use of
$\varphi_{\sigma}$, we have a desired PL map $\varphi: |L| \to |\tilde{K}|$ which is a piecewise embedding.
Finally, we put $T_1'=r\varphi: P\to P$. Then $T_1'$ is a piecewise embedding. Also by the constraction of $r$, we may assume that $d(T_1,T_1')<\epsilon/2$. This means that $P$ satisfies the condition (0-$\mathcal{D})$.
 This completes the proof.
\end{proof}

Many  dynamical properties of Cantor sets have been studied by many authors. Now we consider dynamical properties of higher dimensional fractal sets.

 For $0\leq k < n$, we will construct  a space $L^n_k$  in the $n$-simplex $M_0=<v_0,v_1,...,v_n>$ by Lefshetz's method (see \cite[p.129]{Chi96} and \cite{Lef31}).
We define a sequence $\{(M_i,L_i)\}_{i\in \N}$ of compact $n$-dimensional polyhedra $M_i$ with triangulations $L_i$ inductively as follows.
Let $M_0$ be the $n$-simplex $<v_0,v_1,...,v_n>$ with the standard simplicial complex structure $L_0$.
Suppose $(M_i,L_i)$ has been defined. Let
$$M_{i+1}=\bigcup\{{\mathrm St}(v,\beta^2(L_i))~|~v \mbox{ is a vertex of }~ \beta(L_i^{(k)}) \}$$ and $$L_{i+1}=\beta^2L_{i}|M_{i+1}.$$  Note that $M_{i+1}$ may be regarded as a regular neighborhood of the $k$-skeleton of $L_i$.
Then $\{M_i\}_{i\in \N}$ is a decreasing sequence and we obtained a compact metric space $$L^n_k=\bigcap_{i\in \N}M_i.$$
 Note that $L^1_0$ is a Cantor set and $L^{2d+1}_d~(=\mu^d)$ is called  the $d$-dimensional {\it Menger compactum}. Also $L^2_1$ is called the {\it Sierpi\'{n}ski carpet}.
A space $X$ is a $d$-dimensional {\it Menger manifold} if $X$ is compact and each point $x$ of $X$ has a neighborhood $W$ of $x$ in $X$ such that $W$ is homeomorphic to the $d$-dimensional Menger  compactum $\mu^d$ (for many geometric properties of $\mu^d$, see \cite{Bes88}).

Also the  Sierpi\'{n}ski gasket can be constructed from an equilateral triangle by repeated removal of (open) triangular subsets: Start with an equilateral triangle. Subdivide it into four smaller congruent equilateral triangles and remove the central (open) triangle.
Repeat this step with each of the remaining smaller triangles infinitely. So we have a sequence $\{X_i\}_{i\in \N}$ of continua in the plane and the intersection $X=\bigcap_{i\in \N}X_i$ is called the {\it Sierpi\'{n}ski gasket}.

A compact connected metric space (=continuum) $X$ is said to be a {\it dendrite} if $X$ is a 1-dimensional locally connected continuum which contains no simple closed curve.

\begin{prop} Let $M$ be a $d$-dimensional Menger manifold. Then  $M$ belongs to  0-$\mathcal{DCR}$ and hence $M$ is a reconstruction space. More precisely, there exists a $G_{\delta}$-dense set $E'$ of $C(M,M)\times  C(M,\R)$ such that if $(T,f) \in E'$, then for any $S\subset \N$ of cardinality $2d+1$, $I_{T,f}^S: M \to  \R^{S}$ is an embedding and so
 $$I_{T,f}=T_{T,f}^{\N}:(M,T) \to (\R^{\N},\sigma)$$  is an embedding.
\end{prop}

\begin{proof} By  \cite[Definition 1.2.1 and Corollary 5.2.2]{Bes88},  for each $\epsilon >0$, $M$ admits an $\epsilon$-retraction $r_{\epsilon}:M\to P$ onto a $d$-dimensional polyhedron $P\subset M$. Hence by Theorem 6.2, $M$ belongs to 0-$\mathcal{CR}$. Also it is well-known that the set $e(M,M)$ of all embeddings $T: M\to M$ is  a $G_{\delta}$ dense set of $C(M,M)$ (see  \cite[Theorem 2.3.8]{Bes88}). Hence
$M$ belongs to  0-$\mathcal{DCR}$. Recall the proof of Theorem 5.4. We can complete the latter part of the proof by replacing $C(M,M)$  with $e(M,M)$.
\end{proof}

We will show that the  Sierpi\'{n}ski carpet belongs to  0-$\mathcal{DCR}$. In \cite[p.323]{Why58}, Whyburn proved that the  Sierpi\'{n}ski carpet is homeomorphic to any $S$-curve $X$ (=plane locally connected 1-dimensional continuum whose complement  in the plane consists of countably many components with frontiers being mutually disjoint  simple closed curves $\{S_i\}_{i\in \N}$, and moreover, if $K_1, K_2$ are $S$-curves and $C_1, C_2$ are frontiers of  components of complements of $K_1, K_2$ in the plane $\R^2$, respectively, then each homeomorphism of $C_1$ onto $C_2$ can be extended to a homeomorphism of $K_1$ onto $K_2$.
Such simple closed curves $\{S_i\}_{i\in \N}$ are called the {\it  rational circles} of  the $S$-curve $X$. The union of all these circles $\{S_i\}_{i\in \N}$ is called the {\it rational part} of  $X$, and the remainder $X\setminus (\bigcup_{i\geq 0} S_i)$ is called the  {\it irrational part} of $X$. We need the following lemma.

\begin{lem}
Let $X$ be an $S$-curve in the plane $\R^2$ and let  $\{S_i\}_{i\in \N}$ be  rational circles of  $X$, and $S_0$ the frontier of the unbounded component of $\R^2 \setminus X$. Let $B_k~(k\geq 1)$ be the disk in $\R^2$ with $\partial B_k=S_k$. If $p:\R^2 \to H$ is
 the decomposition map of $\R^2$ obtained by identifying the sets $B_1, B_2,...$ to single points respectively, then the decomposition space $H$ is homeomorphic to $\R^2$, $p(X)=D$ is a disk in the plane $H$ with $\partial D=p(S_0)$, and
 the set $\{p(S_i)~|i=1,2,..\}$ is a countable set in  $D\setminus \partial D$. Moreover, for a point $x$ of $X\setminus S_0$, $x$ is in the  irrational part of $X$ if and only if $p^{-1}(p(x))=\{x\}$.
\end{lem}

\begin{proof} By the Moore's theorem \cite[p.380]{Kur61}, we see that
$H$ is homeomorphic to $\R^2$ and $p(X)=D$ is a disk. Note that the set $\{p(S_j)| j\geq 1\}$ is a countable set in the disk $D$.
\end{proof}

\begin{prop} Let $X=L^2_1\subset \R^2$ be the  Sierpi\'{n}ski carpet. Then  $X$ belongs to  0-$\mathcal{DCR}$.
\end{prop}

\begin{proof} Let $\epsilon >0$.  Recall the Lefshetz's construction of
$L^2_1$ as above.  We see that $M_{i+1}$ is regarded as a regular neighborhood of the $1$-skeleton of $L_i$. So we can easily see that  $X$ admits an $\epsilon$-retraction $r_{\epsilon}:X\to |L_i^{(1)}|$ for a sufficiently large $i\in \N$.  Hence $X$ belongs to 0-$\mathcal{CR}$.

We will show that $X$ belongs to the class 0-$\mathcal{D}$. Let $T\in C(X,X)$ and  $\epsilon >0$.   Let $M_0=\Delta_2$ be a 2-simplex with the standard simplicial complex structure $L_0$.
We have the sequence $(M_i,L_i)$ defined as above, i.e.,
$$M_{i+1}=\bigcup\{{\mathrm St}(v,\beta^2(L_i))~
|~v \mbox{ is a vertex of }~ \beta(L_i^{(1)}) \}$$ and $$L_{i+1}=\beta^2L_{i}|M_{i+1}.$$
Then
$L^2_1=\bigcap_{i\in \N}M_i.$
Note that
${\mathrm St}(v,\beta^2(L_i))$ is a disk in $\R^2$ and
 ${\mathrm St}(v,\beta^2(L_i))\cap X$ is an $S$-curve. Choose  a sufficiently large natural number $i_0$ so that
 $\mathrm{diam ~St}(v,\beta^2(L_{i_0}))<\epsilon$ for each vertex $v$ of
 $\beta(L_{i_{0}}^{(1)})$. Put $D_v=\mathrm{St}(v,\beta^2(L_{i_0}))$.

Let $\{S_k\}_{k\in \N}$ be the family of rational circles of the $S$-curve $X$ such that
$S_k \subset \mathrm{int}_{\R^2}M_{i_0+1}$ and  $B_k$ is the disk with $\partial B_k=S_k$  for each $k\in \N$.   Let $p:\R^2 \to H$ be
 the decomposition map of $\R^2$ obtained by identifying the sets $B_1, B_2,...$ to single points respectively. Then  $p(D_v)$ is a disk in the plane $H$. So   we have a family $$\{p(D_v)~|~v \mbox{ is a vertex of }~ \beta(L_{i_0}^{(1)}) \}$$ of disks in $H$  such that  $$p(M_{i_0+1})=\bigcup \{p(D_v)~|~v \mbox{ is a vertex of }~ \beta(L_{i_0}^{(1)}) \}$$  and
$\mathrm{ord}(\{p(D_v)~|~v \mbox{ is a vertex of }~ \beta(L_{i_0}^{(1)}) \})\leq 2$. Since the set $Z=\{p(S_k)~|k\in \N\}$ is a countable set in $p(M_{i_0+1})$,  we have a disk $E_v$ in $ p(M_{i_0+1})$ such that  \\
$(1)$ $\partial E_v \cap Z=\emptyset$, \\
$(2)$ $p(D_v)\subset \mathrm{int}_{p(M_{i_0+1})}E_v$, \\
$(3)$ $\mathrm{diam}~p^{-1}(E_v)<\epsilon$ and \\
$(4)$ $\mathrm{ord}\{E_v|~v \mbox{ is a vertex of }~ \beta(L_{i_0}^{(1)}) \} \leq 2$.

If necessary, by use of homeomorphism of $\R^2$ we may assume that $H=\R^2$ and each $E_v$ is a convex set in $H$.  Put $D'_v=p^{-1}(E_v)\cap X$.
Choose a large natural number  $j_0\geq i_0$ such that for each 2-simplex $\sigma$ of $L_{j_0}$, there is a vertex $v$ of  $\beta(L_{i_0}^{(1)})$ such that  $T(\sigma \cap X) \subset  \mathrm{int}_{X}D'_v$.  For  each $w \in  L_{j_0}^{(0)}$,
we put  $$V(w)=\{v |~v \mbox{ is a vertex of }~ \beta(L_{i_0}^{(1)})
~\mbox{and}~ T(w)\in D'_v\}.$$
Note that $1\leq |V(w)|\leq 2$. Since $Z$ is a countable set in $H=\R^2$ and by use of usual general position arguments in the plane, we see that for any  $w \in  L_j^{(0)}$, take a point ${\tilde w}$ of the irrational part of $\bigcap\{D'_v|~v \in V(w)\}$ such that
\\
$(5)$ if $w, w' \in  L_j^{(0)}$ and $w\neq w'$, then ${\tilde w}\neq {\tilde w'}$, \\
$(6)$ the set $\{p({\tilde w}) ~|w\in  L_j^{(0)}\}$ is in general position of the plane $H=\R^2$
and the segment $[p({\tilde w}), p({\tilde w'})]$ in $\R^2$ contains no point of $Z$.\\

Let $\sigma$ be any 2-simplex in $L_{j_0}$  with $\sigma=<w_0,w_1,w_2>$. Consider the 2-simplex $\tilde{\sigma}$ in $H=\R^2$ such that $\tilde{\sigma}^{(0)}=\{p(\tilde{w}_0),p(\tilde{w}_1),p(\tilde{w}_2)\}$. Consider a natural homeomorphism $h_{\sigma}: \partial  \sigma \to p^{-1}(\partial \tilde{\sigma})$ with $h_{\sigma}(w_i)=\tilde{w}_i$. Since $\sigma\cap X$ and $p^{-1}(\tilde{\sigma})\cap X$ are $S$-curves, by Whyburn theorem as above there is a homeomorphism
$\varphi_{\sigma}: \sigma \cap X \to p^{-1}(\tilde{\sigma})\cap X$ which is an extension of $h_{\sigma}$. By use of $\varphi_{\sigma}$,  we have a desired piecewise embedding $T':X\to X$ with $d(T,T')<\epsilon$.
Hence
$X$ belongs to  0-$\mathcal{D}$.
\end{proof}

\begin{prop} Let $X$ be the Sierpi\'{n}ski gasket. Then  $X$ belongs to  0-$\mathcal{DCR}$.
\end{prop}
\begin{proof} Let $\epsilon >0$.
We see that $X$ admits an $\epsilon$-retraction $r_{\epsilon}:X\to P$ onto a subgraph  $P$ of  $X$ and so $X$ belongs to 0-$\mathcal{CR}$. We will show that $X$ belongs to the class 0-$\mathcal{D}$.
Let $T\in C(X,X)$ and $\epsilon >0$. Since $T$ is uniform continuous, we choose a sufficiently small positive number  $0<\delta<\epsilon$ such that $d(T,Tr_{\delta}) <\epsilon$, where $r_{\delta}$ is a $\delta$-retraction.  Note that $X$ is a countable union of segments $J_n~(n\in \N)$ in $\R^2$ and also we can choose such a retraction $r_{\delta}$ such that  $r_{\delta}|J_n$ is injective, and hence
 it is a doubly 0-dimensional map. Consider the map
$r_{\delta}T|P:P\to P$. Since $P$ is a graph and hence it is a 1-dimensional manifold with branch structures,
 we have a piecewise embedding map $g:P\to P$ such that $d(g,r_{\delta}T|P)<\epsilon.$ Then
$$d(T,gr_{\delta})\leq d(T,Tr_{\delta})+d(Tr_{\delta},r_{\delta}Tr_{\delta})+d(r_{\delta}Tr_{\delta},gr_{\delta})<3\epsilon$$ and $gr_{\delta}$ is a doubly 0-dimensional map.
Hence
$X$ belongs to  the class 0-$\mathcal{DCR}$.
\end{proof}

\begin{prop} Let $X$ be any dendrite. Then  $X$ belongs to  0-$\mathcal{DCR}$.
\end{prop}

\begin{proof} Since $X$ is a dendrite, we see that  for each $\epsilon >0$, $X$ admits an $\epsilon$-retraction $r_{\epsilon}:X\to P$ onto a subtree $P$ of  $X$. Hence $X$ belongs to 0-$\mathcal{CR}$ (see also \cite{KOU16}). We will show that $X$ belongs to the class 0-$\mathcal{D}$.  Note that $X$ is a countable union of arcs $J_n~(n\in \N)$ and we can choose such a retraction $r_{\epsilon}$ such that  $r_{\epsilon}|J_n$ is injective and hence
 it is a doubly 0-dimensional map. By the same arguments as the proof of Proposition 6.7, we see that
$X$ belongs to  0-$\mathcal{D}$.
\end{proof}

\begin{cor} Let $X$ be one of the following spaces: PL-manifold, manifold with branch structures, Menger manifold, Sierpi\'nski carpet, Sierpi\'nski gasket and dendrite. Then  $X$ is a reconstruction space of dynamical systems.
\end{cor}

\section{Application: Reconstructions of one-sided dynamical systems
from nonlinear time series analysis}
There have been attempts to reconstruct dynamical models directly from data, and nonlinear methods for the analysis of time series data have been extensively investigated. This research is an inverse problem to the numerical analysis of dynamical systems model, in that it seeks to identify models that fit data.

Time-delay embedding is well-known for nonlinear time series analysis, and it is used
in several research fields such as physics, meteorology, informatics, neuroscience
and so on. In laboratories, experimentalists are
striving to find principles of phenomenons from a lot of data and they use delay embedding for reconstructing the dynamical systems from experimental time series. For smooth dynamical systems on manifolds, the celebrated Takens'
reconstruction theorem ensures validity of the delay embedding analysis. Takens'
 theorem means that many dynamics theoretically can be  reconstructed  by the
delay coordinate system, more precisely almost all (two-sided) dynamical systems can be
reconstructed from observation maps (see Takens \cite{Tak81,Tak02} and Sauer,Yorke and Casdagli \cite{SYC91}). So Takens'  theorem is the basis for nonlinear time series analysis and  form a bridge between the theory of nonlinear differential dynamical systems on smooth manifolds and nonlinear time series analysis.

However, unfortunately the systems may not to be two-sided and moreover, they may not be  systems on manifolds. Recently we freqently encounter a situation where  we have to study dynamical systems of spaces that cannot have differential structure. In natural sciences and physical engineering, there has been an increase in importance of fractal sets and more complicated spaces, and also in mathematics, the dynamical properties and stochastic analysis of such spaces have been studied by many authors. Our reconstruction theorem theoretically ensures validity of the delay embedding analysis for (topological) dynamical systems on such complicated compact metric spaces,
i.e., almost all one-sided dynamical systems $(X,T)$ of  spaces $X$ belonging to 0-$\mathcal{DCR}$ can be reconstructed from observation maps $f:X\to \R$ in the sense of  "trajectory embedding", i.e., the delay observation
map  $$I_{T,f}^{(0,1,2,\cdots,k)}: (X,T) \to (I_{T,f}^{(0,1,2,\cdots,k)}(X),\sigma_{T,f}^{(0,1,\cdots k)})$$
is a trajectory-embedding for a natural number $k \geq 2\dim X$, and so  the dynamical system
$$(I_{T,f}^{(0,1,2,\cdots,k)}(X),\sigma_{T,f}^{(0,1,2,\cdots,k)})$$ may reflect many dynamical properties of the original dynamical system $(X,T)$. Especially, $$I_{T,f}:[O(T)]\cong [O(\sigma_{T,f}^{(0,1,2,\cdots,k)})]~ \mbox{and}~ h(T)=h(\sigma_{T,f}^{(0,1,2,\cdots,k)}).$$  In laboratories, experimentalists may
understand how the system $(X,T)$ will go in the future in the sense of orbital
classification  from the analysis of experimental time series. More precisely, for $x,y \in X$, if one can find a time $n\in \N$ such that $$|\{i\in \N|~fT^i(x)=fT^i(y), 0\leq i \leq n \}|=2\dim X+1,$$ then $T^j(x)=T^j(y)$ for $j\geq n$ and hence $[o_T(x)]=[o_T(y)]$.

For more general case where a $d$-dimensional compact metric space $X$ does not belong to 0-$\mathcal{DCR}$ and $(X,T)$ is any one-sided dynamical system, we have an  extension $(\mu^d,T')$ of $(X,T)$, where $\mu^d$ is the $d$-dimensional Menger compactum containing $X$ and $T':\mu^d \to \mu^d$ is an extension of $T$  ~(see \cite{Bes88}). By Proposition 6.4, there is a possibility to be able to investigate the approximate properties of the dynamical system $(X,T)$ by use of time-delay embedding of the dynamical system $(\mu^d,T')$.  \\

{\bf Acknowledgments:}  This work was supported by JSPS KAKENHI
Grant Number JP19K03485.