## Friday, March 14, 2008

### 2-Level type analysis of adding names to games

-- 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 type

data Game = Game [Game] [Game] deriving (Eq,Show)

-- Abstracting Conway's data type

data PolyGame g = PolyGame [g] [g] deriving (Eq,Show)

-- Recovering Conway's data type in terms of the abstraction

newtype RGame = RGame (PolyGame RGame) deriving (Eq,Show)

-- RGame ~ Game

-- Expressions with references and values

data PolyDefRef var val = Def var (PolyDefRef var val) (PolyDefRef var val)

| Ref var

| Val val

deriving (Eq,Show)

-- Games with references and values

data DefRefGame var = DefRefGame (PolyDefRef var (PolyGame (DefRefGame var))) deriving (Eq,Show)

-- Games with references and values in which variables are quoted games

newtype QDefRefGame = QDefRefGame (DefRefGame QDefRefGame) deriving (Eq,Show)

-- Lambda terms with values

data 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 values

data GTerm var = Term var (PolyGame (GTerm var)) deriving (Eq,Show)

-- Lambda terms with games as values and variables that are quoted lambda terms

data 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

-- Sums

data 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

-- Agents

data Agent var proc = Input [var] proc

| Output [proc]

deriving (Eq,Show)

-- Processes

data Process var sum = Case sum

| Deref var

| Compose [Process var sum]

deriving (Eq,Show)

-- Processes over games

data GProcess var =

Process var (Sum var (PolyGame (GProcess var)) (Agent var (GProcess var))) deriving (Eq,Show)

-- Processes over games with quoted process for variables

newtype QGProcess = QGProcess (GProcess QGProcess) deriving (Eq,Show)

Subscribe to:
Post Comments (Atom)

## No comments:

Post a Comment