Kostia Chardonnet

Alexis Saurin

Benoît Valiron

Équipe Πr

A Curry-Howard Correspondence for Linear, Reversible Computation

Keywords: 2012 ACM Subject Classification Theory of computation → Linear logic; Theory of computation → Equational logic and rewriting Reversible Computation, Linear Logic, Curry-Howard Digital Object Identifier 10.4230/LIPIcs.CSL.2023.36

In this paper, we present a linear and reversible programming language with inductives types and recursion. The semantics of the languages is based on pattern-matching; we show how ensuring syntactical exhaustivity and non-overlapping of clauses is enough to ensure reversibility. The language allows to represent any Primitive Recursive Function. We then give a Curry-Howard correspondence with the logic µMALL: linear logic extended with least xed points allowing inductive statements. The critical part of our work is to show how primitive recursion yields circular proofs that satisfy µMALL validity criterion and how the language simulates the cut-elimination procedure of µMALL.

Introduction

Computation and logic are two faces of the same coin. For instance, consider a proof s s . . . . A → B t . . . .

A B

Figure 1 Modus Ponens of A → B and a proof t of A. With the logical rule Modus Ponens one can construct a proof of B: Figure 1 features a graphical presentation of the corresponding proof. Horizontal lines stand for deduction steps -they separate conclusions (below) and hypotheses (above). These deduction steps can be stacked vertically up to axioms in order to describe complete proofs. In Figure 1 the proofs of A and A → B are symbolized with vertical ellipses. The ellipsis annotated with s indicates that s is a complete proof of A → B while t stands for a complete proof of A.

This connection is known as the Curry-Howard correspondence [START_REF] Haskell | Functionality in combinatory logic[END_REF][START_REF] William | The formulae-as-types notion of construction. To HB Curry: essays on combinatory logic, lambda calculus and formalism[END_REF]. In this general framework, types correspond to formulas and programs to proofs, while program evaluation is mirrored with proof simpli cation (the so-called cut-elimination). The Curry-Howard correspondence formalizes the fact that the proof s of A → B can be regarded as a function -parametrized by an argument of type A-that produces a proof of B whenever it is fed with a proof of A. Therefore, the computational interpretation of Modus Ponens corresponds to the application of an argument (i.e. t) of type A to a function (i.e. s) of type A → B. When computing the corresponding program, one substitutes the parameter of the function with t and get a result of type B. On the logical side, this corresponds to substituting every axiom introducing A in the proof s with the full proof t of A. This yields a direct proof of B without any invocation of the "lemma" A → B.

Paving the way toward the veri cation of critical softwares, the Curry-Howard correspondence provides a versatile framework. It has been used to mirror rst and second-order logics with dependent-type systems [START_REF] Bertot | Interactive theorem proving and program development: Coq'Art: the calculus of inductive constructions[END_REF][START_REF] Leroy | Formal veri cation of a realistic compiler[END_REF], separation logics with memory-aware type systems [START_REF] John | Separation logic: A logic for shared mutable data structures[END_REF][START_REF] Jung | Rustbelt: Securing the foundations of the rust programming language[END_REF], resource-sensitive logics with di erential privacy [START_REF] Gaboardi | Linear dependent types for di erential privacy[END_REF], logics with monads with reasoning on sidee ects [START_REF] Swamy | Dependent types and multi-monadic e ects in f[END_REF][START_REF] Maillard | The next 700 relational program logics[END_REF], etc.

Reversible computation is a paradigm of computation which emerged as an energy-preserving model of computation in which data is never erased [START_REF] Fredkin | Conservative logic[END_REF] that makes sure that, given some process f , there always exists an inverse process f -1 such that f • f -1 = Id = f -1 • f . Many aspects of reversible computation have been considered, such as the development of reversible Turing Machines [START_REF] Morita | A universal reversible turing machine[END_REF], reversible programming languages [START_REF] Rosham | Theseus: A high-level language for reversible computing[END_REF] and their semantics [START_REF] Chardonnet | Categorical semantics of reversible patternmatching[END_REF][START_REF] Kaarsgaard | Join inverse rig categories for reversible functional programming, and beyond[END_REF]. However, the formal relationship between a logical system and a computational model have not been developed yet.

This paper aims at proposing a type system featuring inductive types for a purely linear and reversible language. We base our study on the approach presented in [START_REF] Sabry | From symmetric pattern-matching to quantum control[END_REF]. In this model, reversible computation is restricted to two main types: the tensor, written A ⊗ B and the co-product, written A ⊕ B. The former corresponds to the type of all pairs of elements of type A and elements of type B, while the latter represents the disjoint union of all elements of type A and elements of type B. For instance, a bit can be typed with 1 ⊕ 1, where 1 is a type with only one element. The language in [START_REF] Sabry | From symmetric pattern-matching to quantum control[END_REF] o ers the possibility to code isos -reversible maps-with pattern matching. An iso is for instance the swap operation, typed with A ⊗ B ↔ B ⊗ A. However, if [START_REF] Sabry | From symmetric pattern-matching to quantum control[END_REF] hints at an extension towards pure quantum computation, the type system is not formally connected to any logical system.

The problem of reversibility between nite type of same cardinality simply requires to check that the function is injective. That is no longer the case when we work with types of in nite cardinality such as natural numbers.

The main contribution of this work is a Curry-Howard correspondence for a purely reversible typed language in the style of [START_REF] Sabry | From symmetric pattern-matching to quantum control[END_REF], with added generalised inductive types and terminating recursion, enforced by the fact that recursive functions must be structurally recursive: each recursive call must be applied to a decreasing argument. We show how ensuring exhaustivity and non-overlapping of the clauses of the pattern-matching are enough to ensure reversibility and that the obtained language can encode any Primitive Recursive function [START_REF] Rogers | Theory of recursive functions and e ective computability[END_REF]. For the Curry-Howard part, we capitalize on the logic µMALL [START_REF] Baelde | Least and greatest xed points in linear logic[END_REF][START_REF] Baelde | In nitary Proof Theory: the Multiplicative Additive Case[END_REF]: an extension of the additive and multiplicative fragment of linear logic with least and greatest xed points allowing inductive and coinductive statements. This logic contains both a tensor and a co-product, and its strict linearity makes it a good t for a reversible type system. In the literature, multiple proofs systems have been considered for µMALL, some nitary proof system with explicit induction inferences à la Park [START_REF] Baelde | Least and greatest xed points in linear logic[END_REF] as well as non-well-founded proof systems which allow to build in nite derivation [START_REF] Baelde | In nitary Proof Theory: the Multiplicative Additive Case[END_REF][START_REF] Baelde | Bouncing Threads for Circular and Non-Wellfounded Proofs: Towards Compositionality with Circular Proofs[END_REF]. The present paper focuses on the latter. In general, an in nite derivation is called a pre-proof and is not necessarily consistent. To solve this problem µMALL comes equipped with a validity criterion, telling us when an in nite derivation can be considered as a logical proof. We show how the syntactical constraints of being structurally recursive imply the validity of pre-proofs.

Organisation of the paper

The paper is organised as follows: in Section 2 we present the language, its syntax, typing rules and semantics and show that any function that can be encoded in our language represents an isomorphism. In Section 3 we show that our language can encode any Primitive Recursive Function [START_REF] Rogers | Theory of recursive functions and e ective computability[END_REF], this is shown by encoding the set of Recursive Primitive Permutations [START_REF] Paolini | A class of recursive permutations which is primitive recursive complete[END_REF] functions. Then in Section 4, we develop on the Curry-Howard Correspondence part: we show, given a well-typed term from our language, how to translate it into a circular derivation of the logic µMALL and show that the given derivation respects the validity condition and how our evaluation strategy simulates the cut-elimination procedure of the logic.

First-order Isos

Our language is based on the one introduced by Sabry et al [START_REF] Sabry | From symmetric pattern-matching to quantum control[END_REF] which de ne isomorphisms between various types, included the type of lists. We build on the reversible part of the paper by extending the language to support both a more general rewriting system and more general inductive types: while they only allow the inductive type of lists, we consider arbitrary inductive types. The language is de ned by layers. Terms and types are presented in Table 1, while typing derivations, inspired from µMALL, can be found in Tables 2 and3. The language consists of the following pieces.

Basic type. They allow us to construct rst-order terms. The constructors inj l and inj r represent the choice between either the left or right-hand side of a type of the form A ⊕ B; the constructor , builds pairs of elements (with the corresponding type constructor ⊗); fold represents inductive structure of the types µX.A. A value can serve both as a result and as a pattern in the de ning clause of an iso. We write (x 1 , . . . , x n ) for x 1 , . . . , x n or -→ x when n is non-ambiguous and

A 1 ⊗ • • • ⊗ A n for A 1 ⊗ (• • • ⊗ A n ) and A n for A ⊗ • • • ⊗ A n times .
First-order isos. An iso of type A ↔ B acts on terms of base types. An iso is a function of type A ↔ B, de ned as a set of clauses of the form {v 1 ↔ e 1 | . . . | v n ↔ e n }. In the clauses, the tokens v i are open values and e i are expressions. In order to apply an iso to a term, the iso must be of type A ↔ B and the term of type A. In the typing rules of isos, the OD A ({v 1 , . . . , v n }) predicate (corrected from [START_REF] Sabry | From symmetric pattern-matching to quantum control[END_REF], as their de nition makes it impossible to type To oli) syntactically enforces the exhaustivity and non-overlapping conditions on a set of well-typed values v 1 , . . . , v n of type A. The typing conditions make sure that both the left-hand-side and right-hand-side of clauses satisfy this condition. Its formal de nition can be found in Table 4 where V al(e) is de ned as V al(let p = ω p in e) = V al(e), and V al(v) = v otherwise. These checks are crucial to make sure that our isos are indeed reversible. In the last rule on Table 4, we de ne π 1 (S) and π 2 (S) as respectively {v | v, w ∈ S} and {w | v, w ∈ S} and S 1 v and S 2 v respectively as {w | v, w ∈ S} and {w | w, v ∈ S} Exhaustivity for an iso {v 1 ↔ e 1 | . . . | v n ↔ e n } of type A ↔ B means that the expressions on the left (resp. on the right) of the clauses describe all possible values for the type A (resp. the type B). Non-overlapping means that two expressions cannot match the same value. For instance, the left and right injections inj l v and inj r v are non-overlapping while a variable x is always exhaustive. The construction fix g.ω represents the creation of a recursive function, rewritten as ω[g := fix g.ω] by the operational semantics. Each recursive function needs to satisfy a structural recursion criteria: making sure that one of the input arguments strictly decreases on each recursive call. Indeed, since isos can be non-terminating (due to recursion), we need a criterion that implies termination to ensure that we work with total functions. If ω is of type A ↔ B, we can build its inverse ω ⊥ : B ↔ A and show that their composition is the identity. In order to avoid con icts between variables we will always work up to α-conversion and use Barendregt's convention [4, p.26] which consists in keeping all bound and free variables names distinct, even when this remains implicit.

= 1 | A ⊕ B | A ⊗ B | µX.A (Isos, rst-order) α ::= A ↔ B (Values) v ::= () | x | inj l v | inj r v | v 1 , v 2 | fold v (Pattern) p ::= x | p 1 , p 2 (Expressions) e ::= v | let p 1 = ω p 2 in e (Isos) ω ::= {v 1 ↔ e 1 | . . . | v n ↔ e n } | fix f.ω | f (Terms) t ::= () | x | inj l t | inj r t | t 1 , t 2 | fold t | ω t | let p = t 1 in t 2
Ψ ω f : A ↔ B ∆; Ψ e t : A ∆; Ψ e f t : B ω ω : A ↔ B ∆; Ψ e t : A ∆; Ψ e ω t : B ∆ 1 ; Ψ e t 1 : A 1 ⊗ • • • ⊗ A n ∆ 2 , x 1 : A 1 , . . . , x n : A n ; Ψ e t 2 : B ∆ 1 , ∆ 2 ; Ψ e let (x 1 , . . . , x n ) = t 1 in t 2 : B Table 2
Typing of terms and expressions

