To identify the source of runtime errors, techniques such as “debug-by-execution” are widely used, e.g., steppers. Although this technique can be useful for non-runtime errors, it has been less extensively explored because of the inherent difficulties in stepping through programs with such errors. In this new ideas and emerging results paper, we focus on debugging type errors in statically typed languages. We explore “transformational debugging,” a method that transforms erroneous code to provide users with an alternative perspective on the source code, thereby facilitating the debugging process. The proposed approach comprises three phases: In the first phase, we use the error messages from the compiler's type inferencer to “freeze” parts of the program. In the second phase, the type inferencer is used to reduce the number of “frozen” parts. In the third phase, a partial evaluator evaluates the partially “frozen” program. During partial evaluation, the frozen parts are treated as dynamic and therefore remain as code without being evaluated, whereas the other parts are treated as static and are evaluated. This study proposes the generic algorithms for our debugging method and two heuristic strategies for the algorithms. We obtain promising results using a prototype for a subset of OCaml. We explore a novel avenue for debugging: Transformational debugging and partial evaluation as helpful debugging tools.

To exhaustively understand the impact of rule amendments and unforeseen cases on existing norms, it requires connecting their rule-based and case-based representations. However, those connections have not been explored in depth, especially for norms that are represented as soft constraints. This paper aims to explore the connection between constraint hierarchies and case models as representative formalisms of rule-based and case-based representations of soft-constraint norms respectively. To explore the connection, we express norm scopes and preferences in both formalisms as diagrams. Based on tightening and arranging diagrams, we found the translation of constraint hierarchies with one constraint per level into case models. This provides new insights into understanding prototypical cases made by rule-based soft-constraint norms.

Type systems are responsible for assigning types to terms in programs. That way, they enforce the actions that can be taken and can, consequently, detect type errors during compilation. However, while they are able to flag the existence of an error, they often fail to pinpoint its cause or provide a helpful error message. Thus, without adequate support, debugging this kind of errors can take a considerable amount of effort. Recently, neural network models have been developed that are able to understand programming languages and perform several downstream tasks. We argue that type error debugging can be enhanced by taking advantage of this deeper understanding of the language’s structure. In this paper, we present a technique that leverages GPT-3’s capabilities to automatically fix type errors in OCaml programs. We perform multiple source code analysis tasks to produce useful prompts that are then provided to GPT-3 to generate potential patches. Our publicly available tool, Mentat, supports multiple modes and was validated on an existing public dataset with thousands of OCaml programs. We automatically validate successful repairs by using Quickcheck to verify which generated patches produce the same output as the user-intended fixed version, achieving a 39% repair rate. In a comparative study, Mentat outperformed two other techniques in automatically fixing ill-typed OCaml programs.

This paper studies constraint hierarchies for ethical norms, which are unwritten and may be relaxed if they conflict with stronger norms. Since such ethical norms are unwritten, initial representations of ethical norms may contain errors. For correcting those errors, this paper examines fundamental revisions on constraint hierarchies for ethical norms. Although some revisions on representations for ethical norms have been suggested, revisions on constraint hierarchies for ethical norms have not been completely investigated. In this paper, we categorize two fundamental types of revisions on such constraint hierarchies, namely preference revision and content revision. We also compare effects of those revisions in the criteria of syntactic and semantic changes, which are common criteria of revisions on legal theories. From the comparison, we found that preference revision tentatively makes lower syntactic changes. However, its computation is intractable, incomplete, and potentially makes a large number of semantic changes. On the other hand, we show that content revision on constraint hierarchies can make a small number of semantic changes. However, the content revision tentatively produce a large number of syntactic changes. This comparison leads to the possibility of optimization between preference revision and content revision, which we think is an interesting future work.

When literal interpretation of statutes leads to counterintuitive consequences, judges, especially in high courts, may identify counterintuitive consequences and revise interpretation of statutes. Researchers have studied revisions for computational legal representation. Generally, studies on revision usually consider minimal revision to reflect limitation of judges' legislative power. However, those studies tend to minimize the number of operations used for changing rules rather than minimize the changes of semantics (the set of conclusions obtained from the program), which vary among cases. In this paper, we consider minimizing the changes of semantics of a rule-base written in a normal logic program. We consider that each possible fact-base (the representation of a case) has its corresponding semantics and corresponding dominant rule-base, which is a set of Horn clauses obtained from the subset of rule-base that is specific to the considered fact-base. Hence, we present a new sub type of semantics-based minimal revision called a dominant-based minimal revision. Furthermore, we present one guidance to obtain one dominant-based minimal revision by using legal debugging and Closed World Specification. We also compare the dominant-based minimal revision with the syntax-based minimal revision in Theory Distance Metric. As the syntax-based minimal revision minimizes the number of operations used for changing rules, the comparison shows that the syntax-based minimal revision may cause extra semantics changes compared to the dominant-based minimal revision, especially when the rule-base contains multiple rules for the same consequence. We discuss that such extra semantics changes can be considered as unintentional changes caused by the syntax-based minimal revision. Hence, legal reasoning systems can check with the user such extra semantics changes to confirm the user intention of changes.