A Logical Framework with Higher-Order Rational Circular Terms Zhibo Chen and Frank Pfenning

2025-04-24 0 0 657.22KB 40 页 10玖币

侵权投诉

A Logical Framework with

Higher-Order Rational (Circular) Terms

Zhibo Chen and Frank Pfenning

zhiboc@andrew.cmu.edu fp@cs.cmu.edu

Carnegie Mellon University, Pittsburgh, PA, USA

Abstract. Logical frameworks provide natural and direct ways of speci-

fying and reasoning within deductive systems. The logical framework LF

and subsequent developments focus on ﬁnitary proof systems, making the

formalization of circular proof systems in such logical frameworks a cum-

bersome and awkward task. To address this issue, we propose CoLF, a

conservative extension of LF with higher-order rational terms and mixed

inductive and coinductive deﬁnitions. In this framework, two terms are

equal if they unfold to the same inﬁnite regular Böhm tree. Both term

equality and type checking are decidable in CoLF. We illustrate the el-

egance and expressive power of the framework with several small case

studies.

Keywords: Logical Frameworks, Circular Proofs, Regular Böhm Trees

1 Introduction

A logical framework provides a uniform way of formalizing and mechanically

checking derivations for a variety of deductive systems common in the deﬁnitions

of logics and programming languages. In this paper we propose a conservative

extension of the logical framework LF [18] to support direct representations of

rational (circular) terms and deductions.

The main methodology of a logical framework is to establish a bijective cor-

respondence between derivations of a judgment in the object logic and canonical

terms of a type in the framework. In this way, proof checking in the object logic

is reduced to type checking in the framework. One notable feature of LF is the

use of abstract binding trees, where substitution in the object logic can be en-

coded as substitution in the framework, leading to elegant encodings. On the

other hand, encodings of rational terms, circular derivations, and their equality

relations are rather cumbersome. We therefore propose the logical framework

CoLF as a conservative extension of LF in which both circular syntactic objects

and derivations in an object logic can be elegantly represented as higher-order

rational dependently typed terms. This makes CoLF a uniform framework for

formalizing proof systems on cyclic structures. We prove the decidability of type

checking and soundness of equality checking of higher-order rational terms.

arXiv:2210.06663v3 [cs.LO] 10 May 2023

While CoLF allows formalization of circular derivations, proofs by coinduc-

tion about such circular encodings can only be represented as relations in CoLF,

mirroring a similar limitation of LF regarding induction. In future work, we plan

to extend CoLF to support checking of meta-theoretic properties of encodings

analogous to the way Twelf [27] can check properties of encodings in LF.

The main contributions of this paper are:

–The type theory of a logical framework with higher-order rational terms.

The theory allows natural and adequate representations of circular objects

and circular derivations (Section 3).

–A decidable trace condition for ensuring the validity of circular terms and

derivations arising from mixed inductive and coinductive deﬁnitions (Sec-

tion 3.3).

–A sound and complete algorithm to decide the equality of two higher-order

rational terms (Section 3.5).

–A proof of decidability of type-checking in the framework (Section 3.7).

–Case studies of encoding subtyping derivations of recursive types (Section 4).

We have implemented CoLF in OCaml and the implementation can be ac-

cessed at https://www.andrew.cmu.edu/user/zhiboc/colf.html. An addi-

tional case study of the meta-encoding the term model of CoLF in CoLF is

presented in Appendix J.

2 Mixed Inductive and Coinductive Deﬁnitions

We motivate our design through simple examples of natural numbers, conatural

numbers, and ﬁnitely padded streams. The examples serve to illustrate the idea of

coinductive interpretations, and they do not involve dependent types or higher-

order terms. More complex examples will be introduced later in the case studies

(Section 4).

Natural Numbers. The set of natural numbers is inductively generated by

zero and successor. In a logical framework such as LF, one would encode natural

numbers as the signature consisting of the ﬁrst three lines in the top left part of

Fig. 1.

The type theory ensures that canonical terms of the type nat are in one-to-

one correspondence with the natural numbers. Speciﬁcally the inﬁnite stack of

successors succ (succ (succ . . . )) is not a valid term of type nat. Therefore, the

circular term w1 is not a valid term.

Conatural Numbers. We may naturally specify that a type admits a coin-

ductive interpretation by introducing a new syntactic kind cotype. The kind

cotype behaves just like the kind type except that now the terms under cotype

are allowed to be circular. A slightly adapted signature would encode the set

nat : type.

zero : nat.

succ : nat -> nat.

w1 : nat = succ w1. (not valid)

conat : cotype.

cozero : conat.

cosucc : conat -> conat.

