A simpler encoding of indexed types

Tesla Zhang
The Pennsylvania State University

In functional programming languages, generalized algebraic data types (GADTs) are very useful
as the unnecessary pattern matching over them can be ruled out by the failure of unification of type arguments.
In dependent type systems, this is usually called indexed types and it's particularly useful
as the identity type is a special case of it.
However, pattern matching over indexed types is very complicated as it requires term unification in general.
We study a simplified version of indexed types (called simpler indexed types)
where we explicitly specify the selection process of constructors, and we discuss its expressiveness, limitations,
and properties.

§ INTRODUCTION

Correct-by-construction data structures are pleasant to work with,
such as well-typed and well-scoped syntax trees <cit.>.
A key aspect of correct-by-construction data structures is that they carry value-level
information in their types. We start from two simple instances of such data structures:
the finite set type and the sized vector type,
which are base on the general notion of indexed types[
This piece of code is written in Agda <cit.>.
The types and functions are in blue while constructors are in green.
There are other pieces of code written in Aya <cit.>, where types are in green
and constructors are in purple.
In <ref>, we use the latter coloring.]:

The indices of types are the parameters at the right-hand-side of the colons in the signatures
of inductive types, which can be specialized by constructors.
The two constructors of Fin specify the index as $\AgdaInductiveConstructor{suc}~n$,
so when pattern matching over $\AgdaDatatype{Fin}~\AgdaInductiveConstructor{zero}$ requires no clauses.
The algorithm for selecting constructors is a process of term unification, extracting a most-general-unifier
and apply that to the rest of the telescope.
For each constructor, we unify the type arguments with the indices it specifies,
and there are three potential results <cit.>.

* Success positively – the constructor matches.

* Success negatively – the constructor does not matches.

* Failure – cannot decide, pattern matching cannot be performed.

Users will have to understand the error messages with unification failures,
which is an accidental complexity brought into dependent type systems.
The implementation of the unification algorithm also affects the selection of constructors.

We propose an alternative syntax for indexed types.
First, for inductive types without indices, we use a Haskell-style syntax to describe its arguments,
and we allow bindings in the parameters since we are working with dependent types:

&\kwdata~\Nat:\UU \\[-0.3em]
& \mid~\zerocon \\[-0.3em]
& \mid~\succon~(x:\Nat)
\end{aligned}$

&\kwdata~\Dat{List}~(A:\UU):\UU \\[-0.3em]
& \mid~\cons{nil} \\[-0.3em]
& \mid~\cons{cons}~(x:A)~(xs:\Dat{List}~A)
\end{aligned}$

Then, we allow the constructors to perform a pattern matching over the type of the parameters.
For instance, we define the sized vector type using the following syntax:

\begin{align*}
&\kwdata~\Dat{Vec}~(A:\UU)~(n:\Nat):\UU \\[-0.3em]
& \mid~A,\zerocon~\Rightarrow\cons{vnil} \\[-0.3em]
& \mid~A,\succon~n~\Rightarrow\cons{vcons}~(x:A)~(xs:\Dat{Vec}~A~n)
\end{align*}

This pattern matching is not a traditional pattern matching, say,
it does not need to be covering (although in the $\Dat{Vec}$ example it is)
and it can contain seemingly unreachable patterns (like duplicated patterns).
Instead, they represent the selection process of constructors directly.
The type checking of pattern matching consists of two steps: the well-typedness of
patterns and the exhaustiveness of the patterns.
We exemplify the type checking of our encoding of indexed types by describing
the pattern matching over $\Dat{Vec}~\Nat~n$.
First, it tries to match the terms $\Nat, n$ with the patterns $A, \zerocon$ and $A, \succon~n$.
The pattern matching has three potential results, similar to the term unification problem:

* Success positively – the patterns are matched,
this constructor will be available (needs to be matched).

* Success negatively – the patterns do not match,
this constructor is not available (does not need to be matched).

* Failure – the pattern matching gets stuck, pattern matching cannot be performed.

However, pattern matching is a basic construct in dependent type systems,
and it is decidable and terminating – unlike the general term unification problem,
where we normally give up higher-order cases to avoid undecidability.
It is also more friendly to general users because they are required to understand one concept less.

Another example is the finite set type:

\begin{align*}
&\kwdata~\Dat{Fin}~(n:\Nat):\UU \\[-0.3em]
& \mid~\succon~n~\Rightarrow\cons{fzero} \\[-0.3em]
& \mid~\succon~n~\Rightarrow\cons{fsuc}~(x:\Dat{Fin}~n)
\end{align*}

§.§ Problematic indexed types

We propose the new syntax because the term unification problem
generated by general indexed types could be very complicated.
Here are some examples of indexed types in Agda that generate such unification problems:

These examples are impossible to construct with simpler indexed types.
With the proposed syntax,
we could avoid not only implementing such a complicated unification algorithm,
but also explaining these unification failures in error messages.

§.§ Contributions

* We present the syntax (<ref>) and the type checking algorithm
(<ref>) for simpler indexed types in <ref>.

* We discuss their limitations (<ref>), provide a translation of
simpler indexed types to general indexed types (<ref>),
and discuss the compilation of simpler indexed types (<ref>) in <ref>.

* We explore potential extension to simpler indexed types (<ref>)
and compare it with similar work (<ref>) in <ref>.

§ FORMALIZATION OF SIMPLER INDEXED TYPES

In this section, we describe the core language syntax and the type checking of simpler indexed types.
The coverage checking can be adapted from any other dependent type systems with indexed types
by replacing the term unification with pattern matching, so we assume the existence of a suitable coverage check.

§.§ Core language syntax

The syntax of terms is presented in <ref>.
It has spine-normal fully-applied applications on “definitions”
(including types $\Dat D$, constructors $\cons c$, and functions definitions $\func f$).
Normal constructs such as $\lambda$-abstraction and the $\Pi$-type are also available.
$\Rightarrow$ is used in $\lambda$-abstractions instead of dots for
consistency with function definitions and pattern matching clauses.
We use $\overline u$ to denote a list of expressions, and $\emptyset$ when the list is empty.

\begin{align*}
x,y     ::= & && \text{variable names} \\[-0.3em]
A,B,u,v ::= & \quad \func f~\overline u && \text{full application to functions} \\[-0.3em]
\mid & \quad x~\overline u && \text{application to references} \\[-0.3em]
\mid & \quad \Dat D~\overline u && \text{fully applied inductive type} \\[-0.3em]
\mid & \quad \cons c~\overline u && \text{fully applied constructor} \\[-0.3em]
\mid & \quad (x:A)\to B && \text{$\Pi$-type} \\[-0.3em]
\mid & \quad \lam x u && \text{lambda abstraction}
\end{align*}

Syntax of terms

Case-split expressions can be encoded as functions and can be easily added
to our type theory, but they are unrelated to simpler indexed types. Therefore, we omit them.
We will have two syntactic sugars for the $\Pi$-type: $A \to B$ for $(x:A) \to B$,
and $\Delta \to B$ for $(x_1:A_1) \to (x_2:A_2)\to\cdots\to(x_n:A_n)\to B$
where $\Delta=(\overline{x_i:A_i})_{\forall i\in[1,n]}$.
The latter is only used in <ref>.

The syntax for definitions, contexts and signatures is defined in <ref>.
A signature is a list of declarations and a context is a list of bindings.
Constructors are with or without a list of patterns.
The variables in the same pattern are assumed to be distinct.

