K-user mailing list

["Rosu, Grigore" <grosu AT illinois.edu>]

We have in plan to incorporate in the tool a generic means to generate fresh names that will automatically add the nextid cell for you.  Unfortunately, for the time being it needs to be added manually.

Grigore

-----Original message-----

From: Chucky Ellison <celliso2 AT illinois.edu>
To: Stephen Chang <stchang AT ccs.neu.edu>
Cc: "k-user AT cs.uiuc.edu" <k-user AT cs.uiuc.edu>
Sent: Tue, Nov 15, 2011 23:12:56 GMT+00:00
Subject: Re: [K-user] untyped lambda calculi examples missing?

It's a little weird why you need to do this, but it will work if you say:
configuration  <T> <k>$PGM:K</k> <nextId> 0 </nextId> </T>

The nextId cell is needed for the generic substitution.

On Tue, Nov 15, 2011 at 4:02 PM, Stephen Chang <stchang AT ccs.neu.edu> wrote:
> Thank you very much for the pointers everyone. I appreciate all the
> assistance I've received from this list. I'm sorry to be so slow to
> figure things out.
>
>
> So it seems like this should be sufficient to get a call-by-value
> lambda calculus:
>
>
> (in file cbv.k)
>
> require /modules/lambda
>
> module CBV imports LAMBDA
>
>  configuration  <T> <k>$PGM:K</k> </T>
>
> end module
>
>
>
>
> but when I try to compile, I get this error:
>
> stchang@caprica:~/NEU_Research/betaneed/K$ kompile cbv.k
> [ERROR] Error: /home/stchang/k-framework/modules/substitution.k:25-28
> Compilation phase: CONTEXT-TRANSFORMERS Reason: Cell nextId is not at
> the right level in the configuration. Check the initial configuration
> for the definition matches the rule.  Trm:
> <_>_</_>(nextId,_=>_(_`(_`)(#_(N:#Nat),.List`{K`}),_`(_`)(#_(sNat_(N:#Nat)),.List`{K`})),nextId)        Context:
> __(<_>_...</_>(k,_=>_(_`(_`)(beta`[_/_`](K:K,Y:#Id),_`(_`)('`[_`]_,_`,`,_(_`(_`)(#_(X:#Id),.List`{K`}),K':K))),_`(_`)(visitedL`(_`)('`[_`]_),_`(_`)('_visitedL`(`,`,`)_,_`,`,_(_`(_`)('visitedK_,_`(_`)(kList("wklist_"),_`(_`)(#_(id_(N:#Nat)),.List`{K`}))),_`(_`)('eval_`,then`apply`[_/_`],_`,`,_(_`(_`)('beta_`[_/_`],_`,`,_(K':K,_`,`,_(_`(_`)(#_(id_(N:#Nat)),.List`{K`}),_`(_`)(#_(X:#Id),.List`{K`})))),_`,`,_(K:K,_`(_`)(#_(Y:#Id),.List`{K`})))))))),k),<_>_</_>(nextId,_=>_(_`(_`)(#_(N:#Nat),.List`{K`}),_`(_`)(#_(sNat_(N:#Nat)),.List`{K`})),nextId))
> Check .k/kompile_errYT_kvKadNY.txt to find all errors.
> Aborting the compilation
>
>
>
>
>
>
>
> 2011/11/15 Traian Florin Șerbănuță <tserban2 AT illinois.edu>:
>> I think Agent is updated to the last version, yes.
>>
>> Stephen, you can take a look at AGENT in
>> examples/languages/research/agent
>>
>> Agent is built from small pieces, which are all under the `modules'
>> directory from the trunk.  I think the lambda and mu modules can give
>> you an idea about how we use substitution, but you can use AGENT as an
>> example of a non-trivial substitution based language.
>>
>> best wishes,
>> - traian
>>
>>
>> 2011/11/15 Rosu, Grigore <grosu AT illinois.edu>:
>>>
>>> You can also take a look at Agent.  Traian, is Agent updated to the latest
>>> version of the tool?
>>>
>>> Grigore
>>>
>>> -----Original message-----
>>>
>>> From: Stephen Chang <stchang AT ccs.neu.edu>
>>> To: "Lazar, David" <lazar6 AT illinois.edu>
>>> Cc: "k-user AT cs.uiuc.edu" <k-user AT cs.uiuc.edu>
>>> Sent: Tue, Nov 15, 2011 20:53:37 GMT+00:00
>>> Subject: Re: [K-user] untyped lambda calculi examples missing?
>>>
>>> On Tue, Nov 15, 2011 at 3:51 PM, David Lazar <lazar6 AT illinois.edu> wrote:
>>>> We provide substitution as a module you can just import, so you don't
>>>> need to write all of those rules yourself. This module is located in
>>>> modules/substitution.k.
>>>>
>>>> The simply-typed definition doesn't take advantage of this module
>>>> (although it should).
>>>>
>>>> The lambda module (located in modules/lambda.k) does take advantage of
>>>> the substitution module. You can copy the (fairly clear) code in
>>>> modules/lambda.k to add lambda to your definition.
>>>
>>> Cool, thanks! I will check it out.
>>>
>>>
>>>
>>>
>>>>
>>>> Cheers,
>>>> David
>>>>
>>>> On Tue, Nov 15, 2011 at 2:37 PM, Stephen Chang <stchang AT ccs.neu.edu>
>>>> wrote:
>>>>> On Tue, Nov 15, 2011 at 3:22 PM, David Lazar <lazar6 AT illinois.edu> wrote:
>>>>>> Stephen,
>>>>>>
>>>>>> This is accidental. I think someone created the directory but forgot
>>>>>> to add a definition :-).
>>>>>>
>>>>>> PCF is perhaps the closest thing we have to untyped lambda calculus.
>>>>>> The PCF definition is located in
>>>>>> examples/languages/classic/pcf/untyped. Note that this definition is
>>>>>> environment-based. If you want to create a substitution-based
>>>>>> definition, take a look at simply-typed lambda calculus and
>>>>>> modules/lambda.k.
>>>>>
>>>>> I'm looking for a substitution-based definition. I looked at the
>>>>> simply-typed example, but couldnt understand the substitution function
>>>>> :)
>>>>>
>>>>> Is there any documentation that you recommend looking at? I've read
>>>>> the JLAP paper and looked through Grigore's PL textbook draft but are
>>>>> there any more-basic guides for just the tool itself?
>>>>>
>>>>>
>>>>>
>>>>>
>>>>>>
>>>>>> Hope this helps.
>>>>>>
>>>>>> Cheers,
>>>>>> David
>>>>>>
>>>>>> On Tue, Nov 15, 2011 at 2:11 PM, Stephen Chang <stchang AT ccs.neu.edu>
>>>>>> wrote:
>>>>>>> I noticed that the directory examples/languages/classic/lambda/untyped