K-user mailing list

[Stephen Chang <stchang AT ccs.neu.edu>]

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
>>>>>> is empty.
>>>>>>
>>>>>> Similarly, the examples are missing from the online tool:
>>>>>> https://fmse.info.uaic.ro/tools/8/
>>>>>>
>>>>>> Is this intentional or accidental? I'm trying to model an untyped
>>>>>> lambda calculus so these examples would be most useful for me.
>>>>>> _______________________________________________
>>>>>> k-user mailing list
>>>>>> k-user AT cs.uiuc.edu
>>>>>> http://lists.cs.uiuc.edu/mailman/listinfo/k-user
>>>>>>
>>>>>
>>>>
>>>
>> _______________________________________________
>> k-user mailing list
>> k-user AT cs.uiuc.edu
>> http://lists.cs.uiuc.edu/mailman/listinfo/k-user
>>
>> _______________________________________________
>> k-user mailing list
>> k-user AT cs.uiuc.edu
>> http://lists.cs.uiuc.edu/mailman/listinfo/k-user
>>
>>
>