\begin{align*}
\Gamma,\Delta,\Theta ::= & \quad \overline{x_i:A_i} && \text{context} \\[-0.3em]
decl ::= & \quad \kwdata~\Dat D~\Delta~\overline{cons} && \text{simpler indexed type} \\[-0.3em]
\mid & \quad \kw{func}~\func f~\Delta:A~\overline{cls} && \text{function definition} \\[-0.3em]
cons ::= & \quad \mid \overline p\Rightarrow \cons c~\Delta && \text{pattern matching constructor} \\[-0.3em]
\mid & \quad \mid \cons c~\Delta && \text{constructor} \\[-0.3em]
cls  ::= & \quad \mid \overline p\Rightarrow u && \text{pattern matching clause} \\[-0.3em]
p, q ::= & \quad \cons c~\overline p && \text{constructor patterns} \\[-0.3em]
\mid & \quad x && \text{catch-all patterns} \\[-0.3em]
\mid & \quad \kw{impossible} && \text{absurd patterns} \\[-0.3em]
\Sigma ::= & \quad \overline{decl} && \text{signature}
\end{align*}

Syntax of signature and declarations

We will borrow some notational convention from <cit.>[
Other styles of substitution include $u[x\mapsto v]$, $u[x/v]$, etc. (there is a relevant online discussion
$u[v/x]$ for substituting occurrences of $x$ with $v$ in term $u$.
We use $u[\overline v/\overline x]$ to denote a list of substitutions applied sequentially
to the term $u$. Substitution objects are denoted as $\sigma$.
We will assume the substitution operation defined on terms, patterns, and substitutions.

In the typing rules in <ref>, we will omit the vertical bars in $cons$ and $cls$
which are intended to separate the clauses and constructors.

§.§ Operations on terms

We also need some operations on terms and patterns.
All of them are defined by induction on the syntax.
We define $\vars\Delta$ to compute the list of variables in $\Delta$:

\begin{align*}
\vars\emptyset &:= \emptyset \\
\vars{x:A,\Delta} &:= x,\vars\Delta
\end{align*}

We define $\vars p$ to compute the list of bindings in pattern $p$
and $\vars{\overline p}$ to gather all the bindings in the patterns $\overline p$.
This operation requires the well-typedness of the patterns because we need the types of the bindings.
We store these types into the patterns to allow accessing them in this operation:

\begin{align*}
\vars{x:A} &:= x:A \\
\vars{\kw{impossible}} &:= \emptyset \\
\vars{\cons c~\overline p} &:= \vars{\overline p} \\
\vars{\emptyset} &:= \emptyset \\
\vars{x:A,\overline p} &:= x:A,\vars{\overline p}
\end{align*}

We define $\toTerm p$ to compute a term that matches exactly the pattern $p$
and $\toTerm{\overline p}$ to compute a list of terms matching exactly the patterns $\overline p$.
This requires $p$ to contain no $\kw{impossible}$ sub-patterns:

\begin{align*}
\toTerm{x:A} &:= x \\
\toTerm{\cons c~\overline p} &:= \cons c~\toTerm{\overline p} \\
\toTerm{\emptyset} &:= \emptyset \\
\toTerm{q,\overline p} &:= \toTerm q,\toTerm{\overline p}
\end{align*}

We define $\matches u p\mapsto \sigma$ to perform pattern matching,
similar to the Match and Matches operations in <cit.>.
It computes a substitution when the pattern matching success positively
and produces $\bot$ when the pattern matching success negatively.
We will also define a version of this operation to match a list of terms with a list
of patterns $\matches{\overline u}{\overline p} \mapsto \sigma$,
similar to $\vars{\overline p}$ and $\toTerm{\overline p}$.

u x ↦[u/x] ∅∅↦[] up ↦σ
c uc p ↦σ up ↦
c uc p ↦ c_1 ≠c_2
c_1 uc_2 p ↦ up ↦
(v,u)(q, p) ↦ v q ↦
(v,u)(q, p) ↦ up ↦σ

v q ↦σ'
(v,u)(q, p) ↦σ⊎σ'

Pattern matching operation

For all pattern $p$, $\matches{\toTerm p} p \mapsto \sigma$ and for all list of patterns
$\overline p$, $\matches{\toTerm{\overline p}}{\overline p} \mapsto \sigma$.
In both formulae, the substitution $\sigma$ is an identity substitution.

By induction on $p$.

§.§ Typing rules for terms

Well-typed terms are formed under the following type checking judgments:

* $\SGvdash \Delta$ $\Delta$ is a well-formed context under $\Sigma;\Gamma$.

* $\SGvdash u:A$ term $u$ has type $A$ under $\Sigma;\Gamma$.

* $\SGvdash \overline u:\Delta$ terms $\overline u$ instantiate context $\Delta$ under $\Sigma;\Gamma$.

* $\SGvdash u=v:A$ terms $u$ and $v$ are equal inhabitants of type $A$ under $\Sigma;\Gamma$.

Typing rules for types and terms are defined in <ref>.
They are grouped by the relevant type formation.

For simplicity, we will omit several things:

* We assume the conversion check between terms –
the problem is the same as other dependent type systems,
and the strategies used by other systems will apply to ours as well.

* We also have the type-in-type rule to simplify the universe types,
and in practical implementations, we could integrate polymorphic universe levels to
make the system consistent.

* In the implementation of Aya and Arend, we also have the sigma type and records,
but we omit them here for simplicity.

Rules related to the $\Pi$-type.

(x:A)→B: func f Δ:A cls∈Σ

f v:A[v/Δ] Σ;Γ,x:A⊢b:B[x/y]x b : (y:A)→B u : (x:A)→B
v:Au v:B[v/x]

Rules related to indexed types.

D Δ cons∈Σ
u : Δ
D u:  D Δ cons ∈Σ

c Δ_c∈cons

c v:D uConCall  D Δ cons ∈Σ

p ⇒c Δ_c∈cons

u p ↦σ

c v:D uIxCall

Rule for convertible types and type-in-type.

A=B : a:B

Typing rules for types and terms

In the IxCall rule, we perform a pattern matching between the type arguments
and the patterns in the constructor to make sure the availability of the selected constructor,
and apply the resulting substitution to the parameters of the constructor as they can access
the patterns according to the rules in <ref>.
In contrast, the ConCall rule does not perform pattern matching and the constructor
is directly available. The differences between IxCall and ConCall include
a successful $\matches u p$ operation and an extra substitution applied on $\Delta_{\cons c}$.

§.§ Signature well-formedness

A well-formed signature consists of a list of well-typed declarations.
We can think of the whole type checking algorithm as a signature formation process.

To check function definitions and pattern matching constructors,
we first need to type check the patterns and elaborate the pattern matching clauses.
The rules of pattern type checking, similar to the operations in <ref>,
have two versions:

* $\SGvdash p : A \mapsto \Theta$ type-checking a pattern $p$ against a type $A$.

* $\SGvdash \overline p : \Delta \mapsto \Theta$ type-checking patterns
$\overline p$ against a context $\Delta$.

These rules are defined in <ref>.
They produce a context $\Theta$ containing all of the bindings in the give pattern(s).

Rules for one pattern.

x : A ↦x:A  D Δ cons∈Σ

c Δ_c ∈cons

p : Δ_c ↦Θ
c p : D u ↦Θ  D Δ cons∈Σ

q ⇒c Δ_c ∈cons

uq ↦σ

p : Δ_cσ↦Θ
c p : D u ↦Θ  D Δ cons∈Σ

(up ↦)_
∀p ⇒c Δ_c ∈cons

c Δ_c ∉cons
impossible : D u ↦Θ

Rules for a list of patterns.

q : A ↦Θ

p : Δ[q/x] ↦Θ'
q,p : (x:A,Δ) ↦Θ⊎Θ' ∅: ∅↦∅

Type checking of patterns

$\SGvdash \overline p : \Delta \mapsto \Theta \implies \SGvdash \toTerm{\overline p} : \Delta$
and  $\SGvdash p : A \mapsto \Theta \implies \SGvdash \toTerm p : A$.

By induction on $p$.

Then, we define the rules for type checking pattern matching structures as in <ref>
using the operation defined in <ref>.

p : Δ↦Θ

Σ;Γ,Δ,Θ⊢u : A[p/Δ]
pΔu A p : Δ↦Θ

Pattern matching structures

With them, we could define the type checking of function definitions and simpler indexed types,
and form signature by the rules $\SGvdash$ in <ref>.
The declarations are checked one after another so latter functions can depend on former ones.
By that, we will lose induction-recursion <cit.> and induction-induction <cit.>,
and we consider it a potential future work.

)_∀(c Δ_c) ∈cons

)_∀(p ⇒c Δ_c) ∈cons
Σ, D Δ cons;

