K-user mailing list

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

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