Lambda-Free Logical Frameworks

A Tutorial Introduction to the Lambda Calculus

This paper is a concise and painless introduction to the $λ$-calculus. This formalism was developed by Alonzo Church as a tool for studying the mathematical properties of effectively computable functions. The formalism became popular and has provided a strong theoretical foundation for the family of functional programming languages. This tutorial shows how to perform arithmetical and logical computations using the $λ$-calculus and how to define recursive functions, even though $λ$-calculus functions are unnamed and thus cannot refer explicitly to themselves.

Short proofs of strong normalization

This paper presents simple, syntactic strong normalization proofs for the simply-typed lambda-calculus and the polymorphic lambda-calculus (system F) with the full set of logical connectives, and all the permutative reductions. The normalization proofs use translations of terms and types to systems, for which strong normalization property is known.

λ-项的正则语言：语法与语义定义通过逻辑关系等价

Syntactically and semantically regular languages of lambda-terms coincide through logical relations

本文证明简单类型λ-项的正则语言在语法（扩展Hillebrand-Kanellakis）与语义（有限外延模型）定义下等价，通过逻辑关系和胶合构造提供统一证明。

Translating HOL to Dedukti

Dedukti is a logical framework based on the lambda-Pi-calculus modulo rewriting, which extends the lambda-Pi-calculus with rewrite rules. In this paper, we show how to translate the proofs of a family of HOL proof assistants to Dedukti. The translation preserves binding, typing, and reduction. We implemented this translation in an automated tool and used it to successfully translate the OpenTheory standard library.

A Symmetric Lambda-Calculus Corresponding to the Negation-Free Bilateral Natural Deduction

Filinski constructed a symmetric lambda-calculus consisting of expressions and continuations which are symmetric, and functions which have duality. In his calculus, functions can be encoded to expressions and continuations using primitive operators. That is, the duality of functions is not derived in the calculus but adopted as a principle of the calculus. In this paper, we propose a simple symmetric lambda-calculus corresponding to the negation-free natural deduction based bilateralism in proof-theoretic semantics. In our calculus, continuation types are represented as not negations of formul…

On counting untyped lambda terms

We present several results on counting untyped lambda terms, i.e., on telling how many terms belong to such or such class, according to the size of the terms and/or to the number of free variables.

类型理论的模块化构造

A modular construction of type theories

本文提出理论U，一个模块化类型理论构造，使得多个逻辑系统的证明可表达，并证明子理论符号使用对应子理论证明。

无λ高阶逻辑的超位置演算

Superposition for Lambda-Free Higher-Order Logic

本文为无λ高阶逻辑提出反驳完备的超位置演算，支持部分应用，通过非完全单调项序实现，在Zipperposition中实现并评估，有望推动全高阶逻辑自动定理证明器的发展。

Logical Obstruction to Set Agreement Tasks for Superset-Closed Adversaries

In their recent paper (GandALF 2018), Goubault, Ledent, and Rajsbaum provided a formal epistemic model for distributed computing. Their logical model, as an alternative to the well-studied topological model, provides an attractive framework for refuting the solvability of a given distributed task by means of logical obstruction: One just needs to devise a formula, in the formal language of epistemic logic, that describes a discrepancy between the model of computation and that of the task. However, few instances of logical obstruction were presented in their paper and specifically logical obstr…

Counting isomorphism classes of $β$-normal linear lambda terms

Unanticipated connections between different fragments of lambda calculus and different families of embedded graphs (a.k.a. "maps") motivate the problem of enumerating $β$-normal linear lambda terms. In this brief note, it is shown (by appeal to a theorem of Arquès and Beraud) that the sequence counting isomorphism classes of $β$-normal linear lambda terms up to free exchange of adjacent lambda abstractions coincides with the sequence counting isomorphism classes of rooted maps on oriented surfaces (A000698).

The Complexity of Limited Belief Reasoning -- The Quantifier-Free Case

The classical view of epistemic logic is that an agent knows all the logical consequences of their knowledge base. This assumption of logical omniscience is often unrealistic and makes reasoning computationally intractable. One approach to avoid logical omniscience is to limit reasoning to a certain belief level, which intuitively measures the reasoning "depth." This paper investigates the computational complexity of reasoning with belief levels. First we show that while reasoning remains tractable if the level is constant, the complexity jumps to PSPACE-complete -- that is, beyond classical r…

Bridging the Gap between Reinforcement Learning and Knowledge Representation: A Logical Off- and On-Policy Framework

Knowledge Representation is important issue in reinforcement learning. In this paper, we bridge the gap between reinforcement learning and knowledge representation, by providing a rich knowledge representation framework, based on normal logic programs with answer set semantics, that is capable of solving model-free reinforcement learning problems for more complex do-mains and exploits the domain-specific knowledge. We prove the correctness of our approach. We show that the complexity of finding an offline and online policy for a model-free reinforcement learning problem in our approach is NP-c…

Logic for Unambiguous Context-Free Languages

We give in this paper a logical characterization for unambiguous Context Free Languages, in the vein of descriptive complexity. A fragment of the logic characterizing context free languages given by Lautemann, Schwentick and Thérien [18] based on implicit definability is used for this aim. We obtain a new connection between two undecidable problems, a logical one and a language theoretical one.