(pΔu A)_∀p⇒u∈cls
Σ,func f Δ :A cls;

Well-formedness of signature $\Sigma$

§ METATHEORY OF SIMPLER INDEXED TYPES

In this section, we discuss the limitations of simpler indexed types by examples and
provide a complete and sound translation from simpler indexed types to general indexed types.

§.§ Limitations and workarounds

Many useful indexed types cannot be written as simpler indexed types.
For instance, as a common illustration of the convenience brought by indexed types,
the normalizer and the syntax tree for an expression language with
natural numbers and booleans can be defined as a general indexed type in Agda <cit.>.

We cannot encode Term as a simpler indexed type because we cannot
pattern match on types, so the direct translation will not work –
We will need an auxiliary type to help us encoding them:

\begin{align*}
&\kwdata~\Dat{TermTy}:\UU~\mid~\cons{natT}~\mid~\cons{boolT} \\
&\kw{func}~\func{termTy}~(x:\Dat{TermTy}):\UU \\[-0.3em]
& \mid~\cons{natT}\Rightarrow \Nat \\[-0.3em]
& \mid~\cons{boolT}\Rightarrow \Dat{Bool}
\end{align*}

Then, we define the type for terms and the normalize function:

\begin{align*}
&\kwdata~\Dat{Term}~(n:\Dat{TermTy}):\UU \\[-0.3em]
& \mid~\cons{natT}~\Rightarrow\cons{nat}~\Nat \\[-0.3em]
& \mid~\cons{natT}~\Rightarrow\cons{succ}~(\Dat{Term}~\cons{natT}) \\[-0.3em]
& \mid~\cons{boolT}~\Rightarrow\cons{bool}~\cons{boolT} \\[-0.3em]
& \mid~\cons{boolT}~\Rightarrow\cons{inv}~(\Dat{Term}~\cons{boolT}) \\[-0.3em]
& \mid~A~\Rightarrow\cons{case}~(\Dat{Term}~\cons{boolT})~(\Dat{Term}~A)~(\Dat{Term}~A) \\
&\kw{func}~\func{normalize}~(t:\Dat{TermTy})~(x:\Dat{Term}~t):\func{termTy}~t \\[-0.3em]
& \mid~\cons{natT},\cons{nat}~n\Rightarrow n \\[-0.3em]
& \mid~\cons{natT},\cons{succ}~n\Rightarrow \succon~(\func{normalize}~\cons{natT}~n) \\[-0.3em]
& \mid~\cons{boolT},\cons{bool}~b\Rightarrow b \\[-0.3em]
& \mid~\cons{boolT},\cons{inv}~b\Rightarrow \func{not}~(\func{normalize}~\cons{boolT}~b) \\[-0.3em]
& \mid~t, \cons{case}~b~x~y\Rightarrow \func{ifElse}~(\func{normalize}~\cons{boolT}~b) \\[-0.3em]
& \hspace*{1em}~(\func{normalize}~t~x)~(\func{normalize}~t~y)
\end{align*}

In the general case, only when the indices are in canonical constructor form (say,
generated by references to parameters of the constructor and applications to constructors)
can we translate them into simpler index types.
Even though we could use auxiliary types to help us encoding them, there is still one
case where this encoding will fail, where the indices contain references
to the parameters of the indexed type. The simplest case is the identity type:

The index being $x$, a reference to the parameter of Id,
is the essential reason why a general term unification needs to be performed
during the pattern matching over idp.
Pattern matching is a mechanism to match terms by patterns, not by terms.

Simpler indexed type essentially simplifies the problem of constructor selection just
by turning the term-match-term problem to a term-match-pattern problem,
which rules out numerous complication but also loses the benefit of general indexed types.
A potential way to bring general indexed types back without introducing them directly is discussed
as future work in <ref>, requiring the presence of a built-in identity type.

§.§ Translation to indexed types

We could translate simpler indexed types back to general indexed types.
To describe the translation, we define the syntax of general indexed types,
which is the output of the translation, in <ref>.
We do not have type parameters as they are just special cases of indices.

\begin{align*}
decl' ::= & \quad \kwdata~\Dat D~\Delta~\overline{cons'} && \text{indexed type} \\[-0.3em]
cons' ::= & \quad \mid \cons c:A && \text{constructor}
\end{align*}

Syntax of general indexed types

Now we can start the translation.
First, we unify pattern matching constructors with simple constructors.
For constructor $\cons c~\Delta_{\cons c}$ in simpler indexed type $\Dat D~\Delta$, we translate
it into a pattern matching constructor $\vars\Delta \Rightarrow \cons c~\Delta_{\cons c}$.

After that, we could perform the translation of constructors.
In other words, we need to construct the type (“$A$” in <ref>) of the translated constructor.

For pattern matching constructor $\overline p \Rightarrow \cons c~\Delta_{\cons c}$,
we construct the type of the translated constructor as
$\vars{\overline p}~\Delta_{\cons c} \to \Dat D~\toTerm{\overline p}$.

This type is a pi type consisting of the following major components:

* $\vars{\overline p}$: the bindings in the patterns. We turn these bindings into
parameters of the translated type.

* $\Delta_{\cons c}$: the constructor parameters. They are typed under the
bindings in $\vars{\overline p}$, so we append the original parameters to the tail
of these required bindings.

* $\Dat D~\toTerm{\overline p}$: the return type. We specialize the indices of
$\Dat D$ with the terms correspond to $\overline p$. These terms are typed under
$\vars{\overline p}$, which is available in the domain of this pi type.

Every simpler indexed type can be translated into general indexed types.

This translation is defined for all simpler indexed types,
so we get the completeness theorem for free.

The type of the translated constructor is well-scoped and well-typed.

First, it indeed returns a specialization of the type $\Dat D$.

According to <ref>, types in $\Delta_{\cons c}$ are well-typed with
references to the bindings in $\overline p$, but not in $\Delta$.
These bindings are available in $\vars{\overline p}$.

According to <ref>, the well-typedness of $\Dat D~\toTerm{\overline p}$
requires $\toTerm{\overline p} : \Delta$, and we know it is true by <ref>.

The translated constructor needs to be matched if and only if the original constructor
needs to be matched.

The translated constructor does not need to be matched if and only if the original
constructor does not need to be matched.

The translated constructor cannot be matched if and only if the original constructor
cannot be matched.

This theorem actually requires a bit more information to be well-defined – we have not given
the general indexed types typing rules and semantics.

However, since the result of $\toTerm{\overline p}$ is only generated by applications to
constructors and references (by definition), we only need to deal with the unification of these terms,
which are quite simple. They should be structurally equivalent to the rules in <ref>.

Restricting the unification problem to this smaller subset makes the soundness theorem provable
by induction on the patterns $\overline p$.

This translation is also useful in the type checking of the constructors of simpler indexed types.
When we have a reference to such constructor without any argument supplied, we could synthesize
a type for this reference – and we use the type in <ref>.

§.§ Compilation and erasure

