Comparing the expressiveness of transducers and simply-typed linear lambda-calculi

比较不同计算模型和形式的可表达性是理论计算机科学许多领域的一个重要主题，包括复杂性理论、描述复杂性理论和自动机理论。这个项目的主要目的是使用来自自动机理论和线性逻辑语义的技术，在由自动机、λ -演算和逻辑解释自然定义的函数类之间进行这种比较。1996年，lambda演算和自动机之间的惊人联系被发现：使用Church编码的简单类型函数（从字符串到布尔值）可以准确地识别常规语言的类别。然后，线性逻辑和自动机的专家对这种联系进行了改进和进一步利用，以解决与高阶模型检查和自动机在无限数据上运行相关的问题。在此之后，近年来有人系统地比较了Church编码在线性lambda- calculus和string-to-string转导中的表达能力，揭示了一些非平凡的联系，包括正则转导的表征。这些技术包括语义评估、lambda演算中的范式分析和非平凡自动机理论结果的混合。为了对所采用的目标和方法有所了解，人们可以浏览以下内容：-概述计划的摘要：https://cs-web.swan.ac.uk/~cpradic/smp-abstract.pdf-关于该主题的博士论文：https://nguyentito.eu/thesis.pdf该项目将是该努力的延续。有许多具体的问题需要解决，这些问题可以作为在这种情况下工作的一个很好的介绍，包括：-比较非交换线性λ -演算和一阶换能器的表达性-设计极简类型的编程语言，以捕获在线性λ -演算中可以实现的东西与Church编码在Bojanczyk关于多正则函数的工作的精神，但对于无比较的多正则函数——使用共归纳数据类型的Church编码对无限结构和函数lambda可定义的换能器进行类似的比较——检查如果我们允许经典线性逻辑的全部力量而不是直觉主义的片段，是否在表达性上存在差异。这可以通过在同一领域的更具有挑战性的问题或特定于某个领域的更广泛的关注进行后续研究涉及（例如涉及定义行为良好的树转导类的研究或线性逻辑中更专业的主题，如弱指数或线性类型的量化）。虽然有数学逻辑或理论计算机科学的背景是必要的，但一个成功的申请人当然不会被期望在开始之前熟悉上面提到的所有工具。

Comparing the expressiveness of different computation models and formalisms is an important theme in many fields of theoretical computer science including complexity theory, descriptive complexity and automata theory. The main aims of this project would be to carry out such comparisons across classes of functions naturally defined by automata, lambda-calculi and logical interpretations, using techniques coming from automata theory and the semantics of linear logic.In 1996, a striking connection between lambda-calculus and automata was uncovered: the simply-typed functions from strings to booleans using Church encodings recognize exactly the class of regular languages. This sort of connection was then refined and further exploited by specialists of linear logic and automata to tackle problems related to higher-order model checking and automata running over infinite data.Following this, there was an effort in recent years to systematically compare the expressive power of Church encodings in linear lambda-calculi and string-to-string transductions, unveiling some non-trivial connections including a characterization of regular transductions. The techniques involve a mix of semantic evaluation, analyses of the normal forms in the lambda-calculus and non-trivial automata-theoretic results. To get a flavor of both the aims and the methods employed, one may skim through the following:- abstract outlining the programme: https://cs-web.swan.ac.uk/~cpradic/smp-abstract.pdf- PhD thesis on that topic: https://nguyentito.eu/thesis.pdf This project would be a continuation of that effort. There are a number of concrete problems to tackle that can serve as a good introduction to working in that setting, including:- comparing the expressiveness of the non-commutative linear lambda-calculus and first-order transducers- designing minimalistic typed programming languages capturing what is achievable in the linear lambda-calculus with Church encodings in the spirit of Bojanczyk's work on polyregular functions, but for comparison-free polyregular functions- carrying out a similar comparison for transducers over infinite structures and functions lambda-definable using the Church encoding of coinductive datatypes- checking whether there is difference in expressiveness if we allow the full power of classical linear logic instead of the intuitionistic fragmentThis could be followed-up by investigations in more challenging problems in the same area or into broader concerns specific to one of the domains involved (such as investigations which involving defining well behaved-class of tree transductions or more specialized topics in linear logic such as weak exponentials or quantification over linear types).While having a background in either mathematical logic or theoretical computer science would be necessary, a successful applicant would certainly not be expected to be familiar with all the tools mentioned above before starting.