Skip to content

Commit a58451d

Browse files
meditansmeditans
committed
restructure examples
1 parent d32a11b commit a58451d

File tree

1 file changed

+112
-12
lines changed

1 file changed

+112
-12
lines changed

‎Experiment.agda

+112-12
Original file line numberDiff line numberDiff line change
@@ -2,22 +2,122 @@ module Experiment where
22

33
open import Study
44

5-
-- First task would be writing a term in the meta-syntax
5+
-- Preliminary study: combinators in the untyped lambda calculus
6+
-- The K combinator, as a LamTm
7+
kTm : LamTm B0
8+
kTm = lam (lam (var (oz os o')))
69

7-
-- Let's begin with the S combinator, because I can be guided by the types.
8-
-- Being a Tm, this is what I would call the de Bruijn version.
10+
-- Now the K combinator, as a LamTmR
11+
-- Why is it LamTmR / B0 and not LamTmR B0?
12+
-- λx. λy. x
13+
kTmR : LamTmR / B0
14+
kTmR = lam (oz os \\ lam (oz o' \\ var only)) ^ oz
915

10-
tyS2 : (A B C : Ty) → Tm LTyD ((A >> B >> C) >> (A >> B) >> (A >> C)) B0
11-
-- This means that I'm defining a Tm, using the description function for typed
12-
-- terms, and then I also have to give a term which is used in my interpretation
13-
-- function, and then I have to give the context I intend this term to be
14-
-- indexed with (in this case B0 as this is a closed combinator).
16+
-- Let's do the same thing for the s combinator
17+
-- s : (x >> y >> z) >> (x >> y) >> (x >> z)
18+
-- s = λf.λg.λx.f x (g x)
19+
sTm : LamTm B0
20+
sTm = lam (lam (lam ((var (oz os o' o') $ var (oz o' o' os))
21+
$(var (oz o' os o') $ var (oz o' o' os)))))
1522

16-
-- Let's recall that S = λx. λy. λz. xz(yz)
23+
sTmR : LamTmR / B0
24+
sTmR = lam (oz os \\
25+
lam (oz os \\
26+
lam (oz os \\
27+
app (pair (app (pair (var only ^ oz os o')
28+
(var only ^ oz o' os)
29+
(czz cs' c's)) ^ oz os o' os)
30+
(app (pair (var only ^ oz os o')
31+
(var only ^ oz o' os)
32+
(czz cs' c's)) ^ oz o' os os)
33+
(czz cs' c's css))))) ^ oz
1734

18-
-- So the first thing I want to construct is a lambda application, which is part
19-
-- of the syntax I intend. So I have to use the [_] operator
20-
tyS2 A B C = [ lam , [ lam , [ lam , [ app , _ , [ app , _ , oz os o' o' #$ <>
35+
-- Let's recall that S = λx. λy. λz. xz(yz)
36+
tySTm : (A B C : Ty) → Tm LTyD ((A >> B >> C) >> (A >> B) >> (A >> C)) B0
37+
tySTm A B C = [ lam , [ lam , [ lam , [ app , _ , [ app , _ , oz os o' o' #$ <>
2138
, oz o' o' os #$ <> ]
2239
, [ app , _ , oz o' os o' #$ <>
2340
, oz o' o' os #$ <> ] ] ] ] ]
41+
42+
tySTmR : (A B C : Ty) → TmR LTyD ((A >> B >> C) >> (A >> B) >> (A >> C)) B0
43+
tySTmR A B C = [ lam , oz os \\
44+
[ (lam , oz os \\
45+
[ (lam , oz os \\
46+
[ (app , B , pair
47+
( ( oz \\ [ (app , A , pair
48+
((oz \\ # (pair (only ^ oz os) (<> ^ oz o') (czz cs'))) ^ oz os o')
49+
((oz \\ # (pair (only ^ oz os) (<> ^ oz o') (czz cs'))) ^ oz o' os)
50+
(czz cs' c's)) ]) ^ oz os o' os )
51+
((oz \\ [ (app , A , pair
52+
((oz \\ # (pair (only ^ oz os) (<> ^ oz o') (czz cs'))) ^ oz os o')
53+
((oz \\ # ((pair (only ^ oz os) (<> ^ oz o') (czz cs')))) ^ oz o' os)
54+
(czz cs' c's)) ]) ^ oz o' os os)
55+
(czz cs' c's css)) ]) ]) ] ]
56+
57+
-- Now a simpler example, λx.(λy.y)x
58+
ex2Tm : (A : Ty) → Tm LTyD (A >> A) B0
59+
ex2Tm A = [ lam , [ app , _ , [ lam , oz o' os #$ <> ] , oz os #$ <> ] ]
60+
61+
-- The same example, written as a TmR
62+
ex2TmR : (A : Ty) → TmR LTyD (A >> A) B0
63+
ex2TmR A = [ lam , oz os \\ [ app , A , pair
64+
((oz \\ [ lam , oz os \\ # (pair (only ^ oz os) (<> ^ oz o') (czz cs')) ]) ^ oz o')
65+
((oz \\ # (pair (only ^ oz os) (<> ^ oz o') (czz cs'))) ^ oz os)
66+
(czz c's) ] ]
67+
68+
69+
--------------------------------------------------------------------------------
70+
-- Experiments with substitutions
71+
--------------------------------------------------------------------------------
72+
73+
-- What would be a great term to toy with substitution?
74+
-- We'd like a term with which we can implement a language
75+
76+
-- The same example as before, written with concrete types
77+
ex2TmRConc : TmR LTyD (base >> base) B0
78+
ex2TmRConc = [ lam , oz os \\
79+
[ app , base , pair
80+
((oz \\ [ lam , oz os \\ # (pair (only ^ oz os) (<> ^ oz o') (czz cs')) ]) ^ oz o')
81+
((oz \\ # (pair (only ^ oz os) (<> ^ oz o') (czz cs'))) ^ oz os)
82+
(czz c's) ] ]
83+
84+
-- So what would we need to perform the substitution in this term? To do the
85+
-- application (λy.y)x, we'd actually want to substitute the y in the body with
86+
-- the x. How would this be said in this framework?
87+
88+
s : HSub LTyD (B0 - (B0 => base)) (B0 - (B0 => base)) (B0 - (B0 => base))
89+
s = record
90+
{ pass = B0
91+
; act = B0 - (B0 => base)
92+
; passive = oz o'
93+
; active = oz os
94+
; parti = czz c's
95+
; passTrg = oz o'
96+
; actBnd = oz os
97+
; images = B0 - ((oz \\ # (pair (only ^ oz os) (<> ^ oz o') (czz cs'))) ^ oz os)
98+
}
99+
100+
-- How can I write the whole evaluation process?
101+
102+
-- Something like
103+
-- ev : ∀{a ctx} → TmR LTyD a ctx → TmR LTyD a ctx
104+
-- ev (# x) = # x
105+
-- ev [ app , tgtType , pair ((x \\ # x₁) ^ thinning) t2 cover ] =
106+
-- [ app , tgtType , pair ((x \\ # x₁) ^ thinning) ({!ev t2!} ^ _) cover ]
107+
-- ev [ app , tgtType , pair ((x \\ [ x₁ ]) ^ thinning) t2 cover ] = {!!}
108+
-- ev [ lam , snd ] = {!!}
109+
110+
111+
-- ev : ∀{a ctx} → TmR LTyD a / ctx → TmR LTyD a / ctx
112+
-- ev (# x ^ thinning) = # x ^ thinning
113+
-- ev ([ app , t2Type , pair ((x \\ # x₁) ^ thinning₁) ((oz \\ x₃) ^ thinning₂) cover ] ^ thinning) = {!!}
114+
-- -- = [ app , t2Type , pair ((x \\ # x₁) ^ thinning₁) {!t2!} {!!} ] ^ {!!}
115+
-- ev ([ app , t2Type , pair ((x \\ [ x₁ ]) ^ thinning₁) t2 cover ] ^ thinning) = {!!}
116+
-- ev ([ lam , snd ] ^ thinning) = {!!}
117+
118+
ev : ∀{a ctx} → TmR LTyD a ctx → TmR LTyD a / ctx
119+
ev (# x) = # x ^ oi
120+
ev [ app , t2T , pair ((oz \\ # x₁) ^ thinning) ((oz \\ x₂) ^ thinning₁) cover ] -- = {!!}
121+
= [ (app , t2T , pair {!!} {!!} {!!}) ] ^ oi
122+
ev [ app , t2T , pair ((oz \\ [ x ]) ^ thinning) t2 cover ] = {!!}
123+
ev [ lam , snd ] = {!!}

0 commit comments

Comments
 (0)