skip to main |
skip to sidebar
-- This code summarizes the
-- previous post. It shows that
-- for any "closed" recursive type
-- we can devise a closed extension
-- of this type embedding the type
-- as a value in the lambda
-- (or other name mgt) calculus
module Grho( Game, PolyGame, PolyDefRef, DefRefGame, QDefRefGame ,Term, GTerm, QGTerm ,Sum, Agent, Process, GProcess, QGProcess ) where-- Conway's original data typedata Game = Game [Game] [Game] deriving (Eq,Show)-- Abstracting Conway's data typedata PolyGame g = PolyGame [g] [g] deriving (Eq,Show)-- Recovering Conway's data type in terms of the abstractionnewtype RGame = RGame (PolyGame RGame) deriving (Eq,Show)-- RGame ~ Game-- Expressions with references and valuesdata PolyDefRef var val = Def var (PolyDefRef var val) (PolyDefRef var val) | Ref var | Val val deriving (Eq,Show)-- Games with references and valuesdata DefRefGame var = DefRefGame (PolyDefRef var (PolyGame (DefRefGame var))) deriving (Eq,Show)-- Games with references and values in which variables are quoted gamesnewtype QDefRefGame = QDefRefGame (DefRefGame QDefRefGame) deriving (Eq,Show)-- Lambda terms with valuesdata Term var val = Var var | Abs [var] (Term var val) | App (Term var val) [Term var val] | Value val deriving (Eq,Show)-- Lambda terms with games as valuesdata GTerm var = Term var (PolyGame (GTerm var)) deriving (Eq,Show)-- Lambda terms with games as values and variables that are quoted lambda termsdata QGTerm = GTerm QGTerm-- And the following defn's/eqns take it one step further by providing a notion of process with-- Conway games as embedded values-- Process terms with values-- Sumsdata Sum var val agent = PValue val | Locate var agent | Sum [Sum var val agent] deriving (Eq,Show)-- One of the recent observations i've had about the process calculi-- is that '0' is Ground, and as such is another place to introduce-- new Ground. Thus, we can remove the production for '0' and replace-- it with the types of values we would like processes to 'produce'; -- hence the PValue arm of the type, Sum, above. Note that this-- design choice means that we can have expressions of the form-- v1 + v2 + ... + vk + x1A1 + ... xnAn-- i am inclined to treat this as structurally equivalent to -- x1A1 + ... xnAn -- but there is another alternative: to allow -- sums of values to represent superpositions-- Agentsdata Agent var proc = Input [var] proc | Output [proc] deriving (Eq,Show)-- Processesdata Process var sum = Case sum | Deref var | Compose [Process var sum] deriving (Eq,Show)-- Processes over gamesdata GProcess var = Process var (Sum var (PolyGame (GProcess var)) (Agent var (GProcess var))) deriving (Eq,Show)-- Processes over games with quoted process for variablesnewtype QGProcess = QGProcess (GProcess QGProcess) deriving (Eq,Show)
No comments:
Post a Comment