w2 : conat = cosucc w2.

w3 : conat = cosucc (cosucc w3).

eq : conat -> conat -> type.

eq/refl : eq N N.

eqw2w3 : eq w2 w3 = eq/refl.

padding : type.

pstream : cotype.

cocons : nat -> padding -> pstream.

pad : padding -> padding.

next : pstream -> padding.

s1 : pstream = cocons (succ zero)

(pad (pad (next s1))).

p2 : padding = pad p2. (not valid)

s3 : pstream = cocons zero (next s3).

s4 : pstream = cocons zero p5.

p5 : padding = next s4.

p6 : padding = pad p7. (not valid)

p7 : padding = pad p6. (not valid)

Fig. 1. Signatures and Examples for Section 2

of conatural numbers, shown as the ﬁrst three lines in the bottom left part of

Fig. 1.

Because conat is a coinductive type, the canonical forms of type conat in-

cludes cosuccncozero for all nand the inﬁnite stack of cosucc, which is in

one to one correspondence with the set of conatural numbers. Speciﬁcally, the

inﬁnite stack of cosucc, may be represented by the valid circular term w2 as

in Fig. 1. The equality of terms in CoLF is the equality of the inﬁnite trees

generated by unfolding the terms, which corresponds to a bisimulation between

circular terms. For example, an alternative representation of the inﬁnite stack of

cosucc is the term w3, and CoLF will treat w2 and w3 as equal terms, as shown

by the last three lines in the bottom left part of Fig. 1. The terms w2 and w3 are

proved equal by reﬂexivity. On the other hand, a formulation of conats in LF

would involve an explicit constructor, e.g. mu : (conat -> conat) -> conat.

The encoding of equality is now complicated and one needs to work with an

explicit equality judgment whenever a conat is used. Functions deﬁned by coin-

duction (e.g., bisimulation in Appendix K) need to be encoded as relations in

CoLF.

2.1 Finitely Padded Rational Streams

As an example of mixed inductive and coinductive deﬁnition, we consider rational

streams of natural numbers with ﬁnite paddings in between. These streams are

special instances of left-fair streams [5]. We deﬁne streams coinductively and

deﬁne paddings inductively, such that there are inﬁnitely many numbers in the

stream but only ﬁnitely many paddings between numbers, shown in the signature

consisting of ﬁrst ﬁve lines in the right column of Fig. 1. For example, the term

s1 in Fig. 1represents a stream of natural number 1’s with two paddings in

between. Because padding is a type, the term p2 is not valid, as it is essentially

an inﬁnite stack of pad constructors. Deﬁnitions in a CoLF signature can refer

to each other. Thus, the terms s3 and s4 denote the same padded stream, and

the terms p6,p7 and p2 denote the same invalid stream consisting of purely

paddings.

Priorities. To ensure the adequacy of representation, types of kind cotype admit

circular terms while types of kind type admit only ﬁnitary terms. It is obvious

that the circular term w1 is not a valid term of type nat due to the presence of an

inﬁnite stack of inductive constructors, and the circular term w2 is a valid term of

type conat because it is a stack of coinductive constructors. However, when we

have both inductive and coinductive types, it is unclear whether a circular term

(e.g. s1) is valid. Historically, priorities are used to resolve this ambiguity [11].

A priority is assigned to each inductive or coinductive type, and constructors

inherit priorities from their types. Constructors with the highest priority types

are then viewed as primary. In CoLF, priorities are determined by the order of

their declarations. Type families declared later have higher priorities than those

declared earlier. In this way, the type pstream has higher priority than the type

padding. Constructor cocons inherits the priority of pstream, and the term

s1 is viewed as an inﬁnite stack of cocons and is thus valid. Similarly, terms

s3 and s4 are also valid. If we switch the order of declaration of padding and

pstream (thereby switching their priorities), then terms s1,s3, and s4 are no

longer valid.

3 The Type Theory

We formulate the type theory of CoLF, a dependent type theory with higher-

order rational terms and decidable type checking. The higher-order rational

terms correspond to ⊥-free regular Böhm trees [21] and have decidable equality.

3.1 Higher-Order Rational Terms

When we consider ﬁrst order terms (terms without λ-binders), the rational terms

are terms with only ﬁnitely many distinct subterms, and thus their equality is

decidable. We translate this intuition to the higher-order setting. The higher-

order rational terms are those with ﬁnitely many subterms up to renaming of

free and bound variables. We give several examples of rational and non-rational

terms using the signatures in Section 2.

1. The term w2 in Fig. 1is a ﬁrst-order rational term.

2. A stream counting up from zero up0=cocons zero (next (cocons (succ zero)

(next (. . . )))) is a ﬁrst-order term that is not rational.

