K-user mailing list

[David Lazar <lazar6 AT illinois.edu>]

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.

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