-
Solitons near avoided mode crossing in $χ^{(2)}$ nanowaveguides
Authors:
William R. Rowe,
Andrey V. Gorbach,
Dmitry V. Skryabin
Abstract:
We present a model for $χ^{(2)}$ waveguides accounting for three modes, two of which make an avoided crossing at the second harmonic wavelength. We introduce two linearly coupled pure modes and adjust the coupling to replicate the waveguide dispersion near the avoided crossing. Analysis of the nonlinear system reveals continuous wave (CW) solutions across much of the parameter-space and prevalence…
▽ More
We present a model for $χ^{(2)}$ waveguides accounting for three modes, two of which make an avoided crossing at the second harmonic wavelength. We introduce two linearly coupled pure modes and adjust the coupling to replicate the waveguide dispersion near the avoided crossing. Analysis of the nonlinear system reveals continuous wave (CW) solutions across much of the parameter-space and prevalence of its modulational instability. We also predict the existence of the avoided-crossing solitons, and study peculiarities of their dynamics and spectral properties, which include formation of a pedestal in the pulse tails and associated pronounced spectral peaks. Mapping these solitons onto the linear dispersion diagrams, we make connections between their existence and CW existence and stability. We also simulate the two-color soliton generation from a single frequency pump pulse to back up its formation and stability properties.
△ Less
Submitted 19 August, 2021;
originally announced August 2021.
-
Desk Organization: Effect of Multimodal Inputs on Spatial Relational Learning
Authors:
Ryan Rowe,
Shivam Singhal,
Daqing Yi,
Tapomayukh Bhattacharjee,
Siddhartha S. Srinivasa
Abstract:
For robots to operate in a three dimensional world and interact with humans, learning spatial relationships among objects in the surrounding is necessary. Reasoning about the state of the world requires inputs from many different sensory modalities including vision ($V$) and haptics ($H$). We examine the problem of desk organization: learning how humans spatially position different objects on a pl…
▽ More
For robots to operate in a three dimensional world and interact with humans, learning spatial relationships among objects in the surrounding is necessary. Reasoning about the state of the world requires inputs from many different sensory modalities including vision ($V$) and haptics ($H$). We examine the problem of desk organization: learning how humans spatially position different objects on a planar surface according to organizational ''preference''. We model this problem by examining how humans position objects given multiple features received from vision and haptic modalities. However, organizational habits vary greatly between people both in structure and adherence. To deal with user organizational preferences, we add an additional modality, ''utility'' ($U$), which informs on a particular human's perceived usefulness of a given object. Models were trained as generalized (over many different people) or tailored (per person). We use two types of models: random forests, which focus on precise multi-task classification, and Markov logic networks, which provide an easily interpretable insight into organizational habits. The models were applied to both synthetic data, which proved to be learnable when using fixed organizational constraints, and human-study data, on which the random forest achieved over 90% accuracy. Over all combinations of $\{H, U, V\}$ modalities, $UV$ and $HUV$ were the most informative for organization. In a follow-up study, we gauged participants preference of desk organizations by a generalized random forest organization vs. by a random model. On average, participants rated the random forest models as 4.15 on a 5-point Likert scale compared to 1.84 for the random model
△ Less
Submitted 2 August, 2021;
originally announced August 2021.
-
Raman solitons in waveguides with simultaneous quadratic and Kerr nonlinearities
Authors:
William R. Rowe,
Dmitry V. Skryabin,
Andrey V. Gorbach
Abstract:
We analyse Raman-induced self-frequency shift in two-component solitons supported by both quadratic and cubic nonlinearities. Treating Raman terms as a perturbation, we derive expressions for soliton velocity and frequency shifts of the fundamental frequency and second harmonic soliton components. We find these predictions compare well with simulations of soliton propagation. We also show that Ram…
▽ More
We analyse Raman-induced self-frequency shift in two-component solitons supported by both quadratic and cubic nonlinearities. Treating Raman terms as a perturbation, we derive expressions for soliton velocity and frequency shifts of the fundamental frequency and second harmonic soliton components. We find these predictions compare well with simulations of soliton propagation. We also show that Raman shift can cause two-component solitons to approach the boundary of their own existence and subsequently trigger soliton instabilities. In some cases these instabilities are accompanied by an almost complete transfer of power to the second harmonic, and emergence of a single-component Kerr solitonic pulse.
△ Less
Submitted 29 May, 2020;
originally announced June 2020.
-
Temporal quadratic solitons and their interaction with dispersive waves in Lithium Niobate nano-waveguides
Authors:
William R. Rowe,
Dmitry V. Skryabin,
Andrey V. Gorbach
Abstract:
We present a model of soliton propagation in waveguides with quadratic nonlinearity. Criteria for solitons to exist in such waveguides are developed and two example nano-waveguide structures are simulated as proof of concept. Interactions between quadratic solitons and dispersive waves are analysed giving predictions closely matching soliton propagation simulations. The example structures are foun…
▽ More
We present a model of soliton propagation in waveguides with quadratic nonlinearity. Criteria for solitons to exist in such waveguides are developed and two example nano-waveguide structures are simulated as proof of concept. Interactions between quadratic solitons and dispersive waves are analysed giving predictions closely matching soliton propagation simulations. The example structures are found to support five different regimes of soliton and quasi-soliton existence. Pulse propagation in these example waveguides has been simulated confirming the possibility of soliton generation at experimentally accessible powers. Simulations of multi-soliton generation, Cherenkov radiation and quasi-solitons with opposite signs of dispersion in the fundamental and second harmonic are also presented here.
△ Less
Submitted 1 August, 2019;
originally announced August 2019.
-
A Non-wellfounded, Labelled Proof System for Propositional Dynamic Logic
Authors:
Simon Docherty,
Reuben N. S. Rowe
Abstract:
We define a infinitary labelled sequent calculus for PDL, G3PDL^{\infty}. A finitarily representable cyclic system, G3PDL^ω, is then given. We show that both are sound and complete with respect to standard models of PDL and, further, that G3PDL^{\infty} is cut-free complete. We additionally investigate proof-search strategies in the cyclic system for the fragment of PDL without tests.
We define a infinitary labelled sequent calculus for PDL, G3PDL^{\infty}. A finitarily representable cyclic system, G3PDL^ω, is then given. We show that both are sound and complete with respect to standard models of PDL and, further, that G3PDL^{\infty} is cut-free complete. We additionally investigate proof-search strategies in the cyclic system for the fragment of PDL without tests.
△ Less
Submitted 16 May, 2019; v1 submitted 15 May, 2019;
originally announced May 2019.
-
Infinitary and Cyclic Proof Systems for Transitive Closure Logic
Authors:
Liron Cohen,
Reuben N. S. Rowe
Abstract:
Transitive closure logic is a known extension of first-order logic obtained by introducing a transitive closure operator. While other extensions of first-order logic with inductive definitions are a priori parametrized by a set of inductive definitions, the addition of the transitive closure operator uniformly captures all finitary inductive definitions. In this paper we present an infinitary proo…
▽ More
Transitive closure logic is a known extension of first-order logic obtained by introducing a transitive closure operator. While other extensions of first-order logic with inductive definitions are a priori parametrized by a set of inductive definitions, the addition of the transitive closure operator uniformly captures all finitary inductive definitions. In this paper we present an infinitary proof system for transitive closure logic which is an infinite descent-style counterpart to the existing (explicit induction) proof system for the logic. We show that, as for similar systems for first-order logic with inductive definitions, our infinitary system is complete for the standard semantics and subsumes the explicit system. Moreover, the uniformity of the transitive closure operator allows semantically meaningful complete restrictions to be defined using simple syntactic criteria. Consequently, the restriction to regular infinitary (i.e. cyclic) proofs provides the basis for an effective system for automating inductive reasoning.
△ Less
Submitted 28 June, 2018; v1 submitted 2 February, 2018;
originally announced February 2018.
-
Size Relationships in Abstract Cyclic Entailment Systems
Authors:
Reuben N. S. Rowe,
James Brotherston
Abstract:
A cyclic proof system generalises the standard notion of a proof as a finite tree of locally sound inferences by allowing proof objects to be potentially infinite. Regular infinite proofs can be finitely represented as graphs. To preclude spurious cyclic reasoning, cyclic proof systems come equipped with a well-founded notion of 'size' for the models that interpret their logical statements. A glob…
▽ More
A cyclic proof system generalises the standard notion of a proof as a finite tree of locally sound inferences by allowing proof objects to be potentially infinite. Regular infinite proofs can be finitely represented as graphs. To preclude spurious cyclic reasoning, cyclic proof systems come equipped with a well-founded notion of 'size' for the models that interpret their logical statements. A global soundness condition on proof objects, stated in terms of this notion of size, ensures that any non-well-founded paths in the proof object can be disregarded.
We give an abstract definition of a subclass of such cyclic proof systems: cyclic entailment systems. In this setting, we consider the problem of comparing the size of a model when interpreted in relation to the antecedent of an entailment, with that when interpreted in relation to the consequent. Specifically, we give a further condition on proof objects which ensures that models of a given entailment are always 'smaller' when interpreted with respect to the consequent than when interpreted with respect to the antecedent. Knowledge of such relationships is useful in a program verification setting.
△ Less
Submitted 13 February, 2017;
originally announced February 2017.
-
Encoding the Factorisation Calculus
Authors:
Reuben N. S. Rowe
Abstract:
Jay and Given-Wilson have recently introduced the Factorisation (or SF-) calculus as a minimal fundamental model of intensional computation. It is a combinatory calculus containing a special combinator, F, which is able to examine the internal structure of its first argument. The calculus is significant in that as well as being combinatorially complete it also exhibits the property of structural c…
▽ More
Jay and Given-Wilson have recently introduced the Factorisation (or SF-) calculus as a minimal fundamental model of intensional computation. It is a combinatory calculus containing a special combinator, F, which is able to examine the internal structure of its first argument. The calculus is significant in that as well as being combinatorially complete it also exhibits the property of structural completeness, i.e. it is able to represent any function on terms definable using pattern matching on arbitrary normal forms. In particular, it admits a term that can decide the structural equality of any two arbitrary normal forms.
Since SF-calculus is combinatorially complete, it is clearly at least as powerful as the more familiar and paradigmatic Turing-powerful computational models of Lambda Calculus and Combinatory Logic. Its relationship to these models in the converse direction is less obvious, however. Jay and Given-Wilson have suggested that SF-calculus is strictly more powerful than the aforementioned models, but a detailed study of the connections between these models is yet to be undertaken.
This paper begins to bridge that gap by presenting a faithful encoding of the Factorisation Calculus into the Lambda Calculus preserving both reduction and strong normalisation. The existence of such an encoding is a new result. It also suggests that there is, in some sense, an equivalence between the former model and the latter. We discuss to what extent our result constitutes an equivalence by considering it in the context of some previously defined frameworks for comparing computational power and expressiveness.
△ Less
Submitted 26 August, 2015;
originally announced August 2015.
-
Semantic Predicate Types and Approximation for Class-based Object Oriented Programming
Authors:
Steffen van Bakel,
Reuben N. S. Rowe
Abstract:
We apply the principles of the intersection type discipline to the study of class-based object oriented programs and; our work follows from a similar approach (in the context of Abadi and Cardelli's Varsigma-object calculus) taken by van Bakel and de'Liguoro. We define an extension of Featherweight Java, FJc and present a predicate system which we show to be sound and expressive. We also show that…
▽ More
We apply the principles of the intersection type discipline to the study of class-based object oriented programs and; our work follows from a similar approach (in the context of Abadi and Cardelli's Varsigma-object calculus) taken by van Bakel and de'Liguoro. We define an extension of Featherweight Java, FJc and present a predicate system which we show to be sound and expressive. We also show that our system provides a semantic underpinning for the object oriented paradigm by generalising the concept of approximant from the Lambda Calculus and demonstrating an approximation result: all expressions to which we can assign a predicate have an approximant that satisfies the same predicate. Crucial to this result is the notion of predicate language, which associates a family of predicates with a class.
△ Less
Submitted 21 September, 2011;
originally announced September 2011.