The type system is split in two parts: one for terms (noted ∆; Ψ e t : A) and one for isos (noted Ψ ω ω : A ↔ B). In the typing rules, the contexts ∆ are sets of pairs that consist of a term-variable and a base type, where each variable can only occur once and Ψ is a singleton set of a pair of an iso-variable and an iso-type association.

Definition 1 (Structurally Recursive). Given an iso fix f.{v

1 ↔ e 1 | . . . | v n ↔ e n } : A 1 ⊗ • • • ⊗ A m ↔ C, it is structurally recursive if there is 1 ≤ j ≤ m such that A j = µX.B and for all i ∈ {1, . . . , n} we have that v i is of the form (v 1 i , . . . , v m i ) such that v j i is either:
A closed value, in which case e i does not contain the subterm f p Open, in which case for all subterm of the form f p in e i we have p = (x 1 , . . . , x m ) and x j : µX.B is a strict subterm of v j i .

Given a clause v ↔ e, we call the value v j i (resp. the variable x j ) the decreasing argument (resp. the focus) of the structurally recursive criterion.

Remark 2. As we are focused on a very basic notion of structurally recursive function, the typing rules of isos allow to have at most one iso-variable in the context, meaning that we cannot have intertwined recursive call.

Finally, our language is equipped with a rewriting system → on terms, de ned in De nition 4, that follows a deterministic call-by-value strategy: each argument of a function is fully evaluated

∆ 1 e v 1 : A . . . ∆ n e v n : A OD A ({v 1 , . . . , v n }) ∆ 1 ; Ψ e e 1 : B . . . ∆ n ; Ψ e e n : B OD B ({V al(e 1 ), . . . , V al(e n )}) Ψ ω {v 1 ↔ e 1 | . . . | v n ↔ e n } : A ↔ B. f : α ω f : α f : α ω ω : α fix f.ω is structurally recursive Ψ ω fix f.ω : α Table 3 Typing of isos OD A ({x}) OD 1 ({()}) OD A (S) OD B (T ) OD A⊕B ({inj l v | v ∈ S} ∪ {inj r v | v ∈ T }) OD A[X←µX.A] (S) OD µX.A ({fold v | v ∈ S}) OD A (π 1 (S)), ∀v ∈ π 1 (S), OD B (S 1 v ) or OD B (π 2 (S)), ∀v ∈ π 2 (S), OD A (S 2 v ) OD A⊗B (S = { v 1 , v 1 , . . . , v n , v n })
Table 4 Exhaustivity and Non-Overlapping before applying the substitution. This is done through the use of an evaluation context C[], which consists of a term with a hole (where C[t] is C where the hole has been lled with t). Due to the deterministic nature of the strategy we directly obtain the unicity of the normal form. The evaluation of an iso applied to a value relies on pattern-matching : the argument is matched against the left-handside of each clause until one of them matches (written σ[v] = v ), in which case the pattern-matching, as de ned in Table 5, returns a substitution σ that sends variables to values. Because we ensure exhaustivity and non-overlapping (Lemma 5), the pattern-matching can always occur on well-typed terms. The support of a substitution σ is de ned as supp(σ) = {x | (x → v) ∈ σ}. Definition 3 (Substitution). Applying substitution σ on an expression t, written σ(t), is de ned as :

σ(()) = (), σ(x) = v if {x → v} ⊆ σ, σ(inj r t) = inj r σ(t), σ(inj l t) = inj l σ(t), σ( t, t ) = σ(t), σ(t ) , σ(ω t) = ω σ(t) and σ(let p = t 1 in t 2 ) = (let p = σ(t 1 ) in σ(t 2 )).
Definition 4 (Evaluation relation →). We de ne → the rewriting system of our language as follows:

t 1 → t 2 C[t 1 ] → C[t 2 ] Cong σ[p] = v let p = v in t → σ(t) LetE (fix f.ω) → ω[f := (fix f.ω)] IsoRec σ[v i ] = v {v 1 ↔ e 1 | . . . | v n ↔ e n } v → σ(e i )
IsoApp

with C ::= [ ] | inj l C | inj r C | ω C | let p = C in t | C, v | v, C
As usual we note → * for the re exive transitive closure of →.

Lemma 5 (OD A (A) ensures exhaustivity and non-overlapping.). Let OD A (S) and e v : A, then there exists a unique v ∈ S such that v matches v under substitution σ, i.e. σ[v ] = v.

As mentioned above, from any iso ω : A ↔ B we can build its inverse ω ⊥ : B ↔ A, the inverse operation is de ned inductively on ω and is given in De nition 6. Definition 6 (Inversion). Given an iso ω, we de ne its dual ω ⊥ as :

f ⊥ = f, (fix f.ω) ⊥ = fix f.ω ⊥ , {(v i ↔ e i ) i∈I } ⊥ = {((v i ↔ e i ) ⊥
) i∈I } And the inverse of a clause as :

  v 1 ↔ let p 1 = ω 1 p 1 in • • • let p n = ω n p n in v 1   ⊥ :=   v 1 ↔ let p n = ω ⊥ n p n in • • • let p 1 = ω ⊥ 1 p 1 in v 1   .
We can show that the inverse is well-typed and behaves as expected:

Lemma 7 (Inversion is well-typed). Given Ψ ω ω : A ↔ B, then Ψ ω ω ⊥ : B ↔ A.
Theorem 8 (Isos are isomorphisms). For all well-typed isos ω ω : A ↔ B, and for all well-typed values

e v : A, if (ω (ω ⊥ v)) → * v then v = v .
Example 9. We can de ne the iso of type :

A ⊕ (B ⊕ C) ↔ C ⊕ (A ⊕ B) as    inj l (a) ↔ inj r (inj l (a)) inj r (inj l (b)) ↔ inj r (inj r (b)) inj r (inj r (c)) ↔ inj l (c)    Example 10.
We give the encoding of the isomorphism map(ω) and its inverse: for any given iso ω : A ↔ B in our language, we can de ne map(ω)

: [A] ↔ [B] where [A] = µX.1 ⊕ (A ⊗ X)
is the type of lists of type A and [ ] is the empty list (fold (inj l ())) and h :: t is the list construction (fold (inj r h, t )). We also give its dual map(ω) ⊥ below, as given by De nition 6.

map(ω) : [

A] ↔ [B] = fix f.        [ ] ↔ [ ] h :: t ↔ let h = ω h in let t = f t in h :: t        map(ω) ⊥ : [B] ↔ [A] = fix f.        [ ] ↔ [ ] h :: t ↔ let t = f t in let h = ω ⊥ h in h :: t       
Remark 11. In our two examples, the left and right-hand side of the ↔ on each function respect both the criteria of exhaustivity -every-value of each type is being covered by at least one expression-and non-overlapping -no two expressions cover the same value. Both isos are therefore bijections.

The language enjoys the standard properties of typed languages of progress and subject reduction:

Lemma 12 (Subject Reduction). If ∆; Ψ e t : A and t → t then ∆; Ψ e t : A.

Lemma 13 (Progress). If e t : A then, either t is a value, or t → t .

x S x + 1

x P x -1 x Sign -x x Id x x X y y x    x 1 y 1 . . . f ; g . . . x n y n    =    x 1 . . . f x n       y 1 g . . . y n               x 1 y 1 . . . . . . x k f || g y k x 1 y 1 . . . . . . x l y l            =    x 1 y 1 . . . f . . . x k y n       x 1 y 1 . . . g . . . x l y l         x 1 y 1 . . . If[f, g, h]
. . .

x n y n x x           =    f (x 1 , . . . , x n ) if x > 0 g (x 1 , . . . , x n ) if x = 0 h (x 1 , . . . , x n ) if x < 0      x 1 y 1 . . . It[f ] . . . x n y n x x           = (f ; . . . ; f ) | x | (x 1 , . . . , x n ) Figure 2 Generators of RPP

Computational Content

In this section, we study the computational content of our language. In the case of only nite types made up of the tensor, plus and unit, one can represent any bijection by case analysis. Homewer, with in nite types, the expressivity becomes less clear. We show that we can encode Recursive Primitive Permutations [START_REF] Paolini | A class of recursive permutations which is primitive recursive complete[END_REF] (RPP), which shows us that we can encode at least all Primitive Recursive Functions [START_REF] Rogers | Theory of recursive functions and e ective computability[END_REF].

We give a few reminders on the language RPP and its main results, then show how to encode it.

Reminder on RPP

RPP is a set of integer-valued functions of variable arity; we de ne it by arity as follows: we note RPP k for the set of functions in RPP from Z k to Z k , it is built inductively on k ∈ N by: the successor (S), the predecessor (P ), the identity (ID) and the sign-change that are part of RPP 1 . The swap function (X ) and the binary permutation X which sends the pair (x, y) to (y, x) are part of RPP 2 and then, for any function f, g, h ∈ RPP k and j ∈ RPP l , we can build (i) the sequential composition f ;

g ∈ RPP k , (ii) the parallel composition f || j ∈ RPP k+l (iii) the iterator It[f ] ∈ RPP k+1 and (iv) the selection If[f, g, h] ∈ RPP k+1 .
Finally, the set of all functions that form RPP is taken as the union for all k of the RPP k :

RPP = ∪ k∈N RPP k
We present the semantics of each constructors of RPP under a graphical form, as in [START_REF] Paolini | A class of recursive permutations which is primitive recursive complete[END_REF], where the left-hand-side variables of the diagram represent the input of the function and the right-hand-side is the output of the function. The semantics of all those operators are given in Figure 2.

Remark 14. In their paper [START_REF] Paolini | A class of recursive permutations which is primitive recursive complete[END_REF], the authors make use of two other constructors: generalised permutations over Z k and weakenings of functions, but those can actually be de ned from the other constructors so that in the following section we do not give their encoding. Then, if f ∈ RPP k we can de ne an inverse f -1 :

Definition 15 (Inversion). The inversion is de ned as follow :

Id -1 = Id S -1 = P P -1 = S Sign -1 = Sign X -1 = X (g; f ) -1 = f -1 ; g -1 (f || g) -1 = f -1 || g -1 (It[f ]) -1 = It[f -1 ] (If [f, g, h]) -1 = If [f -1 , g -1 , h -1 ]
Proposition 16 (Inversion defines an inverse [START_REF] Paolini | A class of recursive permutations which is primitive recursive complete[END_REF]). [START_REF] Paolini | A class of recursive permutations which is primitive recursive complete[END_REF]). RPP is PRF-Complete and PRF-Sound: it can represent any Primitive Recursive Function and every function in RPP can be represented in PRF.

