Kliknij ten link, aby zobaczyć inne rodzaje publikacji na ten temat: Algebraic datatypes.
Artykuły w czasopismach na temat „Algebraic datatypes”
Utwórz poprawne odniesienie w stylach APA, MLA, Chicago, Harvard i wielu innych
Sprawdź 30 najlepszych artykułów w czasopismach naukowych na temat „Algebraic datatypes”.
Przycisk „Dodaj do bibliografii” jest dostępny obok każdej pracy w bibliografii. Użyj go – a my automatycznie utworzymy odniesienie bibliograficzne do wybranej pracy w stylu cytowania, którego potrzebujesz: APA, MLA, Harvard, Chicago, Vancouver itp.
Możesz również pobrać pełny tekst publikacji naukowej w formacie „.pdf” i przeczytać adnotację do pracy online, jeśli odpowiednie parametry są dostępne w metadanych.
Przeglądaj artykuły w czasopismach z różnych dziedzin i twórz odpowiednie bibliografie.
1
Martinez Lopez, P. "Fork algebraic datatypes". Logic Journal of IGPL 6, nr 4 (1.07.1998): 531–43. http://dx.doi.org/10.1093/jigpal/6.4.531.
Pełny tekst źródła
2
Malewski, Stefan, Michael Greenberg i Éric Tanter. "Gradually structured data". Proceedings of the ACM on Programming Languages 5, OOPSLA (20.10.2021): 1–29. http://dx.doi.org/10.1145/3485503.
Pełny tekst źródłaStreszczenie:
Dynamically-typed languages offer easy interaction with ad hoc data such as JSON and S-expressions; statically-typed languages offer powerful tools for working with structured data, notably algebraic datatypes , which are a core feature of typed languages both functional and otherwise. Gradual typing aims to reconcile dynamic and static typing smoothly. The gradual typing literature has extensively focused on the computational aspect of types, such as type safety, effects, noninterference, or parametricity, but the application of graduality to data structuring mechanisms has been much less explored. While row polymorphism and set-theoretic types have been studied in the context of gradual typing, algebraic datatypes in particular have not, which is surprising considering their wide use in practice. We develop, formalize, and prototype a novel approach to gradually structured data with algebraic datatypes. Gradually structured data bridges the gap between traditional algebraic datatypes and flexible data management mechanisms such as tagged data in dynamic languages, or polymorphic variants in OCaml. We illustrate the key ideas of gradual algebraic datatypes through the evolution of a small server application from dynamic to progressively more static checking, formalize a core functional language with gradually structured data, and establish its metatheory, including the gradual guarantees.
3
Kuncak, Viktor, i Daniel Jackson. "Relational analysis of algebraic datatypes". ACM SIGSOFT Software Engineering Notes 30, nr 5 (wrzesień 2005): 207–16. http://dx.doi.org/10.1145/1095430.1081740.
Pełny tekst źródła
4
Zenger, Matthias, i Martin Odersky. "Extensible algebraic datatypes with defaults". ACM SIGPLAN Notices 36, nr 10 (październik 2001): 241–52. http://dx.doi.org/10.1145/507669.507665.
Pełny tekst źródła
5
Dinesh, T. B., Magne Haveraaen i Jan Heering. "An Algebraic Programming Style for Numerical Software and Its Optimization". Scientific Programming 8, nr 4 (2000): 247–59. http://dx.doi.org/10.1155/2000/494281.
Pełny tekst źródłaStreszczenie:
The abstract mathematical theory of partial differential equations (PDEs) is formulated in terms of manifolds, scalar fields, tensors, and the like, but these algebraic structures are hardly recognizable in actual PDE solvers. The general aim of the Sophus programming style is to bridge the gap between theory and practice in the domain of PDE solvers. Its main ingredients are a library of abstract datatypes corresponding to the algebraic structures used in the mathematical theory and an algebraic expression style similar to the expression style used in the mathematical theory. Because of its emphasis on abstract datatypes, Sophus is most naturally combined with object-oriented languages or other languages supporting abstract datatypes. The resulting source code patterns are beyond the scope of current compiler optimizations, but are sufficiently specific for a dedicated source-to-source optimizer. The limited, domain-specific, character of Sophus is the key to success here. This kind of optimization has been tested on computationally intensive Sophus style code with promising results. The general approach may be useful for other styles and in other application domains as well.
6
Mordido, Andreia, Janek Spaderna, Peter Thiemann i Vasco T. Vasconcelos. "Parameterized Algebraic Protocols". Proceedings of the ACM on Programming Languages 7, PLDI (6.06.2023): 1389–413. http://dx.doi.org/10.1145/3591277.
Pełny tekst źródłaStreszczenie:
We propose algebraic protocols that enable the definition of protocol templates and session types analogous to the definition of domain-specific types with algebraic datatypes. Parameterized algebraic protocols subsume all regular as well as most context-free and nested session types and, at the same time, replace the expensive superlinear algorithms for type checking by a nominal check that runs in linear time. Algebraic protocols in combination with polymorphism increase expressiveness and modularity by facilitating new ways of parameterizing and composing session types.
7
Koparkar, Chaitanya, Mike Rainey, Michael Vollmer, Milind Kulkarni i Ryan R. Newton. "Efficient tree-traversals: reconciling parallelism and dense data representations". Proceedings of the ACM on Programming Languages 5, ICFP (22.08.2021): 1–29. http://dx.doi.org/10.1145/3473596.
Pełny tekst źródłaStreszczenie:
Recent work showed that compiling functional programs to use dense, serialized memory representations for recursive algebraic datatypes can yield significant constant-factor speedups for sequential programs. But serializing data in a maximally dense format consequently serializes the processing of that data, yielding a tension between density and parallelism. This paper shows that a disciplined, practical compromise is possible. We present Parallel Gibbon, a compiler that obtains the benefits of dense data formats and parallelism. We formalize the semantics of the parallel location calculus underpinning this novel implementation strategy, and show that it is type-safe. Parallel Gibbon exceeds the parallel performance of existing compilers for purely functional programs that use recursive algebraic datatypes, including, notably, abstract-syntax-tree traversals as in compilers.
8
Zaiser, Fabian, i C. H. Luke Ong. "The Extended Theory of Trees and Algebraic (Co)datatypes". Electronic Proceedings in Theoretical Computer Science 320 (7.08.2020): 167–96. http://dx.doi.org/10.4204/eptcs.320.14.
Pełny tekst źródła
9
Shah, Amar, Federico Mora i Sanjit A. Seshia. "An Eager Satisfiability Modulo Theories Solver for Algebraic Datatypes". Proceedings of the AAAI Conference on Artificial Intelligence 38, nr 8 (24.03.2024): 8099–107. http://dx.doi.org/10.1609/aaai.v38i8.28649.
Pełny tekst źródłaStreszczenie:
Algebraic data types (ADTs) are a construct classically found in functional programming languages that capture data structures like enumerated types, lists, and trees. In recent years, interest in ADTs has increased. For example, popular programming languages, like Python, have added support for ADTs. Automated reasoning about ADTs can be done using satisfiability modulo theories (SMT) solving, an extension of the Boolean satisfiability problem with first-order logic and associated background theories. Unfortunately, SMT solvers that support ADTs do not scale as state-of-the-art approaches all use variations of the same lazy approach. In this paper, we present an SMT solver that takes a fundamentally different approach, an eager approach. Specifically, our solver reduces ADT queries to a simpler logical theory, uninterpreted functions (UF), and then uses an existing solver on the reduced query. We prove the soundness and completeness of our approach and demonstrate that it outperforms the state of the art on existing benchmarks, as well as a new, more challenging benchmark set from the planning domain.
10
TASSON, CHRISTINE, i LIONEL VAUX. "Transport of finiteness structures and applications". Mathematical Structures in Computer Science 28, nr 7 (5.12.2016): 1061–96. http://dx.doi.org/10.1017/s0960129516000384.
Pełny tekst źródłaStreszczenie:
We describe a general construction of finiteness spaces which subsumes the interpretations of all positive connectors of linear logic. We then show how to apply this construction to prove the existence of least fixpoints for particular functors in the category of finiteness spaces: These include the functors involved in a relational interpretation of lazy recursive algebraic datatypes along the lines of the coherence semantics of system T.
11
Blanchette, Jasmin Christian. "Relational analysis of (co)inductive predicates, (co)algebraic datatypes, and (co)recursive functions". Software Quality Journal 21, nr 1 (28.06.2011): 101–26. http://dx.doi.org/10.1007/s11219-011-9148-5.
Pełny tekst źródła
12
Murali, Adithya, Lucas Peña, Ranjit Jhala i P. Madhusudan. "Complete First-Order Reasoning for Properties of Functional Programs". Proceedings of the ACM on Programming Languages 7, OOPSLA2 (16.10.2023): 1063–92. http://dx.doi.org/10.1145/3622835.
Pełny tekst źródłaStreszczenie:
Several practical tools for automatically verifying functional programs (e.g., Liquid Haskell and Leon for Scala programs) rely on a heuristic based on unrolling recursive function definitions followed by quantifier-free reasoning using SMT solvers. We uncover foundational theoretical properties of this heuristic, revealing that it can be generalized and formalized as a technique that is in fact complete for reasoning with combined First-Order theories of algebraic datatypes and background theories, where background theories support decidable quantifier-free reasoning. The theory developed in this paper explains the efficacy of these heuristics when they succeed, explain why they fail when they fail, and the precise role that user help plays in making proofs succeed.
13
CHLIPALA, ADAM. "Modular development of certified program verifiers with a proof assistant",. Journal of Functional Programming 18, nr 5-6 (15.08.2008): 599–647. http://dx.doi.org/10.1017/s0956796808006904.
Pełny tekst źródłaStreszczenie:
AbstractWe report on an experience using the Coq proof assistant to develop a program verification tool with a machine-checked proof of full correctness. The verifier is able to prove memory safety of x86 machine code programs compiled from code that uses algebraic datatypes. The tool's soundness theorem is expressed in terms of the bit-level semantics of x86 programs, so its correctness depends on very few assumptions. We take advantage of Coq's support for programming with dependent types and modules in the structure of the development. The approach is based on developing a library of reusable functors for transforming a verifier at one level of abstraction into a verifier at a lower level. Using this library, it is possible to prototype a verifier based on a new type system with a minimal amount of work, while obtaining a very strong soundness theorem about the final product.
14
Winterer, Dominik, i Zhendong Su. "Validating SMT Solvers for Correctness and Performance via Grammar-Based Enumeration". Proceedings of the ACM on Programming Languages 8, OOPSLA2 (8.10.2024): 2378–401. http://dx.doi.org/10.1145/3689795.
Pełny tekst źródłaStreszczenie:
We introduce ET, a grammar-based enumerator for validating SMT solver correctness and performance. By compiling grammars of the SMT theories to algebraic datatypes, ET leverages the functional enumerator FEAT. ET is highly effective at bug finding and has many complimentary benefits. Despite the extensive and continuous testing of the state-of-the-art SMT solvers Z3 and cvc5, ET found 102 bugs, out of which 76 were confirmed and 32 were fixed. Moreover, ET can be used to understand the evolution of solvers. We derive eight grammars realizing all major SMT theories including the booleans, integers, reals, realints, bit-vectors, arrays, floating points, and strings. Using ET, we test all consecutive releases of the SMT solvers Z3 and CVC4/cvc5 from the last six years (61 versions) on 8 million formulas, and 488 million solver calls. Our results suggest improved correctness in recent versions of both solvers but decreased performance in newer releases of Z3 on small timeouts (since z3-4.8.11) and regressions in early cvc5 releases on larger timeouts. Due to its systematic testing and efficiency, we further advocate ET's use for continuous integration.
15
Chataing, Nicolas, Stephen Dolan, Gabriel Scherer i Jeremy Yallop. "Unboxed Data Constructors: Or, How cpp Decides a Halting Problem". Proceedings of the ACM on Programming Languages 8, POPL (5.01.2024): 1509–39. http://dx.doi.org/10.1145/3632893.
Pełny tekst źródłaStreszczenie:
We propose a new language feature for ML-family languages, the ability to selectively unbox certain data constructors, so that their runtime representation gets compiled away to just the identity on their argument. Unboxing must be statically rejected when it could introduce confusion, that is, distinct values with the same representation. We discuss the use-case of big numbers, where unboxing allows to write code that is both efficient and safe, replacing either a safe but slow version or a fast but unsafe version. We explain the static analysis necessary to reject incorrect unboxing requests. We present our prototype implementation of this feature for the OCaml programming language, discuss several design choices and the interaction with advanced features such as Guarded Algebraic Datatypes. Our static analysis requires expanding type definitions in type expressions, which is not necessarily normalizing in presence of recursive type definitions. In other words, we must decide normalization of terms in the first-order λ-calculus with recursion. We provide an algorithm to detect non-termination on-the-fly during reduction, with proofs of correctness and completeness. Our algorithm turns out to be closely related to the normalization strategy for macro expansion in the cpp preprocessor.
16
Zhang, Weixin, Yaozhu Sun i Bruno C. D. S. Oliveira. "Compositional Programming". ACM Transactions on Programming Languages and Systems 43, nr 3 (30.09.2021): 1–61. http://dx.doi.org/10.1145/3460228.
Pełny tekst źródłaStreszczenie:
Modularity is a key concern in programming. However, programming languages remain limited in terms of modularity and extensibility. Small canonical problems, such as the Expression Problem (EP), illustrate some of the basic issues: the dilemma between choosing one kind of extensibility over another one in most programming languages. Other problems, such as how to express dependencies in a modular way, add up to the basic issues and remain a significant challenge. This article presents a new statically typed modular programming style called Compositional Programming . In Compositional Programming, there is no EP: It is easy to get extensibility in multiple dimensions (i.e., it is easy to add new variants as well as new operations). Compositional Programming offers an alternative way to model data structures that differs from both algebraic datatypes in functional programming and conventional OOP class hierarchies. We introduce four key concepts for Compositional Programming: compositional interfaces , compositional traits , method patterns , and nested trait composition . Altogether, these concepts allow us to naturally solve challenges such as the Expression Problem, model attribute-grammar-like programs, and generally deal with modular programs with complex dependencies . We present a language design, called CP , which is proved to be type-safe, together with several examples and three case studies.
17
Rossberg, Andreas. "Mutually Iso-Recursive Subtyping". Proceedings of the ACM on Programming Languages 7, OOPSLA2 (16.10.2023): 347–73. http://dx.doi.org/10.1145/3622809.
Pełny tekst źródłaStreszczenie:
Iso-recursive types are often taken as a type-theoretic model for type recursion as present in many programming languages, e.g., classes in object-oriented languages or algebraic datatypes in functional languages. Their main advantage over an equi-recursive semantics is that they are simpler and algorithmically less expensive, which is an important consideration when the cost of type checking matters, such as for intermediate or low-level code representations, virtual machines, or runtime casts. However, a closer look reveals that iso-recursion cannot, in its standard form, efficiently express essential type system features like mutual recursion or non-uniform recursion. While it has been folklore that mutual recursion and non-uniform type parameterisation can nicely be handled by generalising to higher kinds, this encoding breaks down when combined with subtyping: the classic “Amber” rule for subtyping iso-recursive types is too weak to express mutual recursion without falling back to encodings of quadratic size. We present a foundational core calculus of iso-recursive types with declared subtyping that can express both inter- and intra-recursion subtyping without such blowup, including subtyping between constructors of higher or mixed kind. In a second step, we identify a syntactic fragment of this general calculus that allows for more efficient type checking without “deep” substitutions, by observing that higher-kinded iso-recursive types can be inserted to “guard” against unwanted β-reductions. This fragment closely resembles the structure of typical nominal subtype systems, but without requiring nominal semantics. It has been used as the basis for a proposed extension of WebAssembly with recursive types.
18
van der Rest, Cas, i Wouter Swierstra. "A completely unique account of enumeration". Proceedings of the ACM on Programming Languages 6, ICFP (29.08.2022): 411–37. http://dx.doi.org/10.1145/3547636.
Pełny tekst źródłaStreszczenie:
How can we enumerate the inhabitants of an algebraic datatype? This paper explores a datatype generic solution that works for all regular types and indexed families . The enumerators presented here are provably both complete and unique —they will eventually produce every value exactly once—and fair —they avoid bias when composing enumerators. Finally, these enumerators memoise previously enumerated values whenever possible, thereby avoiding repeatedly recomputing recursive results.
19
Bergstra, Jan. "Most General Algebraic Specifications for an Abstract Datatype of Rational Numbers". Scientific Annals of Computer Science 30, nr 1 (31.08.2020): 1–24. http://dx.doi.org/10.7561/sacs.2020.1.1.
Pełny tekst źródła
20
SCULTHORPE, NEIL, NICOLAS FRISBY i ANDY GILL. "The Kansas University rewrite engine". Journal of Functional Programming 24, nr 4 (lipiec 2014): 434–73. http://dx.doi.org/10.1017/s0956796814000185.
Pełny tekst źródłaStreszczenie:
AbstractWhen writing transformation systems, a significant amount of engineering effort goes into setting up the infrastructure needed to direct individual transformations to specific targets in the data being transformed. Strategic programming languages provide general-purpose infrastructure for this task, which the author of a transformation system can use for any algebraic data structure. The Kansas University Rewrite Engine (KURE) is a typed strategic programming language, implemented as a Haskell-embedded domain-specific language. KURE is designed to support typed transformations over typed data, and the main challenge is how to make such transformations compatible with generic traversal strategies that should operate over any type. Strategic programming in a typed setting has much in common with datatype-generic programming. Compared to other approaches to datatype-generic programming, the distinguishing feature of KURE's solution is that the user can configure the behaviour of traversals based on the location of each datum in the tree, beyond their behaviour being determined by the type of each datum. This article describes KURE's approach to assigning types to generic traversals, and the implementation of that approach. We also compare KURE, its design choices, and their consequences, with other approaches to strategic and datatype-generic programming.
21
ZAKIAN, TIMOTHY A. K., TREVOR L. MCDONELL, MATTEO CIMINI i RYAN R. NEWTON. "Ghostbuster: A tool for simplifying and converting GADTs". Journal of Functional Programming 28 (2018). http://dx.doi.org/10.1017/s0956796818000114.
Pełny tekst źródłaStreszczenie:
AbstractGeneralized Algebraic Data Types, or simply GADTs, can encode non-trivial properties in the types of the constructors. Once such properties are encoded in a datatype, however,allcode manipulating that datatype must provide proof that it maintains these properties in order to typecheck. In this paper, we take a step towardgradualizingthese obligations. We introduce a tool, Ghostbuster, that produces simplified versions of GADTs which elide selected type parameters, thereby weakening the guarantees of the simplified datatype in exchange for reducing the obligations necessary to manipulate it. Likeornaments, these simplified datatypes preserve the recursive structure of the original, but unlike ornaments, we focus on information-preserving bidirectional transformations. Ghostbuster generates type-safe conversion functions between the original and simplified datatypes, which we prove are the identity function when composed. We evaluate a prototype tool for Haskell against thousands of GADTs found on the Hackage package database, generating simpler Haskell'98 datatypes and round-trip conversion functions between the two.
22
Bergstra, Jan Aldert. "Arithmetical Datatypes, Fracterms, and the Fraction Definition Problem". Transmathematica, 30.04.2020. http://dx.doi.org/10.36285/tm.33.
Pełny tekst źródłaStreszczenie:
Datatypes and abstract datatypes are positioned as results of importing aspects of universal algebra into computer science and software engineering. It is suggested that 50 years later, by way of a transfer in the opposite direction, outcomes of research on datatypes can be made available via elementary arithmetic. This idea leads to the notions of an arithmetical signature, an arithmetical datatype and an arithmetical abstract datatype and to algebraic specifications for such entities. The area of fractions in elementary arithmetic is chosen as an application area and while taking a common meadow of rational numbers as the basis, an arithmetical datatype equipped with an absorptive element. The use of datatypes and signatures makes syntax available for giving precise definitions in cases where lack of precision is common place. Fracterm is coined as the name for a fraction when primarily understood as a syntactic entity. The main contribution of the paper is to provide a detailed terminology of fracterms. Subsequently the fraction definition problem is stated, a distinction between explicit definitions of fractions and implicit definitions of fractions is made, and an outline of a survey of both forms of definitions of the notion of a fraction is given.
23
Sheng, Ying, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine i Clark Barrett. "Polite Combination of Algebraic Datatypes". Journal of Automated Reasoning, 5.05.2022. http://dx.doi.org/10.1007/s10817-022-09625-3.
Pełny tekst źródła
24
DAGAND, PIERRE-EVARISTE. "The essence of ornaments". Journal of Functional Programming 27 (2017). http://dx.doi.org/10.1017/s0956796816000356.
Pełny tekst źródłaStreszczenie:
AbstractFunctional programmers from all horizons strive to use, and sometimes abuse, their favorite type system in order to capture the invariants of their programs. A widely used tool in that trade consists in defining finely indexed datatypes. Operationally, these types classify the programmer's data, following the ML tradition. Logically, these types enforce the program invariants in a novel manner. This new programming pattern, by which one programs over inductive definitions to account for some invariants, lead to the development of a theory of ornaments (McBride, 2011 Ornamental Algebras, Algebraic Ornaments. Unpublished). However, ornaments originate as a dependently-typed object and may thus appear rather daunting to a functional programmer of the non-dependent kind. This article aims at presenting ornaments from first-principles and, in particular, to declutter their presentation from syntactic considerations. To do so, we shall give a sufficiently abstract model of indexed datatypes by means of many-sorted signatures. In this process, we formalize our intuition that an indexed datatype is the combination of a data-structure and a data-logic. Over this abstraction of datatypes, we shall recast the definition of ornaments, effectively giving a model of ornaments. Benefiting both from the operational and abstract nature of many-sorted signatures, ornaments should appear applicable and, one hopes, of interest beyond the type-theoretic circles, case in point being languages with generalized abstract datatypes or refinement types.
25
Hamana, Makoto. "Cyclic Datatypes modulo Bisimulation based on Second-Order Algebraic Theories". Logical Methods in Computer Science Volume 13, Issue 4 (15.11.2017). https://doi.org/10.23638/lmcs-13(4:8)2017.
Pełny tekst źródłaStreszczenie:
Cyclic data structures, such as cyclic lists, in functional programming are tricky to handle because of their cyclicity. This paper presents an investigation of categorical, algebraic, and computational foundations of cyclic datatypes. Our framework of cyclic datatypes is based on second-order algebraic theories of Fiore et al., which give a uniform setting for syntax, types, and computation rules for describing and reasoning about cyclic datatypes. We extract the "fold" computation rules from the categorical semantics based on iteration categories of Bloom and Esik. Thereby, the rules are correct by construction. We prove strong normalisation using the General Schema criterion for second-order computation rules. Rather than the fixed point law, we particularly choose Bekic law for computation, which is a key to obtaining strong normalisation. We also prove the property of "Church-Rosser modulo bisimulation" for the computation rules. Combining these results, we have a remarkable decidability result of the equational theory of cyclic data and fold.Comment: 38 pages
26
Bergstra, Jan Aldert, i John V. Tucker. "Totalising Partial Algebras". Transmathematica, 28.03.2022. http://dx.doi.org/10.36285/tm.57.
Pełny tekst źródłaStreszczenie:
We will examine totalising a partial operation in a general algebra by using an absorbtive element, bottom, such as an error flag. We then focus on the simplest example of a partial operation, namely subtraction on the natural numbers: n - m is undefined whenever n < m. We examine the use of bottom in algebraic structures for the natural numbers, especially semigroups and semirings. We axiomatise this totalisation process and introduce the algebraic concept of a team, being an additive cancellative semigroup with totalised subtraction. Also, with the natural numbers in mind, we introduce the property of being generated by an iterative function, which we call a splinter. We prove a number of theorems about the algebraic specification of datatypes of natural numbers.
27
Ahrens, Benedikt, André Hirschowitz, Ambroise Lafont i Marco Maggesi. "Presentable signatures and initial semantics". Logical Methods in Computer Science Volume 17, Issue 2 (26.05.2021). https://doi.org/10.23638/lmcs-17(2:17)2021.
Pełny tekst źródłaStreszczenie:
We present a device for specifying and reasoning about syntax for datatypes, programming languages, and logic calculi. More precisely, we study a notion of "signature" for specifying syntactic constructions. In the spirit of Initial Semantics, we define the "syntax generated by a signature" to be the initial object -- if it exists -- in a suitable category of models. In our framework, the existence of an associated syntax to a signature is not automatically guaranteed. We identify, via the notion of presentation of a signature, a large class of signatures that do generate a syntax. Our (presentable) signatures subsume classical algebraic signatures (i.e., signatures for languages with variable binding, such as the pure lambda calculus) and extend them to include several other significant examples of syntactic constructions. One key feature of our notions of signature, syntax, and presentation is that they are highly compositional, in the sense that complex examples can be obtained by gluing simpler ones. Moreover, through the Initial Semantics approach, our framework provides, beyond the desired algebra of terms, a well-behaved substitution and the induction and recursion principles associated to the syntax. This paper builds upon ideas from a previous attempt by Hirschowitz-Maggesi, which, in turn, was directly inspired by some earlier work of Ghani-Uustalu-Hamana and Matthes-Uustalu. The main results presented in the paper are computer-checked within the UniMath system.
28
Bergstra, Jan A., i Alban Ponse. "Datatype defining rewrite systems for naturals and integers". Logical Methods in Computer Science Volume 17, Issue 1 (18.02.2021). https://doi.org/10.23638/lmcs-17(1:17)2021.
Pełny tekst źródłaStreszczenie:
A datatype defining rewrite system (DDRS) is an algebraic (equational) specification intended to specify a datatype. When interpreting the equations from left-to-right, a DDRS defines a term rewriting system that must be ground-complete. First we define two DDRSs for the ring of integers, each comprising twelve rewrite rules, and prove their ground-completeness. Then we introduce natural number and integer arithmetic specified according to unary view, that is, arithmetic based on a postfix unary append constructor (a form of tallying). Next we specify arithmetic based on two other views: binary and decimal notation. The binary and decimal view have as their characteristic that each normal form resembles common number notation, that is, either a digit, or a string of digits without leading zero, or the negated versions of the latter. Integer arithmetic in binary and decimal notation is based on (postfix) digit append functions. For each view we define a DDRS, and in each case the resulting datatype is a canonical term algebra that extends a corresponding canonical term algebra for natural numbers. Then, for each view, we consider an alternative DDRS based on tree constructors that yields comparable normal forms, which for that view admits expressions that are algorithmically more involved. For all DDRSs considered, ground-completeness is proven.Comment: arXiv admin note: text overlap with arXiv:1406.3280
29
Popescu, Andrei. "Rensets and Renaming-Based Recursion for Syntax with Bindings Extended Version". Journal of Automated Reasoning 67, nr 3 (5.07.2023). http://dx.doi.org/10.1007/s10817-023-09672-4.
Pełny tekst źródłaStreszczenie:
AbstractWe introduce renaming-enriched sets (rensets for short), which are algebraic structures axiomatizing fundamental properties of renaming (also known as variable-for-variable substitution) on syntax with bindings. Rensets compare favorably in some respects with the well-known foundation based on nominal sets. In particular, renaming is a more fundamental operator than the nominal swapping operator and enjoys a simpler, equationally expressed relationship with the variable-freshness predicate. Together with some natural axioms matching properties of the syntactic constructors, rensets yield a truly minimalistic characterization of $$\lambda $$ λ -calculus terms as an abstract datatype—one involving an infinite set of unconditional equations, referring only to the most fundamental term operators: the constructors and renaming. This characterization yields a recursion principle, which (similarly to the case of nominal sets) can be improved by incorporating Barendregt’s variable convention. When interpreting syntax in semantic domains, our renaming-based recursor is easier to deploy than the nominal recursor. Our results have been validated with the proof assistant Isabelle/HOL.
30
JASKELIOFF, MAURO, i RUSSELL O'CONNOR. "A representation theorem for second-order functionals". Journal of Functional Programming 25 (2015). http://dx.doi.org/10.1017/s0956796815000088.
Pełny tekst źródłaStreszczenie:
AbstractRepresentation theorems relate seemingly complex objects to concrete, more tractable ones. In this paper, we take advantage of the abstraction power of category theory and provide a datatype-generic representation theorem. More precisely, we prove a representation theorem for a wide class of second-order functionals which are polymorphic over a class of functors. Types polymorphic over a class of functors are easily representable in languages such as Haskell, but are difficult to analyse and reason about. The concrete representation provided by the theorem is easier to analyse, but it might not be as convenient to implement. Therefore, depending on the task at hand, the change of representation may prove valuable in one direction or the other. We showcase the usefulness of the representation theorem with a range of examples. Concretely, we show how the representation theorem can be used to prove that traversable functors are finitary containers, how coalgebras of a parameterised store comonad relate to very well-behaved lenses, and how algebraic effects might be implemented in a functional language.