The compilation of simpler indexed types has an advantage over normal indexed types.
In <cit.>, they used detagging and forcing optimizations to erase the indices during compilation.
These methods are directly expressible in our syntax as the
indices are not even quantified in the constructors (see the examples in <ref>,
where the implicit argument $n$ in the Agda version of
fzero, fsuc
are not present in the corresponding definition as simpler indexed types).
In other words, simpler indexed types enjoy the benefit of index erasure
without any nontrivial compilation technique.

One downside is that there will not be inaccessible patterns <cit.>,
so there will be redundant pattern matching happening at runtime.
Consider the example in <ref>,
the $\func{normalize}$ function using simpler indexed type has two pattern matchings,
while the normalize function using general indexed types has only one.

In conclusion, simpler indexed types are more memory efficient than general indexed types
without optimizations, while they require redundant pattern matchings.
We think of the latter as a potential future work.

§ CONCLUSION

We introduced a simpler encoding of indexed types in dependent type systems.
It reuses the pattern matching for constructor selection to avoid exposing the index
unification problem to the users.
A number of existing indexed types such as Fin and Vect can
be encoded in this simpler way, but not all (exceptions include the identity type in Agda <cit.>
and the examples in <ref>).

§.§ Future work

We could translate simpler indexed types into an even simpler type theory
with only products and coproducts, just like in <cit.>.
This translation requires an algorithm to classify the pattern matching clauses
with overlapping parts. This is done in <cit.>,
but in Aya we have a better implementation. We decide to describe such
translation after the overlapping pattern classification algorithm is formalized.

We could also have a built-in identity type in the type theory and encode the
indexed types with the identity type. The Image type in <cit.> is a great example:

It can be encoded as an inductive type without indices:

\begin{align*}
&\kwdata~\Dat{Image}~(A~B:\UU)~(f:A \to B)~(b:B):\UU \\[-0.3em]
& \mid~\cons{image}~(x:A)~(p:f~x=b)
\end{align*}

We might be able to define a translation from general indexed types into simpler indexed types
with a built-in identity type, and during pattern matching over the encoded types, we perform
a rewriting over the identity proofs that we used to encode the indices.
By that, we will have a different treatment of the index unification problem,
and we could study how it compares to the general indexed types.

This idea (encoding the unification of type indices as a rewriting performed during pattern matching)
is similar to the transpX operation discussed in <cit.>
and the “index-fixing”  operation discussed in <cit.>,
but we are working in a general type theory with any definition of the identity type
as long as they support the J operation, including the path type in homotopy type theory <cit.>,
the path type in cubical type theories <cit.>, the identity type in
intuitionistic type theory <cit.> (either homogeneous or heterogeneous), and others.

The cubical path type is a preferred choice as it does not depend on any fancy unification mechanism.
This means we can develop a type theory expressive enough to discuss indexed types
without dependent pattern matching.

Apart from that, we could seek integration with induction-recursion <cit.>
and induction-induction <cit.> as mentioned in <ref>.

The compilation technique could be investigated to address the limitation discussed in <ref>.

§.§ Related work

Type families in dependent types can be regarded as an encoding of GADTs <cit.>.
This idea was then put into a simpler type system (H-M) in <cit.>,
and was developed further as first-class phantom types in <cit.>
and guarded recursive type constructors in <cit.>.
<cit.> used Leibniz-style encoding of equality to reason over the equality among types
for building well-typed and well-scoped syntax trees.
GADTs are integrated into GHC Haskell in <cit.>.

Indexed types <cit.> are the generalization of inductive types with type-equality,
where values are also allowed to appear as parameters of inductive types.
Agda <cit.> and Idris <cit.> have a more ergonomic design of indexed types
where the equality relations are made implicit.

In <cit.>, the type-family encoding of the sized vector type is discussed
and is directly related to simpler indexed types. However, there are several key advantages of
simpler indexed types over the record encoding given in <cit.>:

* Simpler indexed types have names for the types and constructors.
The record encoding anonymizes the type and the constructors,
so the error messages are harder to understand.

* The pattern matching in simpler indexed type does not need to be covering.
For instance, the simpler indexed type $\Dat{Fin}~\cons{zero}$ is implicitly an empty
type, while encoding it as a function requires writing an explicit pattern matching
clause $\AgdaInductiveConstructor{zero}=\AgdaDatatype{$\bot$}$.

* Similar to coverage, pattern matching in simpler indexed types does not need
to be structurally recursive. The record encoding uses functions so we need to
respect the rules for functions, including persuading the termination checker.

Another work related to the encoding of indexed types is <cit.>,
where they propose an encoding similar to the $\Dat{Image}$ example proposed in <ref>
and discuss a potential optimization to indexed types similar to <cit.>.
The advantages of simpler indexed types over <cit.> still applies to the encoding in <cit.>.
A notable application of indexed types based on <cit.> is ornaments <cit.>.

The proposed feature has been implemented in two systems individually:

* The Arend <cit.> proof assistant, an implementation of homotopy type theory with a cubical-flavored interval type.

* The Aya <cit.> proof assistant, an experimental implementation of a type theory similar to Arend's, but with
other features such as overlapping and order-independent patterns <cit.>.

All of the operations (except $\vars\Delta$ – it is too simple to be a class) in <ref> have a corresponding
class in the package  in the source code of Aya: $\vars p$ corresponds
to , $\toTerm p$ corresponds to , $\matches u p$ corresponds to .

Apart from that, the type checking of terms in <ref> corresponds to ,
the type checking of patterns in <ref> corresponds to ,
and the type checking of declarations in <ref> corresponds to .
The source code of Aya could be retrieved from the link in the corresponding reference entry.
The complete normalizer example in <ref> is available at
as a test-case of the Aya type checker.

§.§ Acknowledgments

We are grateful to Yu Zhang and Yiming Zhu for their suggestions on the draft version of this paper
and Guillaume Allais for their review on an earlier version of this paper.
We would also like to thank the anonymous reviewers from the ICFP TyDe workshop
for their valuable suggestions on improving the paper.

Missing 'biblatex' package
The bibliography requires the 'biblatex' package.

Paris, France

Association for Computing Machinery

booktitleProceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs
seriesCPP 2017
titleType-and-Scope Safe Programs and Their Proofs
Agda,Normalisation by Evaluation,Generic Programming,Lambda-calculus,Semantics,Mechanized Meta-Theory

Savannah, GA, USA

booktitleProceedings of the 4th International Workshop on Types in Language Design and Implementation
seriesTLDI '09
titleDependently Typed Programming in Agda
dependent types,programming
family=Aya developers,

howpublished< https://github.com/aya-prover/aya-dev >
titleThe Aya Proof Assistant

Gothenburg, Sweden

Association for Computing Machinery

booktitleProceedings of the 19th ACM SIGPLAN International Conference on Functional Programming
seriesICFP '14
titlePattern Matching without K
k axiom,homotopy type theory,dependent pattern matching,agda

Nara, Japan

Association for Computing Machinery

booktitleProceedings of the 21st ACM SIGPLAN International Conference on Functional Programming
seriesICFP 2016
titleUnifiers as Equivalences: Proof-Relevant Unification of Dependently Typed Data
Agda,Dependent Types,Inductive Families,Unification,Type Theory

New York, NY, USA

Association for Computing Machinery

journaltitleProc. ACM Program. Lang.
titleElaborating Dependent (Co)Pattern Matching
Dependent pattern matching,Dependent types,Agda,Copatterns

titleHistory of the notation for substitution

Berlin, Heidelberg

Springer Berlin Heidelberg

booktitleAlgebra, Meaning, and Computation: Essays dedicated to Joseph A. Goguen on the Occasion of His 65th Birthday
titleEliminating Dependent Pattern Matching