Given f ∈ RPP k then f ; f -1 = Id = f -1 ; f Theorem 17 (Soudness & Completeness

From RPP to Isos

We start by de ning the type of stricly positive natural numbers, npos, as npos = µX.1 ⊕ X. We de ne n, the encoding of a positive natural number into a value of type npos as 1 = fold inj l () and n + 1 = fold inj r n. Finally, we de ne the type of integers as Z = 1 ⊕ (npos ⊕ npos) along with z the encoding of any z ∈ Z into a value of type Z de ned as: 0 = inj l (), z = inj r inj l z for z positive, and z = inj r inj r -z for z negative. Given some function f ∈ RPP k , we will build an iso isos(f ) : Z k ↔ Z k which simulates f . isos(f ) is de ned by the size of the proof that f is in RPP k .

Definition 18 (Encoding of the primitives).

The Sign-change of type

Z ↔ Z is    inj r (inj l x) ↔ inj r (inj r x) inj r (inj r (x)) ↔ inj r (inj l x) inj l () ↔ inj l ()    The identity is {x ↔ x} : Z ↔ Z The Swap is {(x, y) ↔ (y, x)} : Z 2 ↔ Z 2
The Predecessor is the inverse of the Successor

The Successor is

       inj l () ↔ inj r (inj l (fold (inj l ()))) inj r (inj l x) ↔ inj r (inj l (fold (inj r x))) inj r (inj r (fold (inj l ()))) ↔ inj l () inj r (inj r (fold (inj r x))) ↔ inj r (inj r x)        : Z ↔ Z
Definition 19 (Encoding of Composition). Let f, g ∈ RPP j , ω f = isos(f ) and ω g = isos(g) the isos encoding f and g, we build isos(f ; g) of type Z j ↔ Z j as:

isos(f ; g) =    let (y 1 , . . . , y j ) = ω f (x 1 , . . . , x j ) in (x 1 , . . . , x j ) ↔ let (z 1 , . . . , z j ) = ω g (y 1 , . . . , y j ) in (z 1 , . . . , z j )   
Definition 20 (Encoding of Parallel Composition). Let f ∈ RPP j and g ∈ RPP k , and ω f = isos(f ) and ω g = isos(g), we de ne isos(f || g) of type Z j+k ↔ Z j+k as:.

isos(f || g) =    let (x 1 , . . . , x j ) = ω f (x 1 , . . . , x j ) in (x 1 , . . . , x j , y 1 , . . . , y k ) ↔ let (y 1 , . . . , y k ) = ω g (y 1 , . . . , y k ) in (x 1 , . . . , x j , y 1 , . . . , y k )   
Definition 21 (Encoding of Finite Iteration). Let f ∈ RPP k , and ω f = isos(f ), we encode thenite iteration It[f ] ∈ RPP k+1 with the help of an auxiliary iso, ω aux , of type Z k ⊗ npos ↔ Z k ⊗ npos doing the nite iteration using npos, de ned as:

ω aux = fixg.                ( - → x , fold (inj l ())) ↔ let - → y = ω f - → x in ( - → y , fold (inj l ())) ( - → x , fold (inj r n)) ↔ let ( - → y ) = ω f ( - → x ) in let ( - → z , n ) = g ( - → y , n) in ( - → z , fold (inj r n ))                We can now properly de ne isos(It[f ]) of type Z k+1 ↔ Z k+1 as: isos(It[f ]) =                  ( - → x , inj l ()) ↔ ( - → x , inj l ()) ( - → x , inj r (inj l z)) ↔ let ( - → y , z ) = ω aux ( - → x , z) in ( - → y , inj r (inj l z )) ( - → x , inj r (inj r z)) ↔ let ( - → y , z ) = ω aux ( - → x , z) in ( - → y , inj r (inj r z ))                 
Definition 22 (Encoding of Selection). Let f, g, h ∈ RPP k and their corresponding isos

ω f = isos(f ), ω g = isos(g), ω h = isos(h). We de ne isos(If[f, g, h]) of type Z k+1 ↔ Z k+1 as: isos(If[f, g, h]) =      ( - → x , inj r (inj l z)) ↔ let - → x = ω f ( - → x ) in ( - → x , inj r (inj l z)) ( - → x , inj l ()) ↔ let - → x = ω g ( - → x ) in ( - → x , inj l ()) ( - → x , inj r (inj r z)) ↔ let - → x = ω h ( - → x ) in ( - → x , inj r (inj r z))     
Theorem 23 (The encoding is well-typed). Let f ∈ RPP k , then ω isos(f ) :

Z k ↔ Z k .
Theorem 24 (Simulation). Let f ∈ RPP k and n 1 , . . . , n k elements of Z such that f (n 1 , . . . , n k ) = (m 1 , . . . , m k ) then isos(f )(n 1 , . . . , n k ) → * (m 1 , . . . , m k ) Remark 25. Notice that isos(f ) ⊥ = isos(f -1 ), due to the fact that isos(f ) ⊥ will inverse the order of the let constructions, which will not be the case for isos(f -1 ). They can nonetheless be considered equivalent up to a permutation of let constructions and renaming of variable.

Proof Theorical Content

We want to relate our langage of isos to proofs in a suitable logic. As mentioned earlier, an iso ω ω : A ↔ B corresponds to both a computation sending a value of type A to a result of type B and a computation sending a value of type B to a result of type A. Therefore we want to be able to translate an iso into a proof isomorphism : two proofs π and π ⊥ of respectively A B and B A such that their composition reduces through the cut-elimination to the identity either on A or on B depending on the way we make the cut between those proofs. Since we are working in a linear system with inductive types we will use an extension of Linear Logic called µMALL : linear logic with least and greatest xed points, which allows us to reason about inductive and coinductive statements. µMALL also allows us to consider in nite derivation trees, which is required as our isos can contain recursive variables. We need to be careful though: in nite derivations cannot always be considered as proofs, hence µMALL comes with a validity criterion on in nite derivations trees (called pre-proofs) that tells us whether such derivations are indeed proofs. We recall brie y the basic notions of µMALL, while more details can be found in [START_REF] Baelde | Bouncing Threads for Circular and Non-Wellfounded Proofs: Towards Compositionality with Circular Proofs[END_REF].

C S L 2 0 2 3 36:10 A Curry-Howard Correspondence for Linear, Reversible Computation

F ≡ G F ⊥ , G id Σ, F Φ, F ⊥ Σ, Φ cut , Σ 1 1 F, G, Σ F `G, Σ ` F, Σ G, Φ F ⊗ G, Σ, Φ ⊗ F, Σ G, Σ F & G, Σ & Fi, Σ F1 ⊕ F2, Σ ⊕ i i ∈ {1, 2} Σ Σ, ⊥ ⊥ F [X ← µX.F ], Σ µX.F, Σ µ F [X ← νX.F ], Σ νX.F, Σ ν Figure 3
Rules for µMALL.

Background on µMALL

Given an in nite set of variables V = {X, Y, . . . }, we call formulas of µMALL the objects generated by A, B ::

= X | 1 | 0 | | ⊥ | A ⊗ B | A `B | A ⊕ B | A & B | µX.A | νX.
A where µ and ν bind the variable X in A. The negation on formula is de ned in the usual way:

X ⊥ = X, 0 ⊥ = , 1 ⊥ = ⊥, (A `B) ⊥ = A ⊥ ⊗ B ⊥ , (A ⊕ B) ⊥ = A ⊥ & B ⊥ , (νX.A) ⊥ = µX.A ⊥ having X ⊥ = X
is harmless since we only deal with closed formulas.

We call an occurrence, a word of the form α•w where α ∈ A fresh an in nite set of atomic addresses and its dual A ⊥ fresh = {α ⊥ | α ∈ A fresh } and w a word over {l, r, i} * (for left, right and inside) and formulas occurrences F, G, H, . . . as a pair of a formula and an occurrence, written A α Finally we write Σ, Φ for formula contexts: sets of formulas occurrences. We write

A α ≡ B β when A = B. Negation is lifted to formulas with (A α ) ⊥ = A ⊥ α ⊥ where (α • w) ⊥ = α ⊥ • w and (α ⊥ • w) ⊥ = α • w.
In general, we write α, β for occurrences.

The connectives need then to be lifted to occurrences as well:

Given # ∈ {⊗, ⊕, `, &}, if F = A αl and G = B αr then (F #G) = (A#B) α Given # ∈ {µ, ν} if F = A αi then #X.F = (#X.A) α
Occurrences allow us to follow a subformula uniquely inside a derivation. Since in µMALL we only work with formula occurrences, we simply use the term formula.

The (possibly in nite) derivation trees of µMALL, called pre-proofs are coinductively generated by the rules given in Figure 3. We say that a formula is principal when it is the formula that the rule is being applied to.

Among the in nite derivations that µMALL o er we can look at the circular ones: an in nite derivation is circular if it has nitely many di erent subtrees. The circular derivation can therefore be represented in a more compact way with the help of back-edges: arrows in the derivation that represent a repetition of the derivation. Derivations with back-edge are represented with the addition of sequents marked by a back-edge label, noted f , and an additional rule, Σ be(f ) , which represent a back-edge pointing to the sequent f . We take the convention that from the root of the derivation from to rule be(f ) there must be exactly one sequent annotated by f . Example 26. An in nite derivation and two di erent circular representations with back-edges. . . .

µ µX.X µ µX.X be(f ) µX.X µ f µX.X be(f ) µX.X µ µX.X µ f µX.X
While a circular proof has multiple nite representations (depending on where the back-edge is placed), they can all be mapped back to the same in nite derivation via an in nite unfolding of the back-edge and forgetting the back-edge labels: Definition 27 (Unfolding). We de ne the unfolding of a circular derivation P with a valuation v from back-edge labels to derivations by: U P :

P 1 , . . . , P n Σ r , v = U(P 1 , v), . . . , U(P n , v) Σ r U(be(f ), v) = v(f ) U P : P 1 , . . . , P n f Σ r , v = π = U(P 1 , v ), . . . , U(P n , v ) Σ r with v (g) = π if g = f else v(g).
µMALL comes with a validity criterion on pre-proofs that determines when a pre-proof can be considered as a proof: mainly, whether or not each in nite branch can be justi ed by a form of coinductive reasoning. The criterion also ensures that the cut-elimination procedure holds. For that, we can de ne a notion of thread [START_REF] Baelde | In nitary Proof Theory: the Multiplicative Additive Case[END_REF][START_REF] Baelde | Bouncing Threads for Circular and Non-Wellfounded Proofs: Towards Compositionality with Circular Proofs[END_REF]: an in nite sequence of tuples of formulas, sequents and directions (either up or down). Intuitively, these threads follow some formula starting from the root of the derivation and start by going up. If the thread encounters an axiom rule, it will bounce back and start going down in the dual formula of the axiom rule. It may bounce back again, when going down on a cut rule, if it follows the cut-formula. A thread will be called valid when it is non-stationary (does not follow a formula that is never a principal formula of a rule), and when in the set of formulas appearing in nitely often, the minimum formula (according to the subformula ordering) is a ν formula. For the multiplicative fragment, we say that a pre-proof is valid if for all in nite branches, there exists a valid thread, while for the additive part, we require a notion of additive slices and persistent slices which we do not detail here. Example 31 features an example of a valid proof together with its thread. More details can be found in [START_REF] Baelde | Bouncing Threads for Circular and Non-Wellfounded Proofs: Towards Compositionality with Circular Proofs[END_REF].

Translating isos into µMALL

We start by giving the translation from isos to pre-proofs, and then show that they are actually proofs, therefore obtaining a static correspondence between programs and proofs. We then show that our translation entails a dynamic correspondence between the evaluation procedure of our language and the cut-elimination procedure of µMALL. This will imply that the proofs we obtain are indeed isomorphisms, meaning that if we cut the aforementioned proofs π and π ⊥ , performing the cut-elimination procedure would give either the identity on A or the identity on B.

The derivation we obtain are circular, and we therefore translate the isos directly into nite derivations with back-edge, written circ(ω). We can de ne another translation into in nite derivations as the composition of circ() with the unfolding: ω = U(circ(ω)).

Because we need to keep track of which formula is associated to which variable from the typing context, the translation uses a slightly modi ed version of µMALL in which contexts are split in two parts, written Υ; Θ, where Υ is a list of formulas and Θ is a set of formulas associated with a term-variable (written x : F ). When starting the translation of an iso of type A ↔ B, we start in the context [A α ]; ∅ (for some address α) and end in the context []; Θ. The additional information of the variable in Θ is here to make sure we know how to split the contexts accordingly when needed later during the translation, with respect to the way they are split in the typing derivation. We write Θ = {F | x : F ∈ Θ} and Θ = {x : A | x : A α ∈ Θ}. We also use another rule which allow to send the rst formula from Υ to Θ and associate it a variable to the formula:

