Author name cluster

C.-H.L. Ong

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

6 papers

1 author row

I&C Journal 2011 Journal Article

A saturation method for the modal μ-calculus over pushdown systems

M. Hague
C.-H.L. Ong

We present an algorithm for computing directly the denotation of a μ-calculus formula χ over the configuration graph of a pushdown system. Our method gives the first extension of the saturation technique to the full μ-calculus. Finite word automata are used to represent sets of pushdown configurations. Starting from an initial automaton, we perform a series of automaton manipulations which compute the denotation by recursion over the structure of the formula. We introduce notions of under-approximation (soundness) and over-approximation (completeness) that apply to automaton transitions rather than runs. Our algorithm is relatively simple and direct, and avoids an immediate exponential blow up. Finally, we show experimentally that the direct algorithm is more efficient than via a reduction to parity games.

Details DOI

TCS Journal 2006 Journal Article

Syntactic control of concurrency

D.R. Ghica
A.S. Murawski
C.-H.L. Ong

We consider a finitary procedural programming language (finite data-types, no recursion) extended with parallel composition and binary semaphores. Having first shown that may-equivalence of second-order open terms is undecidable we set out to find a framework in which decidability can be regained with minimum loss of expressivity. To that end we define an annotated type system that controls the number of concurrent threads created by terms and give a fully abstract game semantics for the notion of equivalence induced by typable terms and contexts. Finally, we show that the semantics of all typable terms, at any order and in the presence of iteration, has a regular-language representation and thus the restricted observational equivalence is decidable.

Details DOI

TCS Journal 2004 Journal Article

Games characterizing Levy–Longo trees

C.-H.L. Ong
P. Di Gianantonio

We present a simple strongly universal innocent game model for Levy–Longo trees, i. e. every point in the model is the denotation of a unique Levy–Longo tree. The observational quotient of the model then gives a universal, and hence fully abstract, model of the pure Lazy Lambda Calculus.

Details DOI

TCS Journal 2004 Journal Article

On an interpretation of safe recursion in light affine logic

A.S. Murawski
C.-H.L. Ong

We introduce a subalgebra BC − of Bellantoni and Cook's safe-recursion function algebra BC. Functions of the subalgebra have safe arguments that are non-contractible (i. e non-duplicable). We propose a definition of safe and normal variables in light affine logic (LAL), and show that BC − is the largest subalgebra that is interpretable in LAL, relative to that definition. Though BC − itself is not PF complete, there are extensions of it (by additional schemes for defining functions with safe arguments) that are, and are still interpretable in LAL and so preserve PF closure. We focus on one such which is BC − augmented by a definition-by-cases construct and a restricted form of definition-by-recursion scheme over safe arguments. As a corollary we obtain a new proof of the PF completeness of LAL.

Details DOI

TCS Journal 2003 Journal Article

Exhausting strategies, joker games and full completeness for IMLL with Unit

A.S. Murawski
C.-H.L. Ong

We present a game description of free symmetric monoidal closed categories, which can also be viewed as a fully complete model for Intuitionistic multiplicative linear logic with the tensor unit. We model the unit by a distinguished one-move game called Joker. Special rules apply to the joker move. Proofs are modelled by what we call conditionally exhausting strategies, which are deterministic and total only at positions where no joker move exists in the immediate neighbourhood, and satisfy a kind of reachability condition called P-exhaustion. We use the model to give an analysis of a counting problem in free autonomous categories which generalizes the Triple Unit Problem.

Details DOI

I&C Journal 2000 Journal Article

On Full Abstraction for PCF: I, II, and III

J.M.E. Hyland
C.-H.L. Ong

We present an order-extensional, order (or inequationally) fully abstract model for Scott's language pcf. The approach we have taken is very concrete and in nature goes back to S. C Kleene (1978, in “General Recursion Theory II, Proceedings of the 1977 Oslo Symposium, ” North-Holland, Amsterdam) and R. O. Gandy (1993, “Dialogues, Blass Games, Sequentiality for Objects of Finite Type, ” unpublished manuscript) in one tradition, and to G. Kahn and G. D. Plotkin (1993, Theoret. Comput. Sci. 121, 187–278) and G. Berry and P. -L. Curien (1982, Theoret. Comput. Sci. 20, 265–321) in another. Our model of computation is based on a kind of game in which each play consists of a dialogue of questions and answers between two players who observe the following principles of civil conversation: 1. Justification. A question is asked only if the dialogue at that point warrants it. An answer is proffered only if a question expecting it has already been asked. 2. Priority. Questions pending in a dialogue are answered on a last-asked-first-answered basis. This is equivalent to Gandy's no-dangling-question-mark condition. We analyze pcf -style computations directly in terms of partial strategies based on the information available to each player when he or she is about to move. Our players are required to play an innocent strategy: they play on the basis of their view which is that part of the history that interests them currently. Views are continually updated as the play unfolds. Hence our games are neither history-sensitive nor history-free. Rather they are view-dependent. These considerations give expression to what seems to us to be the nub of pcf -style higher-type sequentiality in a (dialogue) game-semantical setting.

Details DOI