3. A stream that repeats its argument R2=λx. cocons x(next (R2x)) is a

higher-order rational term.

4. A stream that counts up from a given number up =λx. cocons x(next (up

(succ x))) is not a rational higher-order term.

In the deﬁnitions above, bolded symbols on the left of the equality signs

are called recursion constants. It is crucial that in higher-order rational terms,

all arguments to recursion constants are bound variables and not other kinds

of terms. We call this restriction the prepattern restriction as it is similar to

Miller’s pattern restriction [24] except that we allow repetition of arguments. The

prepattern restriction marks the key diﬀerence between the higher-order rational

term R2and the inﬁnitary term up. The term up is not rational because the

argument to up is succ x, which is not a bound variable.

3.2 Syntax

We build subsequent developments on canonical LF [19], a formulation of the

LF type theory where terms are always in their canonical form. Canonical forms

do not contain β-redexes and are fully η-expanded with respect to their typ-

ing, supporting bijective correspondences between object logic derivations and

the terms of the framework. One drawback of this presentation is that canon-

ical terms are not closed under syntactic substitutions, and the technique of

hereditary substitution addresses this problem [29].

The syntax of the theory follows the grammar shown in Fig. 2. We use the

standard notion of spines. For example, a term x M1M2M3will be written as

x·(M1;M2;M3)where xis the head and M1;M2;M3is the spine. To express

rational terms, we add recursive deﬁnitions of the form r:A=Mto the sig-

nature, where Mmust be contractive (judgment Mcontra) in that the head of

Mmust be a constant or a variable. Recursive deﬁnitions look like notational

deﬁnitions [26], but their semantics are very diﬀerent. Recursive deﬁnitions are

interpreted recursively in that the deﬁnition Mmay mention the recursion con-

stant r, and other recursion constants including those deﬁned later in the sig-

nature, while notational deﬁnitions in LF [26] cannot be recursive. Recursion

constants are treated specially as a syntactic entity that is diﬀerent from vari-

ables or constructors (nonrecursive constants). To ensure the conservativity over

LF, we further require all deﬁnitions in Σto be linearly ordered. That is, only

in the body of a recursive deﬁnition can we “forward reference”, and we can only

forward reference other recursion constants. All other declarations must strictly

refer to names that have been deﬁned previously. We write λx and Mto mean a

sequence of λ-abstractions and a sequence of terms respectively. We write x, y, z

for variables, c, d for term constants (also called constructors), afor type family

constants, and r, r0, r00 for recursion constants.

To enforce the prepattern restriction, we use a technical device called prepat-

tern Π-abstractions, and associated notion of prepattern variables and prepattern

spines. Prepattern Π-abstractions are written as Πx ˆ: A2. A1, and xwill be a

prepattern variable (written xˆ: A2) in A1. Moreover, in A1, if yis a variable

of a prepattern type Πw ˆ: A2.B, then the prepattern application of yto xwill

be realized as the head yfollowed by a prepattern spine ([x]), written y·([x]).

The semantics is that prepattern variables may only be substituted by other

prepattern variables, while ordinary variables can be substituted by arbitrary

terms (which include other prepattern variables). In a well-typed signature, if

文档加载中……请稍候！
如果长时间未打开，您也可以点击刷新试试。

下载文档到电脑，查找使用更方便

10 玖币 0人已下载

立即下载

摘要：

ALogicalFrameworkwithHigher-OrderRational(Circular)TermsZhiboChenandFrankPfenningzhiboc@andrew.cmu.edufp@cs.cmu.eduCarnegieMellonUniversity,Pittsburgh,PA,USAAbstract.Logicalframeworksprovidenaturalanddirectwaysofspeci-fyingandreasoningwithindeductivesystems.ThelogicalframeworkLFandsubsequentdevelopm...

展开>> 收起<<

A Logical Framework with Higher-Order Rational Circular Terms Zhibo Chen and Frank Pfenning.pdf

共40页,预览5页

还剩页未读，继续阅读

声明：本站为文档C2C交易模式，即用户上传的文档直接被用户下载，本站只是中间服务平台，本站所有文档下载所得的收益归上传人(含作者)所有。玖贝云文库仅提供信息存储空间，仅对用户上传内容的表现方式做保护处理，对上载内容本身不做任何修改或编辑。若文档所含内容侵犯了您的版权或隐私，请立即通知玖贝云文库，我们立即给予删除！

A Logical Framework with Higher-Order Rational Circular Terms Zhibo Chen and Frank Pfenning

相关推荐

开通VIP享超值会员特权

作者详情

相关内容

热门标签

举报选择: