NEXCEL

People

• Iliano Cervesato
• Coty Gonzalez
• Askerali Maruthullathil
• Hau-yu Wong
• Afrozul Haq
• Nalyn Sriwattanakomen

Past members

• Shikhar Kumar
• Anas Halbawi
• Lamana Mulaffer

• Iliano Cervesato, Edmund Lam and Ali Elgazar: Choreographic Compilation of Decentralized Comprehension Patterns, 10th International Web Rule Symposium — RuleML'16 (Jose Julio Alferes, Leopoldo Bertossi and Guido Governatori, editors), Springer LNCS 9718, Stony Brook, NY, 6-9 July 2016. (Best paper award)
  We develop an approach to compiling high-level specifications of distributed applications into code that is executable on individual computing nodes. The high-level language is a form of multiset rewriting augmented with comprehension patterns. It enables a programmer to describe the behavior of a distributed system as a whole rather than from the perspective of the individual nodes, thus dramatically reducing opportunities for programmer errors. It abstracts away the mechanics of communication and synchronization, resulting in concise and declarative specifications. Compilation generates low-level code in a syntactic fragment of this same formalism. This code forces the point of view of each node, and standard state-of-the-art execution techniques are applicable. It is relatively simple to show the correctness of this compilation scheme.
• Iliano Cervesato and Edmund Lam: Overlap and Independence in Multiset Comprehension Patterns, 30th International Workshop on Unification — UNIF'16 (Silvio Ghilardi and Manfred Schmidt-Schauß, editors), Porto, Portugal, 26 June 2016.
  Rule-based programming, a model of computation by which rules modify a global state by concurrently rewriting disjoint portions of it, is gaining popularity as a simple, effective, and declarative means for implementing concurrent and distributed applications. The state is often a multiset of first-order facts, with the rules specifying transformations over them. A rule consists of a head pattern which identifies a fragment of the state and a body which prescribes actions, often replacing this fragment with new facts. In this paper, we study rule interaction. Specifically, we identify conditions when two rule heads overlap by possibly targeting the same facts, which in many languages would prevent applying them concurrently — non-overlapping rules are independent and can always be executed in parallel without the risk of interference. A precise way of characterizing which rules are independent and which overlap is at the basis of numerous optimizations in the runtime of rule-based languages. It is also a useful debugging tool for programmers. We carry out this study in the context of Comingle, a rule-based language for programming mobile distributed applications. Head patterns in Comingle consist not only of partially instantiated facts, as found in most rule-based languages, but also of constraints and multiset comprehension patterns, which adds a challenging twist to our endeavor and interesting avenues of future work.
• Edmund Lam and Iliano Cervesato: Let's Unify Like Scala Pattern Matching!, 30th International Workshop on Unification — UNIF'16 (Silvio Ghilardi and Manfred Schmidt-Schauß, editors), Porto, Portugal, 26 June 2016.
  Scala's pattern matching framework supports algebraic data types. It also has an extensible system of user-definable pattern extractors. These advanced features enable the development of more complex term manipulations on top of Scala's primitive pattern matching infrastructure. In this paper, we discuss the development of a lightweight library for first-order term unification on top of this extensible pattern matching framework. Together with a set of combinators for writing unification control statements that resemble Scala pattern matching, this library serves as a basis for building more complex domain specific languages (e.g., constraint solvers, logical frameworks) that rely on unification.

• Iliano Cervesato and Edmund Lam: Modular Multiset Rewriting, 20th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning — LPAR'15 (Martin Davis, Andrei Voronkov, Annabelle McIver and Ansgar Fehnker, editors), Springer LNCS 9450, Suva, Fiji, 24-28 November.
  Rule-based languages are being used for ever more ambitious applications. As program size grows however, so does the overhead of team-based development, reusing components, and just keeping a large flat collection of rules from interfering. In this paper, we propose a module system for a small logically-motivated rule-based language. The resulting modules are nothing more than rewrite rules of a specific form, which are themselves just logic formulas. Yet, they provide some of the same features found in advanced module systems such as that of Standard ML, in particular name space separation, support for abstract data types, and parametrization (functors in ML). Our modules also offer essential features for concurrent programming such as facilities for sharing private names. This approach is directly applicable to other rule-based languages, including most forward-chaining logic programming languages and many process algebras.

• Iliano Cervesato and Edmund Lam: Modular Multiset Rewriting, 20th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning — LPAR'15 (Martin Davis, Andrei Voronkov, Annabelle McIver and Ansgar Fehnker, editors), Springer LNCS 9450, Suva, Fiji, 24-28 November.
  Rule-based languages are being used for ever more ambitious applications. As program size grows however, so does the overhead of team-based development, reusing components, and just keeping a large flat collection of rules from interfering. In this paper, we propose a module system for a small logically-motivated rule-based language. The resulting modules are nothing more than rewrite rules of a specific form, which are themselves just logic formulas. Yet, they provide some of the same features found in advanced module systems such as that of Standard ML, in particular name space separation, support for abstract data types, and parametrization (functors in ML). Our modules also offer essential features for concurrent programming such as facilities for sharing private names. This approach is directly applicable to other rule-based languages, including most forward-chaining logic programming languages and many process algebras.
• Askerali Maruthullathil, Reasoning with Relations — How do people do?, Meeting of the Minds – MoM'15, Carnegie Mellon University, Doha, Qatar, 28 April 2015.
  • Relational reasoning operations have different complexity and utilize different cognitive processing
  • This research describes two relational problem solving experiments where we looked at human performance in relational problems, involving elementary relational operations and combination of such operations
  • Operation complexity impacts performance
  • Familiarity doesn't play a significant role

• Askerali Maruthullathil, Role of problem complexity and domain familiarity in relational reasoning — A psychological perspective, Qatar Foundation Annual Research Conference 2014 – QFARC'14, Doha, Qatar, 18-19 November 2014.
  The goal of this paper is to study how people do relational reasoning, such as selecting the grade of all students in a class with GPA (Grade Point Average) greater than 3.5. Literature in the field of psychology of human reasoning offer little insight as to how people solve relational problems. We present two studies that look at human performance in relational problems that use basic relational operators. Our results present the first evidence toward the role of problem complexity on performance as determined by the accuracy and discrimination rates. We also look at the role of familiarity with tabular representation of information, as found in spreadsheets for example, and other factors for relational reasoning, and show that familiarity does not play a significant role in determining performance in relational problem solving, which we found counterintuitive.
• Iliano Cervesato: Proof-Theoretic Foundations of Indexing in Logic Programming, 9th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice – LFMTP'14, Vienna, Austria, 17 July 2014.
  Indexing is generally viewed as an implementation artifact, indispensable to speed up the execution of logic programs and theorem provers, but with little intrinsically logical about it. We show that indexing can be given a justification in proof theory on the basis of focusing and linearity. We demonstrate this approach on predicate indexing for Horn clauses and several formulations of hereditary Harrop formulas. We also show how to refine this approach to discriminate on function symbols as well.

• Iliano Cervesato, NEXCEL, a Deductive Spreadsheet, Qatar Foundation Annual Research Forum 2011 – QFARF'11, Doha, Qatar, 20 November 2011.
  Usability and usefulness have made the spreadsheet one of the most successful computing applications of all times: millions rely on it every day for anything from typing grocery lists to developing multimillion dollar budgets. One thing spreadsheets are not very good at is manipulating symbolic data and helping users make decisions based on them. By tapping into recent research in Logic Programming, Databases and Cognitive Psychology, we propose a deductive extension to the spreadsheet paradigm which addresses precisely this issue. The accompanying tool, which we call NEXCEL, is intended as an automated assistant for the daily reasoning and decision-making needs of computer users, in the same way as a spreadsheet application such as Microsoft Excel assists them every day with calculations simple and complex. Users without formal training in Logic or even Computer Science can interactively define logical rules in the same simple way as they define formulas in Excel. NEXCEL immediately evaluates these rules thereby returning lists of values that satisfy them, again just like with numerical formulas. The deductive component is seamlessly integrated into the traditional spreadsheet so that a user not only still has access to the usual functionalities, but is able to use them as part of the logical inference and, dually, to embed deductive steps in a numerical calculation.
  Under the hood, NEXCEL uses a small logic programming language inspired by Datalog to define derived relations: the target region of the spreadsheet contains a set of logical clauses in the same way that calculated cells contain a numerical formula in a traditional spreadsheet. Therefore, logical reasoning reduces to computing tables of data by evaluating Datalog-like definitions, a process that parallels the calculation of numerical formulas. Each row in the calculated relation is a tuple of values satisfying the definition for this relation, so that the evaluated table lists all such solutions, without repetitions. This linguistic extension significantly enriches the expressive power of the spreadsheet paradigm. Yet, it is provided to the user through a natural extension of the mostly excellent interfaces of modern spreadsheet applications.

Nexcel

• Demo

• A Spreadsheet for Everyday Symbolic Reasoning (I. Cervesato, 2006)
  A conference paper summarizing the features NEXCEL
• NEXCEL, a Deductive Spreadsheet (I. Cervesato, 2007)
  A journal paper describing the features NEXCEL
• A user-centred approach to functions in Excel (S. Peyton Jones, A. Blackwell, M. Burnett, 2003)
  A very well done extension of the spreadsheet paradigm with function definitions

• The probabilistic approach to human reasoning (M. Oaksford and N. Chater, 2001)
  A recent development in the cognitive science of reasoning has been the emergence of a probabilistic approach to the behaviour observed on ostensibly logical tasks. According to this approach the errors and biases documented on these tasks occur because people import their everyday uncertain reasoning strategies into the laboratory. Consequently participants' apparently irrational behaviour is the result of comparing it with an inappropriate logical standard. In this article, we contrast the probabilistic approach with other approaches to explaining rationality, and then show how it has been applied to three main areas of logical reasoning: conditional inference, Wason's selection task and syllogistic reasoning.

  TRENDS in Cognitive Sciences, 5(8) Aug. 2001

• Deductive Reasoning (P.N. Johnson-Laird, 1999)
  This chapter describes the main accounts of deductive competence, which explain what is computed in carrying out deductions. It argues that people have a modicum of competence, which is useful in daily life and a prerequisite for acquiring logical expertise. It outlines the three main sorts of theory of deductive performance, which explain how people make deductions: They rely on factual knowledge, formal rules, or mental models. It reviews recent experimental studies of deductive reasoning in order to help readers to assess these theories of performance.

  Annual Review of Psychology. 50, pp.109-135, 1999

• Conditionals: A Theory of Meaning, Pragmatics, and Inference (P.N. Johnson-Laird and R. Byrne, 2002)
  The authors outline a theory of conditionals of the form If A then C and If A then possibly C. The 2 sorts of conditional have separate core meanings that refer to sets of possibilities. Knowledge, pragmatics, and semantics can modulate these meanings. Modulation can add information about temporal and other relations between antecedent and consequent. It can also prevent the construction of possibilities to yield 10 distinct sets of possibilities to which conditionals can refer. The mental representation of a conditional normally makes explicit only the possibilities in which its antecedent is true, yielding other possibilities implicitly. Reasoners tend to focus on the explicit possibilities. The theory predicts the major phenomena of understanding and reasoning with conditionals.

  Psychological Review,109(4), pp. 646-678, 2002