journaltitleJournal of Symbolic Logic
titleA General Formulation of Simultaneous Inductive-Recursive Definitions in Type Theory

booktitleInternational Workshop on Computer Science Logic
titleInductive-inductive definitions

Berlin, Heidelberg

Springer Berlin Heidelberg

booktitleTypes for Proofs and Programs
titleInductive Families Need Not Store Their Indices

journaltitleTYPES 2018
titleVectors are records, too

Berlin, Heidelberg

Springer Berlin Heidelberg

booktitleProgramming Languages and Systems
titleOverlapping and Order-Independent Patterns

notePreprint available at <https://staff.math.su.se/anders.mortberg/papers/cubicalagda2.pdf>
titleCubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types

New York, NY, USA

Association for Computing Machinery

journaltitleProc. ACM Program. Lang.
titleHigher Inductive Types in Cubical Computational Type Theory
homotopy type theory,cubical type theory,higher inductive types
family=Univalent Foundations Program,

Institute for Advanced Study

< https://homotopytypetheory.org/book >

titleHomotopy Type Theory: Univalent Foundations of Mathematics

titleCubical Type Theory: A Constructive Interpretation of the Univalence Axiom

New York, NY, USA

Association for Computing Machinery

journaltitleProc. ACM Program. Lang.
titleCubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types
Dependent Pattern Matching,Higher Inductive Types,Univalence,Cubical Type Theory

booktitleLogic Colloquium '73, Proceedings of the Logic Colloquium
seriesStudies in Logic and the Foundations of Mathematics
titleAn intuitionistic theory of types: predicative part

booktitleProceedings of the Workshop on Types for Proofs and Programs
titlePattern matching with dependent types

titleSilly Type Families DRAFT

New Orleans, Louisiana, USA

Association for Computing Machinery

booktitleProceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
seriesPOPL '03
titleGuarded Recursive Datatype Constructors
guarded recursive datatype constructors

Cornell University

titleFirst-class phantom types

journaltitleElectronic Notes in Theoretical Computer Science
noteProceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages (LFM 2004)
titleMeta-programming With Built-in Type Equality
Meta-programming,Meta-language,Equality types

ACM SIGPLAN

