اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدAn Inversion Tool for Conditional Term Rewriting Systems -- A Case Study of Ackermann Inversion
92
0
0.0
(
0
)
تأليف
Maria Bendix Mikkelsen
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
We report on an inversion tool for a class of oriented conditional constructor term rewriting systems. Four well-behaved rule inverters ranging from trivial to full, partial and semi-inverters are included. Conditional term rewriting systems are theoretically well founded and can model functional and non-functional rewrite relations. We illustrate the inversion by experiments with full and partial
قيم البحث
اقرأ أيضاً
In this paper, we reconsider the unfolding-based technique that we have introduced previously for detecting loops in standard term rewriting. We improve it by guiding the unfolding process, using distinguished positions in the rewrite rules. This res
ults in a depth-first computation of the unfoldings, whereas the original technique was breadth-first. We have implemented this new approach in our tool NTI and compared it to the previous one on a bunch of rewrite systems. The results we get are promising (better times, more successful proofs).
Most of the seismic inversion techniques currently proposed focus on robustness with respect to the background model choice or inaccurate physical modeling assumptions, but are not apt to large-scale 3D applications. On the other hand, methods that a
re computationally feasible for industrial problems, such as full waveform inversion, are notoriously bogged down by local minima and require adequate starting models. We propose a novel solution that is both scalable and less sensitive to starting model or inaccurate physics when compared to full waveform inversion. The method is based on a dual (Lagrangian) reformulation of the classical wavefield reconstruction inversion, whose robustness with respect to local minima is well documented in the literature. However, it is not suited to 3D, as it leverages expensive frequency-domain solvers for the wave equation. The proposed reformulation allows the deployment of state-of-the-art time-domain finite-difference methods, and is computationally mature for industrial scale problems.
Topological crystalline superconductors have attracted rapidly rising attention due to the possibility of higher-order phases, which support Majorana modes on boundaries in $d-2$ or lower dimensions. However, although the classification and bulk topo
logical invariants in such systems have been well studied, it is generally difficult to faithfully predict the boundary Majoranas from the band-structure information due to the lack of well-established bulk-boundary correspondence. Here we propose a protocol for deriving symmetry indicators that depend on a minimal set of necessary symmetry data of the bulk bands and can diagnose boundary features. Specifically, to obtain indicators manifesting clear bulk-boundary correspondence, we combine the topological crystal classification scheme in the real space and a twisted equivariant K group analysis in the momentum space. The key step is to disentangle the generally mixed strong and weak indicators through a systematic basis-matching procedure between our real-space and momentum-space approaches. We demonstrate our protocol using an example of two-dimensional time-reversal odd-parity superconductors, where the inversion symmetry is known to protect a higher-order phase with corner Majoranas. Symmetry indicators derived from our protocol can be readily applied to ab initio database and could fuel material predictions for strong and weak topological crystalline superconductors with various boundary features.
Curated databases have become important sources of information across scientific disciplines, and due to the manual work of experts, often become important reference works. Features such as provenance tracking, archiving, and data citation are widely
regarded as important features for curated databases, but implementing such features is challenging, and small database projects often lack the resources to do so. A scientific database application is not just the database itself, but also an ecosystem of web applications to display the data, and applications supporting data curation. Supporting advanced curation features requires changing all of these components, and there is currently no way to provide such capabilities in a reusable way. Cross-tier programming languages have been proposed to simplify the creation of web applications, where developers write an application in a single, uniform language. Consequently, database queries and updates can be written in the same language as the rest of the program, and at least in principle, it should be possible to provide curation features reusably via program transformations. As a first step, it is important to establish that realistic curated databases can be implemented in a cross-tier programming language. In this paper, we describe such a case study: reimplementing the web frontend of a real-world scientific database, the IUPHAR/BPS Guide to Pharmacology (GtoPdb), in the Links programming language. We show how features such as language-integrated query simplify the development process, and rule out common errors. We show that the Links implementation performs fewer database queries, while the time needed to handle the queries is comparable to the Java version. While there is some overhead to using Links because of its comparative immaturity compared to Java, the Links version is viable as a proof-of-concept case study.
Abstract. We present a tool to automatically perform the data-size analysis of imperative programs written in C. This tool, called pymwp, is inspired by a classical work on complexity analysis [10], and allows to certify that the size of the values c
omputed by a program will be bounded by a polynomial in the programs inputs. Strategies to provide meaningful feedback on non-polynomial programs and to ``tame the non-determinism of the original analysis were implemented following recent progresses [3], but required particular care to accommodate the growing complexity of the analysis. The Python source code is intensively documented, and our numerous example files encompass the original examples as well as multiple test cases. A pip package should make it easy to install pymwp on any plat-form, but an on-line demo is also available for convenience.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