Υ; x : F, Θ G F :: Υ; Θ G ex(x)
C S L 2 0 2 3 36:12

A Curry-Howard Correspondence for Linear, Reversible Computation

Given a derivation ι in this system, we write ι for the function that sends ι into a derivation of µMALL where (i) we remove all occurrence of the exchange rule (ii) the contexts []; Θ becomes Θ.

Given an iso ω : A ↔ B and initial addresses α, β, its translation into a derivation of µMALL of A α B β is described with three separate phases: Iso Phase. The rst phase consists in travelling through the syntactical de nition of an iso, keeping as information the last encountered iso-variable bounded by a fix f.ω and calling the negative phase when encountering an iso of the form {v 1 ↔ e 1 | . . . | v n ↔ e n } and attaching to the formulas A and B two distinct addresses α and β and to the sequent as a label of name of the last encountered iso-variable. Later on during the translation, this phase will be recalled when encountering another iso in one of the e i , and, if said iso correspond to an iso-variable, we will create a back-edge pointing towards the corresponding sequents.

Negative Phase. Starting from some context [A α ], Θ, the negative phase consists into decomposing the formula A according to the way in which the values of type A on the left-hand-side of ω are decomposed. The negative phase works as follows: we consider a set of (list of values, typing judgement), written (l, ξ) where each element of the set corresponds to one clause v ↔ e of the given iso and ξ is the typing judgement of e. The list of values corresponds to what is left to be decomposed in the left-hand-side of the clause (for instance if v is a pair v 1 , v 2 the list will have two elements to decompose). Each element of the list Υ will correspond to exactly one value in the list l. If the term that needs to be decomposed is a variable x, then we will apply the ex(x) rule, sending the formula to the context Θ. The negative phase ends when the list is empty and hence when Υ = []. When it is the case, we can start decomposing ξ and the positive phase start. The negative phase is de ned inductively on the rst element of the list of every set, which are known by typing to have the same pre x, and is given in Figure 4.

Positive phase. The translation of an expression is pretty straightforward: each let and iso-application is represented by two cut rules, as usual in Curry-Howard correspondence. Keeping the variableformula pair in the derivation is here to help us know how to split accordingly the context Θ when needed, while Υ is always empty and is therefore omitted. While the positive phase carry over the information of the last-seen iso-variable, it is not noted explicitly as it is only needed when calling the Iso Phase. The positive phase is given in Figure 5.

Remark 28. While µMALL is presented in a one-sided way, we write Σ Φ for Σ ⊥ , Φ in order to stay closer to the formalism of the type system of isos.

Definition 29. circ(ω, S, α, β) = π takes a well-typed iso, a singleton set S of an iso-variable corresponding to the last iso-variable seen in the induction de nition of ω and two fresh addresses α, β and produces a circular derivation of the variant of µMALL described above with back-edges. circ(ω, S, α, β) is de ned inductively on ω:

circ(fix f.ω, S, α, β) = circ(ω, {f }, α, β) circ(f, {f }, α, β) = A α B β be(f ) circ({(v i ↔ e i ) i∈I } : A ↔ B, {f }, α, β) = Neg(([v i ], ξ i ) i∈I ) A α f B β
where ξ i is the typing derivation of e i .

Example 30. The translation circ(ω, ∅, α, β) of the iso ω from Example 9 is, with Proof Sketch. In order to show the validity of our derivation we need, for each in nite branch, to build a valid thread. From the previous lemmas and the syntactical constraints of the language, we get that any in nite branch is completely de ned by a single iso-variable, which allows us to reason entirely about a single recursive iso fix f.{v

F = A αl , G = B αrl , H = C αrr and F = A βrl , G = B βrr , H = C βl : Pos e () : 1 = []; ∅ 1 α 1 Pos x : A e x : A = []; x : A α A β id Pos   ξ Θ e t : A 1 Θ e inj l t : A 1 ⊕ A 2   = Pos(ξ) Θ (A 1 ) αl []; Θ (A 1 ⊕ A 2 ) α ⊕ 1 Pos   ξ Θ e t : A 2 Θ e inj r t : A 1 ⊕ A 2   = Pos(ξ) []; Θ (A 2 ) αr []; Θ (A 1 ⊕ A 2 ) α ⊕ 2 Pos   ξ 1 Θ 1 e t 1 ξ 2 Θ 2 e t 2 : A 2 Θ 1 , Θ 2 e t 1 , t 2 : A 1 ⊗ A 2   = Pos(ξ 1 ) []; Θ 1 (A 1 ) αl Pos(ξ 2 ) []; Θ 2 (A 2 ) αr []; Θ 1 , Θ 2 (A 1 ⊗ A 2 ) α ⊗ Pos   ξ Θ e t : ← µX.A] Θ e fold t : µX.A   = Pos(ξ) []; Θ (A[X ← µX.A]) αi []; Θ (µX.A) α µ Pos   ξ 1 Θ 1 e t 1 : A 1 ⊗ • • • ⊗ A n ξ 2 Θ 2 , x 1 : A 1 , . . . , x n : A n e t 2 : B Θ 1 , Θ 2 e let (x i ) i∈I = t 1 in t 2 : B   = Pos(ξ 1 ) []; Θ 1 F 1 ⊗ • • • ⊗ F n Neg(([(x i ) i∈I ], ξ 2 )) [F 1 ⊗ • • • ⊗ F n ]; Θ 2 B α []; Θ 1 , Θ 2 B α cut Pos   Ψ ω ω : A ↔ B ξ Θ e t : A Θ; Ψ e ω t : B   = Pos(ξ) []; Θ A circ(ω, {f }, α, β) [A]; ∅ B β []; Θ B β cut
1 ↔ e 1 | . . . | v n ↔ e n }.
For each in nite branch, we will build a pre-thread that follows the focus of the primitive recursive criterion. We know that the focus is a strict subvariable of the argument that is called recursively, as a consequence we can split the constructed thread into two parts, p 0 and p 1 , corresponding respectively to the negative phase and the positive phase. We also know that, each argument of a recursive call gives us a purely positive proof which is made only of tensors. We can show that the size of p 0 is bigger than p 1 and also that p 1 is a pre x of p 0 . This allows us to make sure that our pre-thread is a thread where the visible part always encounters a ν formula. Finally, the inductive type is decomposed in the negative phase and not in the positive phase (as the right-hand side of a recursive call is purely made of tensors), we can show that (i) the thread is never stationary and (ii) the thread has for minimal recurring formula that is visited in nitely often a ν formula, hence satisfying validity.

We can also show that the rewriting rules of the language simulate the cut-elimination procedure, as it is described in [START_REF] Baelde | Bouncing Threads for Circular and Non-Wellfounded Proofs: Towards Compositionality with Circular Proofs[END_REF]: Proof sketch. The proof relies on the de nition of a novel explicit substitution rewriting system for the language, called → eβ . Explicit substitution are represented as a series of let constructs where the substitution of a variable by a value only occurs when we reach the term let x = v in x. Each rewriting step of this system represents exactly one step of the cut-elimination procedure of µMALL.

Theorem
Then we only need to show that the explicit substitution rewriting system matches, meaning that if

σ = { - → x → - → v } then let - → x = - → v in e → * eβ σ(e).
This leads to the following corollary:

Corollary 39 (Isomorphism of proofs.). Given a well-typed iso ω ω : A ↔ B and two well-typed close value v 1 of type A and v 2 of type B and the proofs π : F 1 G 1 , π ⊥ : G 2 F 1 , φ : F 3 , ψ : G 2 corresponding respectively to the translation of ω, ω ⊥ , v 1 , v 2 then:

φ F 3 φ F 3 π F 1 G 1 G 1 cut π ⊥ G 2 F 2 F 2 cut ψ G 3 π ⊥ F 2 G 2 F 2 cut π F 1 G 1 G 1 cut ψ G 3

Conclusion

Summary of the contribution. We presented a linear, reversible language with inductive types. We showed how ensuring non-overlapping and exhaustivity is enough to ensure the reversibility of the isos. The language comes with both an expressivity result that shows that any Primitive Recursive Functions can be encoded in this language as well as an interpretation of programs into µMALL proofs. The latter result rests on the fact that our isos are structurally recursive.

Future works. We showned a one-way encoding from isos to proofs of µMALL, it is clear that there exists proof-isomorphisms of µMALL that does not correspond to an iso of our language, for instance taking the reversible map function on streams. Therefore, a rst extension to our work would be to consider a two-way encoding and adding coinductive types in the language. This would require relaxing the condition on recursive isos, as termination would be no longer possible to ensure. This is a focus of our forthcoming research.

A second direction for future work is to consider quantum computation, by extending our language with linear combinations of terms. We plan to study purely quantum recursive types and generalised quantum loops: in [START_REF] Sabry | From symmetric pattern-matching to quantum control[END_REF], lists are the only recursive type which is captured and recursion is terminating. The logic µMALL would help in providing a ner understanding of termination and non-termination

6 A

 6 Curry-Howard Correspondence for Linear, Reversible Computation σ[e] = e σ[inj l e] = inj l e σ[e] = e σ[inj r e] = inj r e σ = {x → e} σ[x] = e σ[e] = e σ[fold e] = fold e σ 2 [e 1 ] = e 1 σ 1 [e 2 ] = e 2 supp(σ 1 ) ∩ supp(σ 2 ) = ∅ σ = σ 1 ∪ σ 2 σ[ e 1 , e 2 ] = e 1 , e 2 σ[()] = ()

Figure 5

 5 Figure 5 Positive Phase

  38 (Simulation). Provided an iso ω ω : A ↔ B and values e v : A and e v : B, let π = Pos(ω v) and π = Pos(v), if ω v → * v then π → * cut-elim π .

Table 1

 1 Terms and types ∆ 1 ; Ψ e t 1 : A ∆ 2 ; Ψ e t 2 : B ∆ 1 , ∆ 2 ; Ψ e t 1 , t 2 : A ⊗ B

		∆; Ψ e t : A	∆; Ψ e t : B
	∅; Ψ e () : 1 x : A; Ψ e x : A	∆; Ψ e inj l t : A ⊕ B	∆; Ψ e inj r t : A ⊕ B
		∆; Ψ e t : A[X ← µX.A]
		∆; Ψ

e fold t : µX.A

Table 5

 5 Pattern-matching

Funding This work has been partially funded by the French National Research Agency (ANR) under the research projects SoftQPRO ANR17-CE25-0009-02 and RECIPROG ANR-21-CE48-019-01 and within the framework of "Plan France 2030", under the research project ANR-22-PETQ-0007.

https://hal.archives-ouvertes.fr/hal-03747425

Example 31. Considering the iso swap of type A ⊗ B ↔ B ⊗ A and its µMALL proof

Example 10 we give its corresponding proof π map(S) where F = (A ⊗ B) αirl and G = (B ⊗ A) βirl , then [F ] and [G] are respectively of address α and β:

