Non-deterministic Effects in a Realizability Model

被引:0
作者
Voorneveld, Niels F. W. [1 ]
机构
[1] Univ Ljubljana, Fac Math & Phys, Ljubljana, Slovenia
关键词
Non-determinism; realizability; computability; powerdomains;
D O I
10.1016/j.entcs.2018.03.029
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
We model non-deterministic effects for Turing computability by working in the assemblies of Kleene's first partial combinatory algebra. Two methods will be discussed, one using equivalence relations on trees and one using topological descriptions of powerdomains. We describe these models for a selection of non-deterministic paradigms: angelic, demonic, convex and probabilistic. Though the first approach has a connection to traditional non-deterministic computability, the second approach works better for combining non-determinism with recursion. We establish morphisms from the tree models to the powerdomain models, which are bijective at ground type and give isomorphisms for all but the demonic case. We also see that any of the powerdomain models can be interpreted as a sub-monad of a continuation monad.
引用
收藏
页码:299 / 314
页数:16
相关论文
共 17 条
[1]  
[Anonymous], [No title captured]
[2]  
Battenfeld I., 2008, THESIS
[3]  
Battenfeld I., 2014, LOGICAL METHODS COMP, V10, P1
[4]   Observationally-induced Effects in Cartesian Closed Categories [J].
Battenfeld, Ingo .
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2012, 286 :43-56
[5]  
Downey RG, 2010, THEOR APPL COMPUT, P401, DOI 10.1007/978-0-387-68441-3
[6]  
Gierz G., 2003, CONTINUOUS LATTICES, V1st
[7]   A SMALL COMPLETE CATEGORY [J].
HYLAND, JME .
ANNALS OF PURE AND APPLIED LOGIC, 1988, 40 (02) :135-165
[8]  
HYLAND JME, 1990, P LOND MATH SOC, V60, P1
[9]  
Longley J. R., 1997, Mathematical Structures in Computer Science, V7, P469, DOI 10.1017/S0960129597002387
[10]  
Longley J. R., 1994, THESIS