booktitleInternational Conference on Functional Programming (ICFP'06)
note2016 ACM SIGPLAN Most Influential ICFP Paper Award
titleSimple unification-based type inference for GADTs

Elsevier Science Publishers Ltd.

journaltitleTheor. Comput. Sci.
titleIndexed Types
functional languages,constraints,type system,dependent types,type inference

journaltitleJournal of Functional Programming
titleIdris, a general-purpose dependently typed programming language: Design and implementation

Baltimore, Maryland, USA

Association for Computing Machinery

booktitleProceedings of the 15th ACM SIGPLAN International Conference on Functional Programming
seriesICFP '10
titleThe Gentle Art of Levitation
metaprogramming,type systems,proof assistants,data structure,monads

Cambridge University Press

journaltitleJournal of Functional Programming
titleTransporting functions across ornaments

Cambridge University Press

journaltitleJournal of Functional Programming
titleProgramming with ornaments
family=Group for Dependent Types and HoTT,

JetBrains Research

howpublished< https://arend-lang.github.io >
titleThe Arend Proof Assistant


# Minimal length discretization and properties of modified metric tensor and
geodesics

Abdel Nasser Tawfik∗ Egyptian Center for Theoretical Physics (ECTP), Cairo,
Egypt
World Laboratory for Cosmology And Particle Physics (WLCAPP), Cairo, Egypt
∗E-mail<EMAIL_ADDRESS>Fady T. Farouk  F. Salah Tarabia  Muhammad Maher
Helwan University, Faculty of Science, Physics Department, 11792 Ain Helwan,
Cairo, Egypt

###### Abstract

We argue that the minimal length discretization generalizing the Heisenberg
uncertainty principle, in which the gravitational impacts on the
non–commutation relations are thoughtfully taken into account, radically
modifies the spacetime geometry. The resulting metric tensor and geodesic
equation combine the general relativity terms with additional terms depending
on higher–order derivatives. Suggesting solutions for the modified geodesics,
for instance, isn’t a trivial task. We discuss on the properties of the
resulting metric tensor, line element, and geodesic equation.

###### keywords:

Quantum gravity, Noncommutative geometry, Relativity and gravitation, Line
element, Metric tensor, Geodesic equation, Generalized uncertainty principle

##  1 Introduction

Suggesting a consistent theory for quantum gravity is an ultimate goal of
recent research aiming at unifying quantum mechanics (QM) with the theory of
general relativity (GR). The quantum nature of gravity is still an open
question in physics. It turns to form an enigma occupying the minds of many
physicists for many decades, for instance, so–far there is no scientific
explanation for the origin of the gravitational fields and how particles
behave inside them! This makes the gravity foundamentally different from the
other fources of nature. There were various attempts to reconcile some
principles of GR in a quantum framework [1, 2]. The quantum gravity - on one
hand - is conjectured to add new elements to GR and QM. On the other hand, the
Einstein field equations combine classical geometry with quantum
stress–energy–momentum tensor! For QM, we recall the possible modification in
the Heisenberg uncertainty principle due to gravitational effects111They
weren’t taken into considration in the original Heisenberg uncertainty
principle., known as generalized uncertainty princile (GUP) [3, 4]. The
present work introduces some insights on the possible impacts of GUP on the
metric tensor and the geodesic equation and their properties.

Couple decades ago, the line element modification and the gravity quantization
have been suggested in litrature [5, 6, 7]. A review of these models could be
found in refs. [8, 9, 10]. An extended class of the metric tensors which are
functions of a field of an internal vectors $y^{\alpha}(x)$,
$g_{\mu\nu}(x^{\alpha}\cdot y^{\alpha}(x))$, was also discussed in litrature
[11]. Accordingly, the origin of the gravitational field of spin-1 massless
particle could be determined [11]. Regarding the equivalence principle of
gravitationan and enirtial mass in extended gravity and non–geodesic motion, a
machian request was scratched [12], where a direct coupling between the Ricci
curvature scalar and the matter Lagrangian could be fixed in cosmological
observations [13].

The present script aims at tackling the long–standing essential puzzle that
the Einstein field equations relate non–quantized semi–Riemannian geometry
expressed in Ricci and Einstein tensors, which are basically depending on the
metric tensor $g_{\mu\nu}(x^{\alpha})$, with the full–quantized stress–energy-
momentum tensor $T_{\mu\nu}$ [14]. The approach applied here is the finite
minimal length uncertainty obtained from GUP. GUP was inspired by black hole
physics, doubly special relativity, and string theory [3, 4]. It is worthy
highligting that GUP is comparable with the Planck length, where quantum
fluctuations in quasi–quantized manifold likely emerge [15, 16, 17].

The modifications in the metric tensor and geodesic equation due to GUP shall
be introduced. Accordingly, we believe that the present study offers a
theoretical framework for the observations that the universe acceleratingly
expands. Alongside forces deriving this type of expansion, such as dark energy
[17] and cosmological constant [18], we suggest that it might be also
originated to interdependence of GR on QM, especially at the Planck scale.

The present paper is organized as follows. Section 2 reviews the generalized
uncertainly principle and minimal length uncertainty. The discretized metric
tensor and its properties shall be discussed in section 3. The discretized
geodesic equation and its properties shall be introduced in section 4. Section
5 is devoted to the final conclusions.

##  2 Generalized uncertainly principle and minimal length uncertainty

The Heisenberg uncertainty principle (HUP) is a recipe on how the
uncertainties are constrained in the quantum non–commutation relations of
length and momentum operators, for instance. This was originally suggested in
absence of any gravitational field. Analyzing HUP in gravitational fields
comes up with modifications, know as GUP. Such a phenomenological aspect can
be originated in black hole physics, doubly special relativity, and string
theory [3, 4]. Phenomenology because so–far there is no theoretical
explanation of the gravitational fields origin making gravity substantially
different from the other three forces of nature. A finite minimal length was
suggested as [19],

$\displaystyle\Delta x\,\Delta p\geq\frac{\hbar}{2}\left[1+\beta(\Delta
p)^{2}\right],$ (1)

where $\Delta x$ and $\Delta p$ are length and momentum uncertainties,
respectively. $\beta=\beta_{0}(\ell_{p}/\hbar)^{2}=\beta_{0}/(m_{p}c)^{2}$, is
the GUP parameter with $\ell_{p}=\sqrt{\hbar G/c^{3}}=1.977\times
10^{-16}~{}$GeV-1 the Planck length and $m_{p}=\sqrt{\hbar c/G}=1.22\times
10^{19}~{}$GeV$/c^{2}$ the Planck mass. An upper bound on $\beta_{0}$ is based
on astronomical observations, such as, $\beta_{0}\lesssim 5.5\times 10^{60}$
based on recent gravitational waves observations. From Eq. (1), then the
minimum length uncertainty reads

$\displaystyle\Delta x_{\mbox{min}}\approx\hbar\sqrt{3\beta_{0}}$
$\displaystyle=$ $\displaystyle\ell_{p}\sqrt{\beta_{0}}.$ (2)

The experimental estimations [20] of $\beta_{0}$ range from $\sim 10^{21}$ to
$\sim 10^{39}$. Another GUP approach motivated by quantum deformation of the
Pioncarre algebra [21, 22] suggests that the minimal length associated with is
given as

$\displaystyle\Delta x_{\mbox{min}}\simeq\frac{\hbar G}{\gamma_{0}}$
$\displaystyle=$ $\displaystyle\frac{\ell_{p}^{2}}{\gamma_{0}},$ (3)

where $\gamma_{0}$ is photon’s wavelength sent from infinity to be absorbed in
a black hole. Its experimental estimations [20] range from $\sim 10^{26}$ to
$\sim 10^{34}$.

The UV/IR correspondence can be applied on various phenomena in which short
and long distance physics play a characterized role. For example, gravity [23]
and the ”deformed” commutation relations have features of UV/IR correspondence
[24]. Therefore, we assume that the minimal length discretization could be
analyzed from the UV/IR correspondence [10]. Indeed, $\Delta x$ rapidly
increases (IR) as the $\Delta p$ increases beyond the Planck scale (UV) [25,
26, 27].

Analogous to expression (1), the canonical non–commutation relation of length
and momentum quantum operators is given as

$\displaystyle\left[\hat{x}_{i}\,,\hat{p}_{j}\right]\geq\delta_{ij}i\,\hbar\left(1+\beta
p^{2}\right),$ (4)

where $p^{2}=g_{ij}p^{0i}\,p^{0j}$ and $g_{ij}$ is Minkowski spacetime metric
tensor, for instance $(-,+,+,+)$. Both length and momentum operators,
respectively, read

$\displaystyle\hat{x}_{i}$ $\displaystyle=$ $\displaystyle\hat{x}_{0i}(1+\beta
p^{2}),$ (5) $\displaystyle\hat{p}_{j}$ $\displaystyle=$
$\displaystyle\hat{p}_{0j},$ (6)

in which $\hat{x}_{0i}$ and $\hat{p}_{0j}$ can be derived from the
corresponding non–communitation relation,

$\displaystyle[\hat{x}_{0i},\hat{p}_{0j}]$ $\displaystyle=$
$\displaystyle\delta_{ij}i\,\hbar.$ (7)

##  3 Discretized metric tensor and its properties

With the quantum non–commutation operations discussed in section 2 the
four–dimensional Minkowskian manifold of the line element can be given as

$\displaystyle ds^{2}$ $\displaystyle=$ $\displaystyle
g_{\mu\nu}dx^{\mu}dx^{\nu},$ (8)

where $\mu$, $\nu$, and $\lambda=0,1,2,3$. This could be extended to
eight–dimensional spacetime tangent bundle with coordinates
$x^{A}=(x^{\mu}(\zeta^{a}),\beta\dot{x}^{\mu}(\zeta^{a}))$, where
$\dot{x}^{\mu}=dx^{\mu}/d\zeta^{\mu}$ [28]. Obviously, the line element reads

$\displaystyle d\tilde{s}^{2}=g_{AB}\,dx^{A}\,dx^{B},$ (9)

where $x^{A}=x^{A}(\zeta^{\mu})$, $g_{AB}=g_{\mu_{\nu}}\otimes g_{\mu\nu}$,
and the indices $A$ and $B=0,1,\cdots,7$. With some assumptions and
approximations, this manifold could be reformulated as an effective
four–dimensional spacetime manifold,

$\displaystyle\tilde{g}_{\mu\nu}$ $\displaystyle=$ $\displaystyle
g_{AB}\frac{\partial x^{A}}{\partial\zeta^{\mu}}\frac{\partial
x^{B}}{\partial\zeta^{\nu}}\simeq g_{ab}\Big{[}\frac{\partial
x^{a}}{\partial\zeta^{\mu}}\frac{\partial
x^{b}}{\partial\zeta^{\nu}}+\beta\frac{\partial\dot{x}^{a}}{\partial\zeta^{\mu}}\frac{\partial\dot{x}^{b}}{\partial\zeta^{\nu}}\Big{]}\simeq\left(1+\beta\ddot{x}^{\lambda}\ddot{x}_{\lambda}\right)g_{\mu\nu}.$
(10)

$\ddot{x}^{\mu}=\partial\dot{x}^{\mu}/\partial\zeta^{\mu}$ is four–dimensional
acceleration. The indices $a$, and $b=0,1,\cdots,7$.

It is now proper to highlight a number of the discretized metric tensor
properties. First, we distinguish between flat and curved spacetime:

  * •

For flat spacetime, $g_{\mu\nu}=\eta_{\mu\nu}$ and the modified metric tensor
reads

$\displaystyle\tilde{g}_{\mu\nu}$ $\displaystyle\simeq$
$\displaystyle\eta_{\mu\nu}+\beta\ddot{x}^{\lambda}\ddot{x}_{\lambda}\eta_{\mu\nu}\simeq\eta_{\mu\nu}+h_{\mu\nu},$
(11)

where $h_{\mu\nu}=\beta\ddot{x}^{\lambda}\ddot{x}_{\lambda}\eta_{\mu\nu}$. The
quantum fluctuations from which the minimal length uncertainty likely emerges
are compassed in $h_{\mu\nu}$. In other words, both GR metric tensor and this
modified one are only distinguishable, at finite $h_{\mu\nu}$.

  * •

For curved spacetime, the modified metric tensor reads

$\displaystyle\tilde{g}_{\mu\nu}$ $\displaystyle\simeq$ $\displaystyle
g_{\mu\nu}+\beta\ddot{x}^{\lambda}\ddot{x}_{\lambda}g_{\mu\nu}.$ (12)

Again, $\beta\ddot{x}^{\lambda}\ddot{x}_{\lambda}g_{\mu\nu}$ represents the
minimal length contributions.

The $\tilde{g}_{\mu\nu}$, Eq. (12), seems to play the same role as that of
$g_{\mu\nu}$, namely it turns a covariant tensor into a contravariant tensor
and vice versa. $\tilde{g}_{\mu\nu}$ is apparently symmetric in its indices
$\mu$ and $\nu$ as its components are likely equal upon exchanging the
indices. The $\tilde{g}_{\mu\nu}$ symmetric properties are invariant upon
basis transformation only if its indices are of the same type; variant or
covariant. For spacetime represented by a four–dimensional differentiable
manifold $\mathcal{M}$, the metric tensor, $\tilde{g}_{\mu\nu}$, Eq. (12), is
covariant, second–degree, symmetric on $\mathcal{M}$. Such manifold is
Lorentzian. In local coordinates $x^{\mu}$, the metric can be expressed in
$dx^{\mu}$ (one–form gradients of the scalar coordinate fields $x^{\mu}$), and
the coefficients $\tilde{g}_{\mu\nu}$ ($16$ real–valued functions). If the
local coordinates are specified, the metric can be written as a $4\times 4$
symmetric matrix with the coefficients $\tilde{g}_{\mu\nu}$. If the matrix is
non–singular having non–vanishing determinant, $\tilde{g}_{\mu\nu}$ is
non–degenerate. The Lorentzian signature of $\tilde{g}_{\mu\nu}$ obviously
implies that the matrix has one negative and three positive eigenvalues. Under
a change of the local coordinates $x^{\mu}\to x^{\bar{\mu}}$, we obtain

$\displaystyle\tilde{g}_{\bar{\mu}\bar{\nu}}=\frac{\partial
x^{\alpha}}{\partial x^{\bar{\mu}}}\,\frac{\partial x^{\beta}}{\partial
x^{\bar{\nu}}}\;\tilde{g}_{\alpha\beta}=\Theta^{\alpha}_{\bar{\mu}}\,\Theta^{\beta}_{\bar{\nu}}\;\tilde{g}_{\alpha\beta}$
(13)

If $dx^{\mu}$ are regarded as the components of an infinitesimal coordinate
displacement four–vector, the metric determines the invariant square of an
infinitesimal line element. Also, it is apparent that the principle of the
general covariance is satisfied even in absence of gravitational effects on
the modified Minkowski metric. Then, the modified four–dimensional line
element can be expressed as

$\displaystyle d\tilde{s}^{2}$ $\displaystyle=$ $\displaystyle
g_{\mu\nu}\left(dx^{\mu}dx^{\nu}+\beta^{2}d\dot{x}^{\mu}\;d\dot{x}^{\nu}\right)=ds^{2}+\beta^{2}\ddot{x}^{\lambda}\ddot{x}_{\lambda}\,ds^{2},$
(14)

and $d\tilde{s}^{2}$ manifests the causal structure of the spacetime. Only
timelike four–dimensional line element, $d\tilde{s}^{2}<0$, can physically
covered by a massive object. If $d\tilde{s}^{2}=0$ the line element is
lightlike (covered by massless photon). On the other hand, for
$d\tilde{s}^{2}>0$, the four–dimensional line element is an incremental proper
length, i.e., spacelike.

##  4 Discretized geodesic equation and its properties

The properties of the manifold including geodesics in GR
[$\ddot{x}^{\mu}+\Gamma^{\mu}_{\alpha\beta}\dot{x}^{\mu}\dot{x}^{\nu}=0$ with
$\dot{x}^{\mu}=\partial x^{\mu}/\partial s$, Christopher symbols
$\Gamma^{\mu}_{\alpha\beta}=(g^{\mu\gamma}/2)(\partial
g_{\gamma\alpha}/\partial x^{\beta})+\partial g_{\gamma\beta}/\partial
x^{\alpha}-\partial g_{\alpha\beta}/\partial x^{\gamma})$, and $s$ is a scalar
parameter of motion such as a proper time] can be generalized. For example,
the notion of a ”straight line” is to be generalized to ”curved spacetime”.
The consequences of the length discretization or minimal length uncertainty
based on GUP, generalize the world line of a free particle. GR assumes that
gravity couldn’t be regarded as a force but it should be emerged from
”classical” curved spacetime geometry and ”quantized” stress–energy–momentum
tensor is causing the ”classical” spacetime curvature. The approach utilized
here is discretized minimal length, which modifies both metric tensor and line
element.

As discussed in ref. [10], using the variational principle and extremization
of the path $s_{AB}$, the geodesic equation could be derived as follows.

  * •

In flat spacetime (Minkowski space)

$\displaystyle\beta{\cal
L}\frac{d^{2}\dot{x}^{\mu}}{ds^{2}}-\frac{dx^{\mu}}{ds}+c$ $\displaystyle=$
$\displaystyle 0.$ (15)

Even if $\beta$, the GUP parameter vanishes, the geodesic equation reduces to
that of a straight line, at constant velocity, i.e., both $\beta$ terms
disappear.

  * •

and in curved spacetime

$\displaystyle\frac{d^{2}x^{\mu}}{ds^{2}}+\Gamma^{\eta}_{\mu\nu}\frac{dx^{\mu}}{ds}\frac{dx^{\nu}}{ds}$
$\displaystyle=$ $\displaystyle\beta\Bigg{\\{}\frac{d}{ds}\Big{[}{\cal
L}\frac{d^{2}\dot{x}^{\mu}}{ds^{2}}\Big{]}+\frac{1}{2}g^{\mu\nu}\Bigg{(}g_{\mu\nu,\alpha}\frac{d\dot{x}^{\mu}}{ds}\frac{d\dot{x}^{\nu}}{ds}-{\cal
L}g_{\mu\alpha,\gamma}\frac{d\dot{x}^{\gamma}}{ds}\frac{d\dot{x}^{\mu}}{ds}\Bigg{)}$
(16) $\displaystyle{\cal
L}g^{\mu\nu}\Bigg{(}2g_{\mu\alpha,\gamma}\frac{d}{ds}+g_{\mu\alpha,\gamma,\delta}\frac{dx^{\delta}}{ds}\Bigg{)}\frac{dx^{\gamma}}{ds}\frac{d\dot{x}^{\mu}}{ds}\Bigg{\\}}$

where the proper time can be deduced from the Lagrangian, $\tau=\int{\cal
L}(s,\dot{x},\ddot{x})\,ds$,

$\displaystyle\frac{\partial\tau}{\partial s}$ $\displaystyle=$
$\displaystyle{\cal
L}(s,\dot{x},\ddot{x})=-\left[g_{\mu\nu}\left(\frac{dx^{\mu}}{ds}\frac{dx^{\nu}}{ds}+\beta\frac{d\dot{x}^{\mu}}{ds}\frac{d\dot{x}^{\nu}}{ds}\right)\right]^{1/2},$
$\displaystyle\Gamma^{\eta}_{\mu\nu}$ $\displaystyle=$
$\displaystyle\frac{1}{2}g^{\eta\alpha}\left[g_{\mu\alpha,\nu}-g_{\alpha\nu,\mu}+g_{\mu\nu,\alpha}\right],$
$\displaystyle g_{\mu\nu,\alpha}$ $\displaystyle=$
$\displaystyle\frac{\partial g_{\mu\nu}}{\partial x^{\alpha}},$ $\displaystyle
g_{\mu\alpha,\gamma,\delta}$ $\displaystyle=$
$\displaystyle\frac{\partial}{\partial x^{\delta}}\left(\frac{\partial
g_{\mu\alpha}}{\partial x^{\gamma}}\right).$

The $\beta$–terms in Eq. (16) distinguish this expression of discretized
geodesics from the GR geodesics,

$\displaystyle\frac{d^{2}x^{\mu}}{ds^{2}}+\Gamma^{\eta}_{\mu\nu}\frac{dx^{\mu}}{ds}\,\frac{dx^{\nu}}{ds}=0,$
(17)

which could be solved when, for instance, assuring that the proper time reads
$ds^{2}=g_{\mu\nu}dx^{\mu}dx^{\nu}$. Under the condition that

$\displaystyle g_{\mu\nu}\frac{dx^{\mu}}{ds}\,\frac{dx^{\nu}}{ds}=\epsilon,$
(18)

where $\epsilon=0$ for photon and $\epsilon=1$ for massive particles, the
geodesic equation is supplemented. For conserved energy and angular momentum
the geodesic equation can be expressed as an ordinary first–order differential
equation [29].

Solving the discretized geodesic equation, Eq. (16), is not a trivial task,
because of the finite terms in rhs, which encompass higher–order derivatives.

##  5 Conclusions

The approach of minimal length uncertainty conserves both Christoffel
connection222The metric connection characterizes the affine connection to a
manifold provided with the metric. This allows lengths, for instance, to be
measured on that manifold. and the equivalence principle of the gravitational
and inertial mass. They are not affected. This allows to recover any
violations in the equivalence principle, especially as a possible reason of
quantum gravity. We highlight that this conclusion contradicts previous
studies [30, 31]. The reason could be the rigorous procedure implemented in
the present study. We have first determined the modified metric tensor.
Accordingly, we have obtained the modified line element. Both are key
principles of the proposed theory of discretized geometry. We could also
derive the corresponding geodesics, in which the appearance of higher–order
derivatives substantially distinguishes this expression from the GR geodesics.

The modification to the line element is summarized in the term
$\beta^{2}\ddot{x}^{\lambda}\ddot{x}_{\lambda}$, which highlights the
essential contributions added by the acceleration of the test particle. We
conclude that the length discretization ensures that the line element wouldn’t
only expand but apparently accelerates. The metric tensor is also modified by
the term $\beta\ddot{x}^{\lambda}\ddot{x}_{\lambda}$. The properties of the
modified metric tensor has been elaborated.

We find that the modified geodesics is not only providing the acceleration of
a test particle inside the gravitational field. Higher–order derivatives are
also present [32], namely the jerk, $\dddot{x}^{\mu}$, which in turn is
derived from the time derivative of the acceleration. In contract to GR
geodesics, solving the modified geodesics isn’t a trivial task. The
corresponding differential equations are complex and non–linear.

## Acknowledgments

AT is very grateful to organizers of sixteenth Marcel Grossmann meeting - MG16
for their kind invitation and financial support!

## References

  * [1] C. Rovelli and L. Smolin, Loop Space Representation of Quantum General Relativity, Nucl. Phys. B 331, 80 (1990).
  * [2] J. F. Donoghue, General relativity as an effective field theory: The leading quantum corrections, Phys. Rev. D 50, 3874 (1994).
  * [3] A. N. Tawfik and A. M. Diab, Generalized Uncertainty Principle: Approaches and Applications, Int. J. Mod. Phys. D 23, p. 1430025 (2014).
  * [4] A. N. Tawfik and A. M. Diab, Review on Generalized Uncertainty Principle, Rept. Prog. Phys. 78, p. 126001 (2015).
  * [5] A. Feoli, G. Lambiase, G. Papini and G. Scarpetta, Schwarzschild field with maximal acceleration corrections, Phys. Lett. A 263, 147 (1999).
  * [6] S. Capozziello, A. Feoli, G. Lambiase, G. Papini and G. Scarpetta, Massive scalar particles in a modified Schwarzschild geometry, Phys. Lett. A 268, 247 (2000).
  * [7] V. Bozza, A. Feoli, G. Lambiase, G. Papini and G. Scarpetta, Maximal acceleration effects in Kerr space, Phys. Lett. A 283, 53 (2001).
  * [8] P. O. Hess, M. Schafer and W. Greiner, Pseudo-complex General Relativity (Springer, Heidelberg, 2015).
  * [9] P. Hess, Alternatives to Einstein’s General Relativity Theory, Prog. Part. Nucl. Phys. 114, p. 103809 (2020).
  * [10] A. N. Tawfik, A. M. Diab, S. Shenawy and E. A. El Dahab, Consequences of minimal length discretization on line element, metric tensor and geodesic equation, Astron. Nachr. 342, 54 (2021).
  * [11] C. G. Oliveira, On the properties of an extended class of metric tensors in relativity, Int. J. Theor. Phys. 24, p. 1081 (1985).
  * [12] I. Licata, C. Corda and E. Benedetto, A machian request for the equivalence principle in extended gravity and nongeodesic motion, Grav. Cosmol. 22, 48 (2016).
  * [13] I. Licata, C. Corda and E. Benedetto, A machian request for the equivalence principle in extended gravity and nongeodesic motion, Grav. Cosmol. 22, 48 (2016).
  * [14] H. Stephani, D. Krämer, M. MacCallum, C. Hoenselaers and E. Herlt, Exact solutions of Einstein’s field equations; 2nd ed. (Cambridge Univ. Press, Cambridge, 2003).
  * [15] F. Karolyhazy, Gravitation and quantum mechanics of macroscopic objects, Nuovo Cimento (Italy) Divided into Nuovo Cimento A and Nuovo Cimento B (10), 42A (1966).
  * [16] A. Tawfik and A. Diab, Emergence of cosmic space and minimal length in quantum gravity: a large class of spacetimes, equations of state, and minimal length approaches, Indian J. Phys. 90, 1095 (2016).
  * [17] A. N. Tawfik and E. A. El Dahab, Review on Dark Energy Models, Grav. Cosmol. 25, 103 (2019).
  * [18] P. Peebles and B. Ratra, The Cosmological Constant and Dark Energy, Rev. Mod. Phys. 75, 559 (2003).
  * [19] A. Kempf, G. Mangano and R. B. Mann, Hilbert space representation of the minimal length uncertainty relation, Phys. Rev. D 52, 1108 (1995).
  * [20] D. Gao and M. Zhan, Constraining the generalized uncertainty principle with cold atoms, Phys. Rev. A 94, p. 013607 (2016).
  * [21] M. Maggiore, A Generalized uncertainty principle in quantum gravity, Phys. Lett. B 304, 65 (1993).
  * [22] M. Maggiore, Quantum groups, gravity and the generalized uncertainty principle, Phys. Rev. D 49, 5182 (1994).
  * [23] M. G. Jackson, Gravity from a modified commutator, Int. J. Mod. Phys. D 14, 2239 (2005).
  * [24] M. Jackson, Gravity from a modified commutator, International Journal of Modern Physics D 14, 2239 (2005).
  * [25] J. M. Maldacena, The Large N limit of superconformal field theories and supergravity, Int. J. Theor. Phys. 38, 1113 (1999).
  * [26] S. Gubser, I. R. Klebanov and A. M. Polyakov, Gauge theory correlators from noncritical string theory, Phys. Lett. B 428, 105 (1998).
  * [27] E. Witten, Anti-de Sitter space and holography, Adv. Theor. Math. Phys. 2, 253 (1998).
  * [28] H. E. Brandt, Causal Domain of Minkowski-spacetime Tangent Bundle, Found. Phys. Lett. 13, 581 (2000).
  * [29] E. Hackmann and C. Lammerzahl, Complete Analytic Solution of the Geodesic Equation in Schwarzschild- (Anti-) de Sitter Spacetimes, Phys. Rev. Lett. 100, p. 171101 (2008).
  * [30] S. Ghosh, Quantum Gravity Effects in Geodesic Motion and Predictions of Equivalence Principle Violation, Class. Quant. Grav. 31, p. 025025 (2014).
  * [31] F. Scardigli and R. Casadio, Is the equivalence principle violated by generalized uncertainty principles and holography in a brane-world?, Int. J. Mod. Phys. D 18, 319 (2009).
  * [32] D. Eager, A.-M. Pendrill and N. Reistad, Beyond velocity and acceleration: jerk, snap and higher derivatives, European Journal of Physics 37, p. 065008 (oct 2016).