We painted in blue the pre-thread that follows the focus of the structurally recursive criterion. During the negative phase which consists of the ν, &, `, ⊥ rules the pre-thread is going up, at each time going into the subformula corresponding to the focus. Then, during the positive phase the pre-thread is not active during the multiple cut rules until it reaches the id rule, where the pre-thread bounces and starts going down before bouncing back up again in the cut rule, into the in nite branch, where the behavior of the pre-thread will repeat itself. One can then show that this pre-thread is indeed a thread, according to [START_REF] Baelde | Bouncing Threads for Circular and Non-Wellfounded Proofs: Towards Compositionality with Circular Proofs[END_REF] and that it is valid: among the formulas it visits in nitely often, the minimal formula is [F ], which is a ν formula as since [F ] is on the left hand side of the sequent, we get

Lemma 32. Given π = circ(ω), for each in nite branch of π, only a single iso-variable is visited in nitely often.

Proof. Since we have at most one iso-variable, we never end up in the case that between an annotated sequent f and a back-edge pointing to f we encounter another annotated sequent.

Among the terms that we translate, the translation of a value yields what we call a Purely Positive Proof : a nite derivation whose only rules have for active formula the sole formula on the right of the sequent. Any such derivation is trivially a valid pre-proof.

C S L 2 0 2 3 36:14 A Curry-Howard Correspondence for Linear, Reversible Computation We can then de ne the notion of bouncing-cut and their origin:

Definition 35 (Bouncing-Cut). A Bouncing-cut is a cut of the form :

Due to the syntactical restrictions of the language we get the following:

Property 36 (Origin of Bouncing-Cut). Given a well-typed iso, every occurrence of a rule be(f ) in circ(ω) is a premise of a bouncing-cut.

In particular, when following a thread going up into a bouncing-cut, it will always start from the left-hand-side of the sequent, before going back down on the right-hand-side of the sequent. It will also always bounce back up on the bouncing-cut to reach the back-edge.

Theorem 37 (Validity of proofs). If ω ω : A ↔ B and π = circ(ω, ∅, α, β) then π satis es µMALL validity criterion from [START_REF] Baelde | Bouncing Threads for Circular and Non-Wellfounded Proofs: Towards Compositionality with Circular Proofs[END_REF].


Samy Brazane
email: samy.brazane@u-pec.fr

Olivier Riou

Fabien Delaleux

Laurent Ibos

Jean-Felix Durastanti

Thermal drift of infrared cameras remains a major problem for the accuracy and repeatability of radiometric measurements. To control the thermal drift, we developed a cold box to adjust the temperature of the FLIR A325sc camera housing. An error diagram is proposed to estimate the optimal camera operating temperature as a function of the ambient temperature for which the thermal drift is properly managed. The effectiveness of thermal drift compensation is examined on both camera functional ranges. The use of a cold box improves the thermal drift compensation efficiency and reduces the non-repeatability of irradiance measurements.

Conclusion

We checked the calibration of the FLIR A325sc camera. The latter is found calibrated for the range 1 [20-110] °C. Analysis of range 2 [0-350] °C highlights two major behaviors: 1. below 225°C, the thermal drift compensation is made difficult because of the self-heating of the measurement chain due to high intensity of black body irradiance and 2. as the optics of the camera screens the irradiance, the compensation takes over. It is not enough to counteract the self-heating of the lens becoming more absorbent. This effect can't be avoided during measuring situation for which the camera is continuously irradiated. As these effects are systematic, corrections of object's thermosignal are possible.

Camera features Black body

We used the Fluke 9100s thermometer calibrator. This commercial device was chosen because of its temperature range [35°C -375°C], its inter-cavity uniformity (0.07°C @ 50°C) and its accuracy of ±0.25°C @ 50°C. • Apparent emissivity of cavities is improved by coating wells using graphite based paint. • Cavities with a size larger than 9 IFOV offer high apparent emissivity. Reproducibility 0,004 0,005 0,007 0,005 0,006 0,006 Repeatability 0,002 0,002 0,002 0,002 0,002 0,002 Accuracy 0,004 0,005 0,004 0,004 0,004 0,004 Combined uncertainty 0,006 0,007 0,008 0,007 0,008 0,008 Thermal drift problem

Cold box

In our activities, we noticed a non-repetitiveness of the temperatures detected by the thermal camera FLIR A325sc as a function of the ambient temperature.

Thermal drift management

We verify the accuracy of the camera calibration within its two functional ranges : range 1: [-20; 120]°𝐶 and range 2: [0; 350]°𝐶. • Observed deviations within [20 -110] °C are regular in range 1. The offset shown in table are in same order of magnitude of black body temperature uncertainty (±0.25°C). It means that the camera can be considered as calibrated over the range [20 -110] °C. Thermal drift is well managed.

• Within range 2, deviations are consequent (2.5 𝑂𝑆 ≡ 1°𝐶 @ 60°𝐶) and exhibit an inflection at approximatively 225°C, denoting two different behaviors (zone 1 and zone 2). 225°C correspond to a Wien wavelength (5,8 μm) for which the camera lens becomes progressively opaque.

Within zone 1, the thermal compensation is made difficult because of the self-heating of the measurement chain due to the black body irradiance. The cold box is not able to counteract this phenomenon because it thermalizes only the housing.

Within zone 2, compensation of thermal drift takes over. However, it is not enough to counteract the self-heating of the lens becoming more absorbent. The thermal drift is reversed with a very marked slope.

This effect can be avoided during calibration process (short exposure) but not during measuring situation for which the camera is continuously irradiated.

Fig

  Fig. 1. Fluke 9100s Thermometer Calibrator

Fig. 4 .Fig. 5 .

 45 Fig. 4. Cold box. A thermocouple indicates the temperature of camera housing

Fig. 3 .

 3 Fig. 3. Observed deviations of 𝑡°𝐵 𝐵 -𝑡°𝑎 𝑝𝑝 and 𝑡°𝑐 𝑎𝑚 , versus 𝑡°𝑎 𝑚𝑏

962 0,973 0,984 0,988 0,987 0,988

	Cavity index	# 1	# 2	# 3	# 4	# 5	# 6
	Diameter F [mm] 1,6	3,2	4	4,8	4,8	6,4
	d /(D x IFOV)	3,2	6,4	8,0	9,6	9,6	12,8
	Average apparent emissivity	0,

Table 1 .

 1 Analysis of deviations within range 1


J Khatua

S Bhattacharya

Q P Ding

S Vrtnik

A M Strydom

N P Butch

H Luetkens

M. S Edwin Ramachandra Kermarrec

A Rao

Zorko

M S Ramachandra Rao

A Zorko

Y Furukawa

P Khuntia

Spin liquid state in a rare-earth hyperkagome lattice

published or not. The documents may come   L'archive ouverte pluridisciplinaire

I. INTRODUCTION

Quantum materials wherein superposition and entanglement are at play may exhibit exotic physical phenomena, such as spin liquids with fractional quantum numbers coupled to emergent gauge field that offer a novel paradigm in advancing quantum science and technology [1][2][3][4]. The experimental realization of quantum spin liquid with exotic collective excitations in quantum materials set an outstanding track in modern condensed matter since the seminal proposal of P. W. Anderson in 1973 [5,6]. Quantum spin liquids (QSLs) are characterized by absence of magnetic order down to T = 0, long-range entanglement, coherent fluctuation of spins and the preservation of local symmetries despite strong exchange interaction between spins [6][7][8][9]. Fractionalization of quantum numbers is a fingerprint of QSLs which are different from spin waves in conventional magnets. This is a well established scenario in one-dimensional (1D) magnets. It has been suggested that also 2D and 3D QSLs can host fractionalized deconfined quasiparticles such as spinons and * pkhuntia@iitm.ac.in Majorana fermions the understanding of which is essential in advancing fundamental physics and is highly relevant for fault-tolerant quantum computing [6,[10][11][12][13][14][15][16][17]. However, the presence of perturbations, such as extra exchange couplings, unavoidable disorder, and defects in real materials put a strong constraint for the ideal realization of quantum spin liquids with D ≥ 2 [18][19][20]. Moreover, 3D spin lattices that are composed of small triangular motifs in edge-or corner-sharing fashion, can host strong frustration similar to 2D spin lattices. Namely, quantum fluctuations in such 3D frustrated lattices with low value of spin could lead to unconventional ground states including spin liquids [11,12]. This has motivated us to explore new quantum materials with rich potential to host such states with fractional quantum numbers [21][22][23]. The intertwining of spin-orbit coupling, anisotropy, spin correlations and frustration in rare-earth magnets offer another route to realize novel quantum states [4,7,[24][25][26]. In recent years, spin-orbit driven frustrated magnets have provided a new light to realize novel quantum phenomena ranging from spin ice state [7,27] to spin liquid [15,24,28] and anomalous and spontaneous Hall effect [29,30] to Bose-Einstein condensate phase [25,31]. In lanthanide magnetic materi-als, the interplay between spin-orbit coupling and lowsymmetry crystal electric field leads to Kramers doublets where effective J eff = 1/2 moments of rare-earth ions appear, contrary to pure S = 1/2 moments in transition metal ions. The 3D spin lattice based quantum magnets host a plethora of unconventional properties of 3D magnets including non-trivial short-range spin correlation [32], unconventional spin glass [33], and magnetic Coulomb phase [34,35]. For example, the lanthanide family A 2 B 2 O 7 where rare-earth ions form a pyrochlore lattice is a rich reservoir that hosts a wide range of quantum phenomena owing to complex interplay between competing degrees of freedom [7,36]. Quite recently, Ce 2 Zr 2 O 7 was proposed to be a 3D QSL candidate, where Ce 3+ ions with J eff = 1/2 moments decorate a network of corner-sharing tetrahedra [37]. The observation of U (1) QSL and emergent phases driven by multipolar interactions in its analogue Ce 2 Sn 2 O 7 also set a unique example of a 3D spin-lattice for exploring quantum many-body phenomena [38]. Furthermore, the garnet series R 3 B 5 O 12 (R = rare-earth ions and B = Ga and Al) where the rare-earth ions decorate two interpenetrating hyperkagome lattices are known to harbor myriads of interesting quantum phenomena such as long-range multipolar state [39,40] and Ising antiferromagnets [41,42]. However, most of the garnets undergo a magnetic phase transition at lower temperature [43][44][45][46][47][48][49]. Therefore, the search for an ideal 3D spin lattice to realize a QSL state poses a particularly challenging problem. For example no report has been published so-far on a structurally perfect 4f -based hyperkagome lattice in which high degree of spin frustration and anisotropic interactions mediated by spin-orbit coupling could stabilize an enigmatic 3D spin liquid. Here, we report a new rare-earth based quantum magnet Li 3 Yb 3 Te 2 O 12 and investigate its inherent physics of 3D frustrated spin-lattice with J eff = 1/2 moments of Yb 3+ ions. Li 3 Yb 3 Te 2 O 12 crystallizes in the cubic space group Ia 3d where Yb 3+ ions form an interpenetrating hyperkagome spin-lattice. Our thermodynamic results suggests the presence of a Kramers doublet state and antiferromagnetic interaction between J eff = 1/2 spins at low temperature. The absence of long-range magnetic ordering and spin freezing down to at least 38 mK in our ac susceptibility, specific heat and NMR experiments is the first fingerprint of a spin liquid state in this frustrated quantum material. Furthermore, specific heat measurements show the presence of short-range spin correlations in this antiferromagnet. Our complementary experimental probes thus demonstrate a dynamic ground state and a field-induced gapped behavior in the spin excitation spectrum in this spin-orbit driven frustrated hyperkagome quantum material.

II. METHODS

Sample synthesis:

Polycrystalline samples of Li 3 Yb 3 Te 2 O 12 (henceforth LYTO) were synthesized by a standard solid-state reaction of Li 2 CO 3 (99.0 %, Alfa Aesar), Yb 2 O 3 (99.998 %, Alfa Aesar), and TeO 2 (99.9995 %, Alfa Aesar) [50]. Since the lanthanide-oxide and Li 2 CO 3 are generally hygroscopic, before being weighted, Yb 2 O 3 and Li 2 CO 3 were preheated at 900 • C and 100 • C, respectively. The stoichiometric mixtures of starting materials were pelletised and heated at 800 • C for 30 hours in air with several intermittent grindings. We also used Y 2 O 3 (99.999 %, Alfa Aesar) and followed the same procedure to prepare the isostructural nonmagnetic analogue Li 3 Y 3 Te 2 O 12 . The phase purity was checked by room temperature powder X-ray diffraction (XRD) using smartLAB Rigaku X-ray diffractometer with Cu Kα radiation (λ =1.54 Å). The crystal structure of LYTO was confirmed by the Rietveld refinement of X-ray diffraction data using GSAS software [51]. All the XRD peaks could be indexed with the cubic space group Ia 3d and lattice parameter a = 12.173 Å [50]. No secondary phase is detected in XRD and the Rietveld refinement of XRD data rules out the presence of any inter-site disorder between the constituent atoms. The observed sharp XRD peaks indicate high quality polycrystalline samples investigated in this work. Magnetization measurements: Magnetization data were acquired using a Quantum Design, SQUID magnetometer in the temperature range 2 K ≤ T ≤ 350 K. Magnetic susceptibility (χ(T)) data were recorded in magnetic fields 0.1 and 1 T and the zero-field cooled (ZFC) and field cooled (FC) data were collected in a magnetic field of 0.01 T. In order to determine the effective magnetic moment (µ eff ) and Curie-Weiss temperature (θ CW ), the high-temperature (>160 K) inverse susceptibility (1/χ(T)) data were fitted with Curie-Weiss (CW) law χ = χ 0 + C /(T -θ CW ). Here C is the Curie constant which is used to calculate µ eff = √ 8C µ B , χ 0 is the temperature independent paramagnetic susceptibility, and θ CW provides an estimate of magnetic exchange interactions. The isotherm magnetization data are reproduced well (see SI Fig. 3) by a function of the form M /M s = B 1/2 (y), where

B J (y) = [ 2J+1 2J coth[ y(2J+1) 2J ] -1 2J coth y 2J ]
is the Brillouin function, M s (= gJµ B ) is the saturation magnetization and the parameter y = gµ B Jµ 0 H/k B T , where µ B is the Bohr magneton, g is the Landé g-factor. The Brillouin function fit with fixed J = 1/2 to magnetization data yields Landé g factor, g = 3.54 ± 0.02. Specific heat measurements: Specific heat measurements were performed in the temperature range 0.35 K ≤ T ≤ 270 K under magnetic fields 0 T ≤ µ 0 H ≤ 7 T, using thermal-relaxation technique provided by Quantum Design, PPMS. Furthermore, specific heat measurements were carried out separately in the temperature range 0.054 K ≤ T ≤ 4 K in zero-field using a dilution refrigerator which was also used to measure ac

T ( K ) 0 . 1 T 1 T ( b ) ( d ) ( c ) 1/χ (m o l / c m 3 ) T ( K ) 1 T χ ' ( a r b . u n i t s ) T ( K ) 1 0 K H z 4 K H z 1 K H z 0 . 4 K H z 0 . 1 K H z 4 0 H z ( a ) H a c = 3 O e FIG.
1. Crystal structure and bulk magnetic properties of LYTO. (a) The position of the Yb 3+ magnetic ions within the unit cell. These Yb 3+ ions decorate two interpenetrating chains of 3D corner-shared triangles known as the hyperkagome lattice. (b) Rietveld refinement of powder X-ray diffraction data recorded at room temperature. The experimentally observed points (circles), the calculated Rietveld refinement profile (solid line), the Bragg reflection positions (olive vertical bars) and the difference between the observed and calculated intensity (blue line) are shown. (c) The temperature dependence of magnetic susceptibility in two magnetic fields. The inset shows the temperature dependent inverse magnetic susceptibility data with the orange and red lines showing the Curie-Weiss fits for the low-and high-temperature data, respectively. (d) The temperature dependence of the real part of ac susceptibility at different frequencies down to 45 mK.

susceptibility in the temperature range 0.045 K ≤ T ≤ 4 K at six different frequencies using a Dynacool PPMS instrument from Quantum Design. The total specific heat of LYTO can be expressed as a sum of contributions from the electronic spins in the ground state Kramers doublet (C mag ), lattice contribution (C lat ) and nuclear contribution (C n ) i.e., C tot (T ) = C mag (T ) + C lat (T ) + C n . We also measured specific heat of the Li 3 Y 3 Te 2 O 12 which we used as a non-magnetic analogue to subtract the lattice contribution. After subtraction lattice contribution, we subtracted nuclear Schottky contribution C n ∝ T -2 to obtain magnetic specific heat. NMR measurements: Field-swept 7 Li (I = 3/2, and gyromagnetic ratio 16.54 MHz/T) NMR measurements down to 38 mK at several frequencies were carried out on a homemade phase-coherent spin-echo pulse spectrometer equipped with a 9 T Oxford magnet. The low temperature NMR measurements were performed with a Oxford Kelvinox dilution refrigerator. NMR spectra measurements were carried out using a standard Han-echo sequence while the spin lattice relaxation time measurements were performed following saturationrecovery method. In LYTO, 7 Li is an NMR active nucleus which couples with Yb 3+ ions via hyperfine interactions. Therefore, 7 Li NMR can probe the intrinsic magnetic susceptibility as well as low-energy spin excita-tions via spectrum position, and spin-lattice relaxation, respectively. The temperature dependence of the NMR shift (K) at different frequencies was extracted from the fit of field-swept NMR spectra. For an anisotropic magnetic material three different components of NMR shift K (T ) such as K iso (isotropic shift), K ax (axial shift) and K aniso (anisotropic shift), arising from a general hyperfine coupling tensor, can be determined from the observed experimental line shape. In this respect, the principal components K X , K Y and K Z of tensor K (T ) can be used to define [52,53]. The temperature dependence of the NMR shift scales with the magnetic susceptibility as

K iso = 1/3(K X + K Y +K Z ), K aniso = 1/2(K Y -K X ) and K ax = 1/6(2K Z -K X -K Y )
K ax/iso (T) = K 0 + (A ax/iso hf /N A µ B )χ spin (T)
, where K 0 is the temperature independent chemical and orbital shift, A hf is the hyperfine coupling constant between 7 Li nucleus and Yb 3+ spins, µ B is the Bohr magneton and N A is the Avogadro number, respectively. To extract the hyperfine couplings, the standard Clogston-Jaccarino plot (see SI Fig. 7) was used to fit in two temperature regimes and the obtained fitting parameters are given in SI note 5. The fit of NMR spectra below 1 K is not very good (see SI Fig. 6) which could be due to an additional spectral weight in the low-field side at low temperature,however, the origin is not clear at this moment. To uncover the dynamics of Yb 3+ spins in LYTO at very low-energy, we conducted spin-lattice relaxation time measurement. In order to estimate T -1

1 , the recovery of longitudinal nuclear magnetization data were fitted by the single exponential function M z (t) = (M 0 -M (t))/M 0 = A exp(-t/T 1 ) in the entire temperature range of the investigation, where M 0 is the equilibrium magnetization, M z (t) is the magnetization at time t after the saturation pulse and A is a constant. The validity of a single exponential function in a wide temperature range suggests that the electronic moments are uniformly distributed in the host lattice without disorder. The fits of the recovery curves with a formula for I = 3/2 nuclei were not as good as the single exponential function. µSR: Muon spin relaxation measurements were performed at the Paul Scherrer Institute, on the GPS instrument. A weak transverse field of 50 Oe was applied to determine the initial asymmetry parameter. Zero-field (ZF) and longitudinal applied fields (LF) datasets were obtained using VETO mode resulting in minimal background signal (< 0.02). Inelastic neutron scattering: Time-of-flight inelastic neutron scattering measurements were carried out at the NIST Center for Neutron Research (NCNR, Gaithersburg, MD) on the DCS spectrometer. In order to isolate the field evolution of the inelastic spectrum, a field-independent background, made of the average of the 0 and 2T datasets for E > 0.85 meV and of the average of the 7, 8, 9 and 10 T datasets for E < 0.85 meV, was subtracted from the Q-integrated energy cuts. Simulations of powder-averaged dynamical structure factor for inelastic neutron scattering were done with the SpinW software [54].

III. RESULTS

A. Magnetization

The magnetic susceptibility χ(T ) data do not exhibit any signs of a magnetic phase transition down to 2 K (Fig. 1 (c)). The Curie-Weiss (CW) fit to the hightemperature (>160 K) χ(T ) data yields θ CW ≈ -78 (1) K, µ eff = 4.4 µ B , which is close to µ eff = 4.54 µ B of a free Yb 3+ (J = 7/2) spin and χ 0 = 4.97 × 10 -4 cm 3 /mol. The estimated large negative θ CW is ascribed to the energy scale of excited crystal electric field levels [24]. The interaction energy scale of 4f systems is much lower and is in our case revealed at low-temperature where the CW fit of 1/χ(T ) data in the temperature range 2 K ≤ T ≤ 10 K yields µ eff = 3.0 µ B and θ CW ≈ -0.3 K ± 0.03 K. The obtained effective moment is smaller than the Yb 3+ free-ion value, which suggests a Kramers doublet state at low temperature, as also confirmed by specific heat measurements (see below). The negative CW temperature indicates antiferromagnetic interactions between the pseudo 1/2 moment of Yb 3+ ions with approximate interaction energy of the order of θ CW . The Curie-Weiss temperature of most 4f systems is typically small and thus the onset of spin correlation develops at very low temperature in these quantum materials [37,38,42,55,56]. Furthermore, the absence of any bifurcation in zero-field cooled (ZFC) and field cooled (FC) susceptibility data (see SI Fig. 2) in the field of 100 Oe suggests that Yb 3+ spins are not frozen down to 2 K. In order to confirm the absence of spin freezing, we performed ac susceptibility measurement down to millikelvin temperatures at different frequencies. Fig. 1 (d) depicts the real part of ac susceptibility as a function of temperature down to 45 mK and it exhibits a broad maximum around 80 mK which suggests the short range interaction between Yb 3 + moments in LYTO [57][58][START_REF] Zhong | Proc. Natl. Acad. Sci[END_REF]. Importantly, the absence of any frequency dependency of ac susceptibility strongly rules out glassy behavior of Yb 3+ spins in LYTO. The magnetization isotherms at a few selected temperatures are shown in SI Fig. 3 and the absence of any visible hysteresis rules out the presence of any ferromagnetic signal. The calculated Landé g factor, g = 3.46 ± 0.02, from the low-temperature Curie-Weiss fit of magnetic susceptibility, is close to that obtained Landé g factor from Brillouin function fit of the magnetization isotherm. A similar value of powder average of Landé g factor is also observed in Yb based 3D pyrochlore system suggesting the single-ion properties of LYTO are expected to be similar to the pyrochlore system [58].

T ( K ) L i 3 Y b 3 T e 2 O 1 2 L i 3 Y 3 T e 2 O 1 2 ( a ) m 0 H = 0 T ∆S ( J / K . m o l Y b ) T ( K ) R l n 2 ( c ) 5 C m a g ( J / K . m o l Y b ) T ( K ) 0 T 1 T 2 T 3 T 5 T 7 T ( b ) FIG.
2. Specific heat of LYTO in various magnetic fields. (a) The temperature dependence of specific heat (Cp) of LYTO and its non-magnetic analog Li3Y3Te2O12 in zero-magnetic field. (b) Low-temperature magnetic specific heat (Cmag(T )) after subtraction of lattice and nuclear contributions in zero-field as well as non-zero field. (c) The temperature dependence of entropy change (∆S = Cmag(T )/T dT , the temperatures of the color plots correspond to those in (b).) for magnetic fields up to 7 T with the expected entropy (R ln 2 for spin-1/2) indicated by a black dashed line.

B. Specific heat

Fig. 2 (a) shows the total specific heat measured in zero-magnetic field. The absence of any λ-type peak suggests that there is no phase transition down to 54 mK. After subtracting the lattice contribution using the nonmagnetic analog Li 3 Y 3 Te 2 O 12 and the nuclear contribution associated with the hyperfine splitting of the Yb 3+ nuclear spin multiplet [START_REF] Steppke | [END_REF], the resulting temperature dependence of magnetic specific heat, C mag (T ) is shown in Fig. 2 (b) in the temperature range 54 mK ≤ T ≤ 10 K. Below 2 K, the zero-field magnetic specific heat, C mag (T ) starts increasing and shows a broad maximum around 0.18 K, which indicates the presence of short-range spin correlations between Yb 3+ moments [28]. The presence of broad maximum around 0.18 K agrees well with the estimated CW temperature at low temperatures and it is consistent with general expectation for a quantum spin liquid candidate [58]. In finite applied magnetic fields, it is observed that the broad maximum shifts to higher temperatures with increased field which opens gap owing to Zeeman splitting of the lowest Kramers doublet state. It is worth noting that we have not observed any suppression of C mag (T ) in presence of magnetic field thus ruling out the presence of disorder [61]. Therefore, there is no uncertainties in Schottky contribution due to the effect of disorder in the extracted C mag (T ) data. It is observed that the gap size increases with the increasing magnetic fields linearly (see SI Figs. 4 and9) and the fit yields g = 3.34 ± 0.01 which is consistent with that obtained Landé gfactor from bulk magnetization measurements. The magnetic field induced Zeeman gap in magnetic specific heat data is observed at very low-temperature in several rareearth based spin-liquid candidates with relatively small exchange interactions compared to the Zeeman splitting [37, 61]. In Fig. 2 (c), we present the estimated entropy change, ∆S, by integrating C mag (T )/T data in the temperature range 0.054 K ≤ T ≤ 16 K and 0.35 K ≤ T ≤ 16 K for zero-field and finite magnetic fields, respectively. The total entropy (Rln2) expected for J eff = 1/2 state is fully recovered for zero-field as well as for non-zero magnetic fields. This provides the concrete evidence of a Kramers doublet ground state of Yb 3+ spins in LYTO at low temperature.

C. Muon spin relaxation

We also performed muon spin relaxation (µSR), to confirm the absence of static magnetism on a local scale.

With its spin I = 1/2 and gyromagnetic ratio γ µ /2π = 135.5 MHz/T, an implanted muon is an unbeatably sensitive probe of magnetism. Fig. 3 shows the muon asymmetry obtained in zero (ZF) and longitudinal (LF) applied field configurations down to 1.57 K. The ZF relaxation shape is nearly exponential in the T -range 1.57-50 K. A fit of the asymmetry using a stretched exponential function A(t) = e -(λt) β leads to large β ∼ 0.8 -1 values. This is typical of strongly fluctuating local fields and, indeed, relaxation under LF remains almost unchanged, except for the highest field of 7500 Oe, corroborating the dynamical character of Yb 3+ moments. We further investigated this dynamics through temperature dependence of the muon spin relaxation rate λ (Fig. 3). Above 20 K, the strong relaxation (∼ 1.85 µs -1 ) is typical of other related 4f rare-earth based magnetic materials, such as

1 . 0 1 . 2 1 . 4 1 . 6 0 . 0 1 0 . 1 1 1 0 1 0 0 -4 -2 0 2 4 0 . 1 1 1 0 1 0 0 1 E -5 0 . 0 1 1 0 0 1 2 3 4 5 1 E -5 0 . 0 1 1 0 1 / T ( K -1 ) 6 . 0 4 K 5 . 2 3 K 4 . 5 3 K 4 . 3 0 K 3 . 4 6 K 2 . 9 7 K 2 . 4 6 K 1 . 8 6 K 1 . 3 5 K 1 . 2 0 K 1 . 1 0 K 1 . 0 0 K 0 . 9 0 K 0 . 8 0 K 0 . 7 0 K 0 . 6 0 K 0 . 5 0 K 0 . 4 0 K 0 . 3 0 K 0 . 2 0 K 0 . 1 0 K S p i n -e c h o i n t e n s i t y ( a r b . u n i t s ) m o H ( T ) 7 L i N M R f = 2 0 . 5 M H z 0 . 0 3 8 K T ( K ) ( a ) ( b ) ( c )
K i s o , K a x ( % ) T ( K ) K i s o ( 4 9 . 6 2 9 M H z ) K a x ( 4 9 . 6 2 9 M H z ) K i s o ( 2 0 . 5 M H z ) K a x ( 2 0 . 5 M H z ) ( d ) 2 0 . 5 M H z ( m 0 H ∼ 1 . 2 4 T ) 4 9 . 6 2 M H z ( m 0 H ∼ 3 T ) 7 9 M H z ( m 0 H ∼ 4 . 8 T ) 1 / T 1 ( 1 0 3 s -1
)

7 L i N M R 1 / T 1 ( 1 0 3 s -1
) FIG. 4. 7 Li NMR spectra and spin-lattice relaxation rate in various magnetic fields reflecting the spin dynamics in the QSL state of LYTO. (a) 7 Li NMR spectra measured at constant frequency ν = 20.5 MHz at a few representative temperatures. The orange vertical line corresponds to zero-shift reference line at 1.238 T. (b) The temperature dependence of isotropic (Kiso) and axial (Kax) 7 Li NMR shifts of LYTO where the solid line is the scaled magnetic susceptibility measured in 1 T. (c) The temperature dependence of the 7 Yb 3 Ga 5 O 12 or Yb 2 Ti 2 O 7 , and is consistent with fast fluctuations assuming a similar local field amplitude [32]. The slight decrease of λ at low temperatures can be understood in the context of the presence of antiferromagnetic spin correlations, and the first-order 1/T -expansion λ(T ) = λ (∞) (1 + θ CW /T ) [62] gives a crude estimate of θ CW = -0.25(5) K (the red line in Fig. 3 (c)), in agreement with magnetization measurements.

D. Nuclear magnetic resonance

We carried out NMR experiments in LYTO in order to confirm the absence of magnetic ordering down to the lowest experimentally accessible temperatures and to track static and dynamic susceptibilities. 7 Li NMR spectra are relatively narrow at room temperature (See SI Fig. 5), however, they exhibit marked broadening below 10 K due to anisotropic interactions and the development of Yb 3+ electron spin correlations. We observed no de- (e-f) Intensity versus energy for the Q-integrated region [0, 1.5] Å-1 for the zero-field dataset (e) and some selected datasets under applied fields (from which a field-independent background has been subtracted) (f). Experimental data points are symbols, purple line the estimated elastic contribution of the zero-field data and blue line is the Lorentzian quasi-elastic contribution. Solid black lines in (f) are simulations assuming an axially symmetric g-tensor (see text). (g) Median position of the spectrum as a function of the applied field (black squares). Red solid line is a linear fit.

tectable line corresponding to the satellite transitions on both sides of the central transition, which indicates the presence of a very weak quadrupole interaction. Furthermore, the line shape was found asymmetric indicating the presence of either asymmetry in the hyperfine coupling between the Li nucleus and Yb 3+ spins or asymmetry in spin susceptibility at low-temperature, both leading to asymmetry in hyperfine fields. The smooth evolution of the NMR spectra in the entire temperature range rules out the presence of a long-range magnetic ordering at least down to 38 mK. The observation of clear shift of spectra in Fig. 4 (a) uniquely determines the intrinsic uniform static spin susceptibility on a microscopic scale. It is independent and saturates to a finite value in the low-temperature limit due to the strong polarization of the Yb 3+ moments under the applied magnetic field. Fig. 4 (b) presents the temperature dependence of the isotropic NMR shift, K iso , and the axial shift K ax , that were extracted from the fitting of NMR spectra. At high-temperatures both K iso and K ax scale with bulk magnetic susceptibility as expected due to significant hyperfine coupling between 7 Li nuclei and Yb atoms (see SI Fig. 7). The scaling of K with χ indicates that the macroscopic magnetization is intrinsic and originates from Yb 3+ electronic moments while any impurity contributions are negligible. The NMR shift reveals the presence of anisotropic hyperfine field as expected for 4f quantum magnets possibly associated with spin-orbit interactions. The nuclear spin-lattice relaxation rate (T -1 1 ) probes the wave-vector q-averaged low-energy spin excitations owing to dynamical electron spin susceptibility in the ground state of correlated quantum materials. ∝ exp (-∆/k B T ) yield a straight line with a slope proportional to the gap [63,64]. We observe that the obtained gap indeed scales linearly with the applied magnetic field (see SI Fig. 9), which is consistent with the specific heat results. In addition, three distinct energy regimes are also observed in the spin-spin relaxation rate (T -1 2 ; see SI Fig. 8). The absence of any peak feature in the temperature dependence of T -1 1 rules out the presence of any phase transition also from the spin dynamics perspective down to 200 mK, the lowest temperature that was reached in our spin-lattice relaxation experiment. NMR results thus reveal the presence of a dynamic ground state down to 38 mK with a fieldinduced owing to Zeeman splittings of the Kramers doublet state.

E. Inelastic neutron scattering

In order to investigate in more detail the nature of excitations at low-energy, we carried out inelastic neutron scattering measurements on the cold neutron time-of-flight instrument (DCS) at the NCNR (Gaithersburg, MD). Fig. 5 shows the dynamical structure factor measured for an incident energy E i = 3.27 meV with a resolution of 0.11 meV (FWHM). The inelastic spectrum of the zero-field dataset is essentially featureless (Fig. 5 (a)). The Q-intregated energy cut (Fig. 5 (e)) can be well fitted to an elastic Gaussian line plus a quasi-elastic Lorentzian profile, S(Q, E) ∼ (1 -e -E/k B T ) -1 EΓ/(E 2 + Γ 2 ), accounting for the magnetic contribution. In agreement with the NMR and µSR results, the Yb 3+ ions are found to be in a paramagnetic fluctuating regime characterized by a quasi-elastic line with the linewidth Γ = 0.05(2) meV setting an upper value of the energy scale of the interactions (∼ 0.6 K), which is consistent with all other results. Upon increasing the field, a non-dispersive mode emerges from the elastic line (Fig. 5 b-d) whose median position depends linearly on the applied field (Fig. 5 g). It is ascribed to the Zeeman splitting of the effective spin J eff = 1/2 of the Kramers doublet. Fig. 5 (f) shows Q-integrated energy cuts for different applied fields, which further reveal the presence of two humps whose center to center distance increases with fields. This spectrum is characteristic of an axially symmetric g-tensor [START_REF] Abragam | Electron paramagnetic resonance of transition ions[END_REF]. To further extract the values of the g-tensor along the local anisotropy axis, g z = g , and in the perpendicular plane, g xx = g yy = g ⊥ , we simulated the powder-averaged dynamical neutron structure factor (black lines in Fig. 5f) and found g = 4.0 (1) g ⊥ = 2.85 (5), that account for all the datasets from 2 to 9 T. This leads to the powder-average value g = g 2 /3 + 2g 2 ⊥ /3 = 3.27 (7), which is in reasonable agreement with that obtained from other experiments.

IV. SUMMARY

In the 3D rare-earth based quantum material Li 3 Yb 3 Te 2 O 12 featuring a perfect hyperkagome lattice constituted by Yb 3+ ions, our results using several complementary experimental techniques reveal that Yb 3+ realizes a Kramers doublet and hence an effective J eff = 1/2 degrees of freedom captures the essence of the low energy physics in the ground state. The Yb 3+ spins remain dynamic, which is characterized by quasi-elastic INS line in inelastic neutron scattering experiments and J eff = 1/2 moments interacting with an energy of 0.6 K, which is rather low but typical for 4f -based quantum materials. Furthermore, ac susceptibility data show no sign of spin freezing down to 45 mK. The lack of phase transition down to 54 mK is evidenced also by the magnetic specific heat data and a broad maximum around 0.18 K in zero-field is attributed to the presence of short-range spin-correlations. The compound thus presents an interesting setting wherein geometrical frustration conspires with quantum fluctuations to evade magnetic long-range ordering as further revealed by our NMR results down to 38 mK that is consistent with ac susceptibility and specific heat results, the primary hallmark of a dynamic ground state. A field induced gap was evidenced in the specific heat, NMR relaxation rate and neutron scattering results which is reconciled with the Zeeman splitting of the effective spin J eff = 1/2 of the Kramers doublet. The 4f moments on a hyperkagome lattice-an emblematic frustrated three dimensional model offer a rare realization of a spin liquid. Our comprehensive results demonstrate a liquid-like dynamic state in a rare-earth hyperkagome, which might open the possibility of stabilizing spin-orbit driven quantum disordered state in 4f magnets. This new family of rare-earth hyperkagome quantum material Li 3 RE 3 Te 2 O 12 holds great potential to realize spin-orbit driven quantum phenomena and opens new avenues for modern theoretical approaches in establishing generic frameworks in the context of spin liquids.

FIG. 3 .

 3 FIG. 3. µSR data confirming a dynamic ground state in LYTO. Muon asymmetry decay obtained in ZF (a) and various LFs at 1.57 K (b) (symbols). The datasets have been shifted vertically by 0.05 for clarity. Lines are fits to a stretched exponential function (see text). The temperature (c) and longitudinal field (d) dependence of the muon spin relaxation rate λ extracted respectively from (a) and (b). The red line shows the 1/T -expansion of λ(T ) and indicates the presence of antiferromagnetic correlation (see text). Error bars depict an uncertainty of one standard deviation.

1 1

 1 FIG.4.7 Li NMR spectra and spin-lattice relaxation rate in various magnetic fields reflecting the spin dynamics in the QSL state of LYTO. (a)7 Li NMR spectra measured at constant frequency ν = 20.5 MHz at a few representative temperatures. The orange vertical line corresponds to zero-shift reference line at 1.238 T. (b) The temperature dependence of isotropic (Kiso) and axial (Kax)7 Li NMR shifts of LYTO where the solid line is the scaled magnetic susceptibility measured in 1 T. (c) The temperature dependence of the7 Li NMR spin-lattice relaxation rate (T -1 1 ) for three different fields in log-log scale. (d) T -1 1 as a function of inverse temperature (T -1 ) for different fields in semi-log scale. The black line represents a fit to a phenomenological model valid for thermally activated behavior of T -1 1 as discussed in the text. Error bars depict an uncertainty of one standard deviation.

FIG. 5 .

 5 FIG. 5. Inelastic neutron scattering. (a-d) Intensity maps of the dynamical structure factor S(Q, E) for polycrystalline LYTO measured at T = 1.5 K under zero applied field (a), µ0H = 2 T (b), µ0H = 4 T (c) and µ0H = 5 T (d).(e-f) Intensity versus energy for the Q-integrated region [0, 1.5] Å-1 for the zero-field dataset (e) and some selected datasets under applied fields (from which a field-independent background has been subtracted) (f). Experimental data points are symbols, purple line the estimated elastic contribution of the zero-field data and blue line is the Lorentzian quasi-elastic contribution. Solid black lines in (f) are simulations assuming an axially symmetric g-tensor (see text). (g) Median position of the spectrum as a function of the applied field (black squares). Red solid line is a linear fit.

Fig. 4 ( 1 1 1 1 1 1 1 1 1 1 1 1 1 1

 41111111 c) shows the temperature dependence of T -in three different magnetic fields, which exhibits the present of three different relaxation regimes. Upon lowering the temperature from 300 K, T -increases in the intermediate temperature range and exhibits a plateau around 70 K. Such increase of T -is not expected for paramagnetic Yb 3+ spins but is rather due to crystal electric field effects, where spin fluctuations ν slow down with decreasing temperature and cause increased NMR relaxation in the fast fluctuation regime, where 1/T 1 ∝ 1/ν [63]. Below 70 K, T -remains constant and field-independent down to 10 K, which suggests that the relaxation is dominated by paramagnetic fluctuations of Yb 3+ spins. At low T, i.e., below ∼ 10 K depending on the field, a dramatic field dependence of T -develops with a decrease of the T -value larger than two orders of magnitude in 4.8 T compared to that in 1.24 T at 1.6 K. T -1 1 decreases exponentially in the temperature range 0.2 K ≤ T ≤ 10 K, suggesting a gapped excitation spectrum. It is also observed that, T -1 1 drops faster in higher magnetic fields which again suggests a field-driven gap as the specific heat data does. In Fig. 4 (d), we present T -as a function of inverse temperature (T -1 ) in a semi-log plot where the phenomenological model relevant for thermally activated behavior i.e., T -1 1

V. ACKNOWLEDGMENTS

We acknowledge stimulating discussions with P. Mendels. PK acknowledges the funding by the Science and Engineering Research Board, and Department of Science and Technology, India through Research Grants. This research was supported by the U.S. Department of Energy, Office of Basic Energy Sciences, Division of Materials Sciences and Engineering. Ames Laboratory is operated for the U.S. Department of Energy by Iowa State University under Contract No. DE-AC02-07CH11358. EK and SB acknowledges the France Canada Research Fund for financial support. AZ acknowledges the financial support of the Slovenian Research agency under program No. P1-0125 and projects No. J1-2461 and No. N1-0148. AMS thanks the URC/FRC of UJ and the SA-NRF for financial support.


Byungjae Hwang

Rafael Piestun

Kristina Irsch
email: kristina.irsch@cnrs.fr

Non-Isoplanatic PSF and Image Estimation Using Speckle Illumination

We propose a speckle-illumination statistical method to recover the point-spread function (PSF) and high-resolution fluorescence images in the presence of aberrations, without any calibration or isoplanatism assumptions. The accurate PSF estimation enables its use in deconvolution for high-resolution 3D imaging.

Introduction

Speckle illumination provides a convenient and effective solution for structured-illumination imaging, enabling resolution enhancement [START_REF] Mudry | Structured illumination microscopy using unknown speckle patterns[END_REF], optical sectioning [START_REF] Ventalon | Quasi-confocal fluorescence sectioning with dynamic speckle illumination[END_REF], and PSF estimation [START_REF] Meitav | Point spread function estimation from projected speckle illumination[END_REF]. One key benefit of structured illumination is the possibility to enhance resolution by a factor x2 using linear methods. Unfortunately, deterministic patterned illumination, such as sinusoidal patterns, falter in the presence of aberrations. Interestingly, under easy-tosatisfy assumptions, speckle statistics are not affected by aberrations and hence random speckle patterns are attractive for structured illumination with aberration caused by the optics, the medium, or the sample [START_REF] Premillieu | Blind speckle illumination for aberration correction[END_REF]. The reconstruction and PSF estimation can be accomplished from a speckle-illuminated large field-of-view image under the assumption that the image is obtained from an isoplanatic imaging system [START_REF] Mudry | Structured illumination microscopy using unknown speckle patterns[END_REF][START_REF] Ventalon | Quasi-confocal fluorescence sectioning with dynamic speckle illumination[END_REF][START_REF] Meitav | Point spread function estimation from projected speckle illumination[END_REF]. Isoplanatism is thus a common assumption that limits applicability and performance.

Here, we propose a method for fluorescence image acquisition and reconstruction, in the presence of aberrations, using multiple image frames acquired by illuminating a fluorescent sample with randomly varying speckle patterns. From the acquired images, multiple sub-images are extracted to estimate the local PSF, and the variance of the images are calculated to recover high-resolution images. Finally, a deconvolution process using the calculated image and the estimated PSF provides imaging with twice the resolution of the equivalent wide-field system. Multiple sub-images are extracted from the series of images in the region of interest. The Fourier magnitude of the PSF is estimated using power spectrum averaging (top). The Fourier phase is estimated via coherent averaging using the cross-correlation (bottom). The cross-correlation is calculated iteratively, updating the image resulting from the combination of the estimated Fourier magnitude and phase. PSF estimation -As illustrated in Figure 1, the acquired speckle-illuminated image frames at the region of interest (ROI) are split into multiple sub-images so that they are uncorrelated. Thus, coherent averaging of the sub-images can be used to estimate the Fourier phase of the PSF [START_REF] Hwang | Imaging through random media using coherent averaging[END_REF]. To estimate the Fourier magnitude of the PSF, we perform power-spectrum averaging of the sub-images. The Fourier phase of the PSF is extracted from the Fourier phase that results from averaging the shifted sub-images based on the cross-correlation. The PSF within the ROI is retrieved by iteratively recombining the Fourier phase and the Fourier magnitude.

Method

High-resolution image recovery -Calculating the variance of the images enables coherent averaging of the randomly scattered Fourier-transformed objects at the center of the k-space. From the Fourier perspective, the Fourier-transformed images contain the low-resolution information limited by the (local) optical transfer function (OTF) at the center and the high-resolution information beyond the OTF outside the center. The low-resolution information can be easily removed by subtracting the mean of the acquired images. The high-resolution information beyond the OTF is randomly scattered and superposed in the k-space. By calculating the mean square of the remainders, the high-frequency image is reconstructed beyond the OTF.

Figure 2 illustrates the method through a simulation of fluorescence imaging.

Conclusion

From the randomly generated speckle-illumination microscopy, the imaging PSF and a high-resolution image are reconstructed using simple statistical calculations without assuming isoplanatism or performing calibration. The mean of the aligned sub-images provides the imaging PSF, and the variance of the acquired images directly yields a high-resolution image. The estimated PSF and the variance can be used in a deconvolution algorithm to obtain a high-resolution image without the aberration effects of the detection path.

Fig. 1 .

 1 Fig. 1. Flow chart of the non-isoplanatic PSF estimation. Image frames are acquired using a series of speckle-illumination patterns (left).Multiple sub-images are extracted from the series of images in the region of interest. The Fourier magnitude of the PSF is estimated using power spectrum averaging (top). The Fourier phase is estimated via coherent averaging using the cross-correlation (bottom). The cross-correlation is calculated iteratively, updating the image resulting from the combination of the estimated Fourier magnitude and phase.

  (3D, COSI, DH, FLatOptics, IS, pcAOP) © Optica Publishing Group 2023

Figure 2 (

 2 Figure 2 illustrates the method through a simulation of fluorescence imaging. Figure 2(a) shows the actual aberrated PSF, while 2(b) shows the estimation, exhibiting excellent agreement. Figures 2(c) and 2(d) show respectively the actual and estimated power spectrum. Figure 2(e) shows the aberrated wide-field image and 2(f) shows the reconstructed image after deconvolution with the accurate PSF estimation. The deconvolution is performed using the estimated PSF and the variance of the speckle-illuminated image frames to reconstruct a highresolution image without the effects of the aberrations. In this example, the aberrations are a linear combination of equally-weighted Zernike modes 3,4,5,7,8,12,13 and the image frames have additive Gaussian noise (SNR = 4.6).

Fig. 2 .

 2 Fig. 2. PSF estimation and image reconstruction simulation example: (a) the aberrated PSF as the input, (b) the estimated PSF, (c) the power spectrum of the input, (d) the estimated power spectrum, (e) the aberrated wide-field image, (f) the reconstructed image by applying the estimated PSF to the variance (deconvolution).

  (3D, COSI, DH, FLatOptics, IS, pcAOP) © Optica Publishing Group 2023