Search

Your search keyword '"Mu, Shin-Cheng"' showing total 98 results
Start Over Author "Mu, Shin-Cheng"
98 results on '"Mu, Shin-Cheng"'

1. Bottom-up computation using trees of sublists (Functional Pearl)

Author

Mu, Shin-Cheng

Subjects
Computer Science - Programming Languages, F.3.1, D.2.4
Abstract

Some top-down problem specifications, if executed directly, may compute sub-problems repeatedly. Instead, we may want a bottom-up algorithm that stores solutions of sub-problems in a table to be reused. It can be tricky, however, to figure out how the table can be represented and efficiently maintained. We study a special case: computing a function $h$ taking lists as inputs such that $h~xs$ is defined in terms of all immediate sublists of $xs$. Richard Bird studied this problem in 2008, and presented a concise but cryptic algorithm without much explanation. We give this algorithm a proper derivation, and discover a key property that allows it to work. The algorithm builds trees that have certain shapes -- the sizes along the left spine is a diagonal in Pascal's triangle. The crucial function we derive transforms one diagonal to the next., Comment: Submitted to Journal of Functional Programming

Published
2023

2. Deriving monadic quicksort (Declarative Pearl)

Author

Mu, Shin-Cheng and Chiang, Tsung-Ju

Subjects
Computer Science - Programming Languages, Computer Science - Data Structures and Algorithms
Abstract

To demonstrate derivation of monadic programs, we present a specification of sorting using the non-determinism monad, and derive pure quicksort on lists and state-monadic quicksort on arrays. In the derivation one may switch between point-free and pointwise styles, and deploy techniques familiar to functional programmers such as pattern matching and induction on structures or on sizes. Derivation of stateful programs resembles reasoning backwards from the postcondition.

Published
2021
Full Text
View/download PDF

3. A greedy algorithm for dropping digits (Functional Pearl)

Author

Bird, Richard and Mu, Shin-Cheng

Subjects
Computer Science - Programming Languages
Abstract

Consider the puzzle: given a number, remove $k$ digits such that the resulting number is as large as possible. Various techniques were employed to derive a linear-time solution to the puzzle: predicate logic was used to justify the structure of a greedy algorithm, a dependently-typed proof assistant was used to give a constructive proof of the greedy condition, and equational reasoning was used to calculate the greedy step as well as the final, linear-time optimisation.

Published
2021

4. Longest segment of balanced parentheses -- an exercise in program inversion in a segment problem (Functional Pearl)

Author

Mu, Shin-Cheng and Chiang, Tsung-Ju

Subjects
Computer Science - Programming Languages
Abstract

Given a string of parentheses, the task is to find the longest consecutive segment that is balanced, in linear time. We find this problem interesting because it involves a combination of techniques: the usual approach for solving segment problems, and a theorem for constructing the inverse of a function -- through which we derive an instance of shift-reduce parsing.

Published
2021

5. Calculating a backtracking algorithm: an exercise in monadic program derivation

Author

Mu, Shin-Cheng

Subjects
Computer Science - Programming Languages
Abstract

Equational reasoning is among the most important tools that functional programming provides us. Curiously, relatively less attention has been paid to reasoning about monadic programs. In this report we derive a backtracking algorithm for problem specifications that use a monadic unfold to generate possible solutions, which are filtered using a $\mathit{scanl}$-like predicate. We develop theorems that convert a variation of $\mathit{scanl}$ to a $\mathit{foldr}$ that uses the state monad, as well as theorems constructing hylomorphism. The algorithm is used to solve the $n$-queens puzzle, our running example. The aim is to develop theorems and patterns useful for the derivation of monadic programs, focusing on the intricate interaction between state and non-determinism.

Published
2021

6. Equational reasoning for non-determinism monad: the case of Spark aggregation

Author

Mu, Shin-Cheng

Subjects
Computer Science - Programming Languages
Abstract

As part of the author's studies on equational reasoning for monadic programs, this report focus on non-determinism monad. We discuss what properties this monad should satisfy, what additional operators and notations can be introduced to facilitate equational reasoning about non-determinism, and put them to the test by proving a number of properties in our example problem inspired by the author's previous work on proving properties of Spark aggregation.

Published
2021

7. Type Safe Redis Queries: A Case Study of Type-Level Programming in Haskell

Author

Lai, Ting-Yan, Chuang, Tyng-Ruey, and Mu, Shin-Cheng

Subjects
Computer Science - Programming Languages
Abstract

Redis is an in-memory data structure store, often used as a database, with a Haskell interface Hedis. Redis is dynamically typed --- a key can be discarded and re-associated to a value of a different type, and a command, when fetching a value of a type it does not expect, signals a runtime error. We develop a domain-specific language that, by exploiting Haskell type-level programming techniques including indexed monad, type-level literals and closed type families, keeps track of types of values in the database and statically guarantees that type errors cannot happen for a class of Redis programs., Comment: This work is to be presented at the 2nd Workshop on Type-Driven Development (TyDe 2017), September 3, 2017, Oxford, UK. This paper is not included in the workshop proceedings published by the ACM. The authors choose to place it in the public domain

Published
2017

8. An Executable Sequential Specification for Spark Aggregation

Author

Chen, Yu-Fang, Hong, Chih-Duo, Lengál, Ondřej, Mu, Shin-Cheng, Sinha, Nishant, and Wang, Bow-Yaw

Subjects
Computer Science - Distributed, Parallel, and Cluster Computing, Computer Science - Logic in Computer Science
Abstract

Spark is a new promising platform for scalable data-parallel computation. It provides several high-level application programming interfaces (APIs) to perform parallel data aggregation. Since execution of parallel aggregation in Spark is inherently non-deterministic, a natural requirement for Spark programs is to give the same result for any execution on the same data set. We present PureSpark, an executable formal Haskell specification for Spark aggregate combinators. Our specification allows us to deduce the precise condition for deterministic outcomes from Spark aggregation. We report case studies analyzing deterministic outcomes and correctness of Spark programs., Comment: an extended version of a paper accepted at NETYS'17

Published
2017

9. Declarative Pearl: Deriving Monadic Quicksort

Author

Mu, Shin-Cheng, Chiang, Tsung-Ju, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Woeginger, Gerhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Nakano, Keisuke, editor, and Sagonas, Konstantinos, editor

Published
2020
Full Text
View/download PDF

10. Handling Local State with Global State

Author

Pauwels, Koen, Schrijvers, Tom, Mu, Shin-Cheng, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Woeginger, Gerhard, Editorial Board Member, Yung, Moti, Editorial Board Member, and Hutton, Graham, editor

Published
2019
Full Text
View/download PDF

11. Functional Pearl: Folding Polynomials of Polynomials

Author

Cheng, Chen-Mou, Hsu, Ruey-Lin, Mu, Shin-Cheng, Hutchison, David, Series Editor, Kanade, Takeo, Series Editor, Kittler, Josef, Series Editor, Kleinberg, Jon M., Series Editor, Mattern, Friedemann, Series Editor, Mitchell, John C., Series Editor, Naor, Moni, Series Editor, Pandu Rangan, C., Series Editor, Steffen, Bernhard, Series Editor, Terzopoulos, Demetri, Series Editor, Tygar, Doug, Series Editor, Weikum, Gerhard, Series Editor, Gallagher, John P., editor, and Sulzmann, Martin, editor

Published
2018
Full Text
View/download PDF

13. Functional Pearl: Nearest Shelters in Manhattan

Author

Mu, Shin-Cheng, Chen, Ting-Wei, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Kobsa, Alfred, Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, and Garrigue, Jacques, editor

Published
2014
Full Text
View/download PDF

15. Constructing List Homomorphisms from Proofs

Author

Chi, Yun-Yan, Mu, Shin-Cheng, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, and Yang, Hongseok, editor

Published
2011
Full Text
View/download PDF

16. Programming from Galois Connections

Author

Mu, Shin-Cheng, Oliveira, José Nuno, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, and de Swart, Harrie, editor

Published
2011
Full Text
View/download PDF

17. A Grammar-Based Approach to Invertible Programs

Author

Matsuda, Kazutaka, Mu, Shin-Cheng, Hu, Zhenjiang, Takeichi, Masato, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, and Gordon, Andrew D., editor

Published
2010
Full Text
View/download PDF

18. Algebra of Programming Using Dependent Types

Author

Mu, Shin-Cheng, Ko, Hsiang-Shang, Jansson, Patrik, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Audebaud, Philippe, editor, and Paulin-Mohring, Christine, editor

Published
2008
Full Text
View/download PDF

20. A Pushdown Machine for Recursive XML Processing

Author

Nakano, Keisuke, Mu, Shin-Cheng, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Dough, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, and Kobayashi, Naoki, editor

Published
2006
Full Text
View/download PDF

21. An Algebraic Approach to Bi-directional Updating

Author

Mu, Shin-Cheng, Hu, Zhenjiang, Takeichi, Masato, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Dough, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, and Chin, Wei-Ngan, editor

Published
2004
Full Text
View/download PDF

22. An Injective Language for Reversible Computation

Author

Mu, Shin-Cheng, Hu, Zhenjiang, Takeichi, Masato, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Dough, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, and Kozen, Dexter, editor

Published
2004
Full Text
View/download PDF

25. Inverting Functions as Folds

Author

Mu, Shin-Cheng, Bird, Richard, Goos, Gerhard, editor, Hartmanis, Juris, editor, van Leeuwen, Jan, editor, Boiten, Eerke A., editor, and Möller, Bernhard, editor

Published
2002
Full Text
View/download PDF

45. Programming from Galois connection : principles and applications

Author

Mu, Shin-Cheng, Oliveira, José Nuno Fonseca, and Universidade do Minho

Abstract

"Technical Report No. TR-IIS-10-009", Problem statements often resort to superlatives such as in eg. “. . . the smallest such number”, “. . . the best approximation”, “. . . the longest such list” which lead to specifications made of two parts: one defining a broad class of solutions (the easy part) and the other requesting the optimal such solution (the hard part). This paper introduces a binary relational combinator which mirrors this linguistic structure and exploits its potential for calculating programs by optimization. This applies in particular to specifications written in the form of Galois connections, in which one of the adjoints delivers the optimal solution being sought. The framework encompasses re-factoring of results previously developed by Bird and de Moor for greedy and dynamic programming, in a way which makes them less technically involved and therefore easier to understand and play with.

Published
2010

Catalog

Books, media, physical & digital resources
See catalog results