racket - Trying to define a small language with redex -


i'm following amb tutorial redex and, @ same time, building model typed arithmetic expressions, found in pierce's types , programming languages.

i have defined syntax , type system such small language, i'm in trouble define small step semantics. before got problems, let me present definitions i've got far.

first, i've defined syntax of language.

(define-language ty-exp   [e  (ttrue)       (ffalse)       (zero)       (suc e)       (ppred e)       (iszero e)       (iff e e e)]   [t (nat)      (bool)])

next, defined type system without problems.

(define-judgment-form ty-exp   #:mode (types o)   #:contract (types e t)    [    ----------------------"t-zero"     (types (zero) (nat))   ]    [    -------------------------- "t-false"      (types (ffalse) (bool))   ]    [    -------------------------- "t-true"      (types (ttrue) (bool))   ]    [      (types e (nat))    -------------------------- "t-suc"      (types (suc e) (nat))   ]    [      (types e (nat))    -------------------------- "t-pred"      (types (ppred e) (nat))   ]    [      (types e (nat))    -------------------------- "t-iszero"      (types (iszero e) (bool))   ]    [    (types e_1 (bool))    (types e_2 t_1)    (types e_3 t_1)    -------------------------- "t-iff"    (types (iff e_1 e_2 e_3) (t_1))   ] )

as far understand, need define semantics using evaluation contexts. next step define such contexts , values language.

(define-extended-language ty-exp-ctx-val ty-exp   (c (suc c)      (ppred c)      (iszero c)      (iff c e e)      hole)   (nv (zero)       (suc nv))   (bv (ttrue)       (ffalse))   (v  (nv)       (bv)))

non-terminal c stands contexts, nv numerical values, bv boolean values , v values. using definition of values, defined function testing if expression value.

(define v? (redex-match ty-exp-ctx-val v))

using setup, tried defined operational semantics language. in pierce's book, such semantics (without evaluation contexts) follows:

e --> e' ---------------- (e-suc) suc e --> suc e'  ------------------ (e-pred-zero) pred 0 --> 0        nv e ------------------- (e-pred-succ) pred (suc e) --> e  e --> e' ------------------- (e-pred) pred e --> pred e'   -------------------- (e-iszero-zero) iszero 0 --> true  nv e ------------------------ (e-iszero-succ) iszero (suc e) --> false   e --> e' -------------------------(e-iszero) iszero e --> iszero e'  ---------------------- (e-if-true) if true e e' --> e  -----------------------(e-if-false) if false e e' --> e'  e --> e' -----------------------(e-if) if e e1 e2 --> if e' e1 e2

in order express such semantics using evaluation contexts, removed rules e-suc, e-pred, e-izero , e-if , defined rule stepping in expression context:

e --> e' --------------(e-context) e[e] --> e[e']

as far understand, don't need represent such context rule in redex. so, have defined semantics language as:

(define red   (reduction-relation    ty-exp-ctx-val    #:domain e    (--> (in-hole c (iff (ttrue) e_1 e_2))         (in-hole c e_1)         "e-if-true")    (--> (in-hole c (iff (ffalse) e_1 e_2))         (in-hole c e_2)         "e-if-false")    (--> (in-hole c (iszero (zero)))         (in-hole c (ttrue))         "e-iszero-zero")    (--> (in-hole c (iszero (suc (e))))         (in-hole c (ffalse))         (side-condition (v? (term e)))         "e-iszero-suc")    (--> (in-hole c (ppred (zero)))         (in-hole c (zero))         "e-pred-zero")    (--> (in-hole c (ppred (suc (e))))         (in-hole c (e))         (side-condition (v? (term e)))         "e-pred-suc")  ))

now, come problem: when tried execute 

(traces red (term (iif (iszero zero) ttrue ffalse)))

racket returns following error message:

 reduction-relation: relation not defined (iif (iszero (zero)) (ttrue) (ffalse))

surely, i'm doing silly, can't figure out what. me this?

after running program, see problem is.

try:

(traces red (term (iff (iszero (zero)) (ttrue) (ffalse))))

in 

(define-language ty-exp   [e  (ttrue)       (ffalse)       (zero)       (suc e)       (ppred e)       (iszero e)       (iff e e e)]   [t (nat)      (bool)])

you have parentheses around ttrue, ffalse , zero.


Comments

Post a Comment

Popular posts from this blog

android - InAppBilling registering BroadcastReceiver in AndroidManifest -

i'm implementing inapp billing in android app. works well, however, i'm trying decouple broadcast receiver activity manifest. suggestion in android's trivialdrive sample: // important: dynamically register broadcast messages updated purchases. // register receiver here instead of <receiver> in manifest // because call getpurchases() @ startup, therefore can ignore // broadcasts sent while app isn't running. // note: registering listener in activity bad idea, done here // because sample. regardless, receiver must registered after // iabhelper setup, before first call getpurchases(). currently there's class extends broadcastreceiver : public class iabbroadcastreceiver extends broadcastreceiver { /** * intent action receiver should filter for. */ public static final string action = "com.android.vending.billing.purchases_updated"; private final iabbroadcastlistener mlistener; public iabbroadcastreceiver(iabbroadcastlistener listener) { m
Read more

python Tkinter Capturing keyboard events save as one single string -

is possible store keyboard events 1 string? code below stores 1 char , prints it. card reader or bar code reader, contains collection of character/ string not 1 character @ time. goal save char pressed text variable. from tkinter import * root = tk() def key(event): text= event.char text+= event.char print ("pressed", text) def callback(event): frame.focus_set() print ("clicked at", event.x, event.y) frame = frame(root, width=100, height=100) frame.bind("<key>", key) frame.bind("<button-1>", callback) frame.pack() root.mainloop() currently, creating text variable , everytime key() function gets called, , text stores last character typed. you can define text module level variable , , use module level text inside key function - text = '' def key(event): global text text+= event.char print("pressed", text)
Read more

sql server - Why does Linq-to-SQL add unnecessary COUNT()? -

here tables: create table customer ( cid int primary key, name varchar(32) ) create table ord ( oid int primary key, cid int foreign key references customer, address varchar(20) ) here's linq-to-sql statement: var aaa = c in db.customer select new { c, o = c.ord.tolist() }; and here's inexplicable query generated linq-to-sql: select [t0].[cid] [cid], [t0].[name] [name], [t1].[oid] [oid], [t1].[cid] [cid2], [t1].[address] [address], (select count(*) [dbo].[ord] [t2] [t2].[cid] = [t0].[cid]) [value] [dbo].[customer] [t0] left outer join [dbo].[ord] [t1] on [t1].[cid] = [t0].[cid] order [t0].[cid], [t1].[oid] i want understand how rid of count(*) part. it's entirely uncalled for! linq needs count(*) in order determine number of entries returned o = c.ord.tolist() .
Read more