K-user mailing list

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