K-user mailing list

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

Thank you for the explanation.


2011/11/16 Traian Florin Șerbănuță 
<tserban2 AT illinois.edu>:
> Hi Stephen,
>
> It is true that the first programs generate the same thing.  To
> explain why, I need to talk a little about where those programs come
> from.
> You see, AGENT is built from pieces, and as each piece was added,
> tests were created for it.  However, once threads were added, we added
> a mechanism to dissolve completed threads, which means that virtually
> all examples without I/O will not exhibit anything in the final
> configuration.
>
> sorry about that.  if you want to see those programs at work, try them
> in the directories from /tests/regression/
> look for the directories resembling names of modules, such as:  exp
> lambda mu imp calcc halt io
>
> best wishes,
> - traian
>
> În data de 16 noiembrie 2011, 15:55, Stephen Chang
> <stchang AT ccs.neu.edu>
>  a scris:
>> 2011/11/16 Traian Florin Șerbănuță 
>> <tserban2 AT illinois.edu>:
>>> Hi Stephen,
>>>
>>> Sorry abut that;  the agent definition on K seems outdated.  please
>>> update using either svn up  in the trunk or alternatively run the
>>> ./k-update script
>>
>> Thanks, it seems to be working now! I think I asked this already, but
>> how does one see the result of running a program? All the programs
>> seem to be generating the same output (see below). Also, is there a
>> way to view/log each rewrite step?
>>
>>
>> <T>
>>  <barrier>
>>    true
>>  </barrier>
>>  <nextAgent>
>>    1
>>  </nextAgent>
>>  <IO>
>>    <in>
>>      .
>>    </in>
>>    <out>
>>      .
>>    </out>
>>  </IO>
>>  <messages>
>>    .
>>  </messages>
>>  <waiting>
>>    .
>>  </waiting>
>>  <world>
>>    .
>>  </world>
>> </T>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>>
>>> best wishes,
>>> - traian
>>>
>>>
>>>
>>>
>>> 2011/11/16 Stephen Chang 
>>> <stchang AT ccs.neu.edu>:
>>>> Running on the virtual machine now :)
>>>>
>>>> Trying to run a program with the agent example language, but still
>>>> getting some errors. Adding --search doesn't seem to help either. Any
>>>> ideas?
>>>>
>>>>
>>>> k@KVM:~/k-shared/k-examples/languages/research/agent$
>>>>  krun programs/p1
>>>> Warning: kast reported errors or warnings:
>>>> Warning: "programCompile.maude", line 3 (mod
>>>> TEST-DO-NOT-USE-THIS-NAME): module AGENT-SYNTAX does not exist.
>>>> Warning: "programCompile.maude", line 9: bad token +.
>>>> Warning: "programCompile.maude", line 9: no parse for term.
>>>> Can't call method "getChildNodes" on an undefined value at
>>>> /home/k/k-framework/core/perl/ast.pl line 23.
>>>>
>>>> Error:
>>>> Fatal: kast returned a non-zero exit code: ExitFailure 9
>>>> Attempted command:
>>>> kast --k-definition ./agent --main-module AGENT --syntax-module
>>>> AGENT-SYNTAX 
>>>> /home/k/k-shared/k-examples/languages/research/agent/.k/krun_tmp/pgm1890.in
>>>>
>>>> k@KVM:~/k-shared/k-examples/languages/research/agent$
>>>>  krun --search programs/p1
>>>> Warning: kast reported errors or warnings:
>>>> Warning: "programCompile.maude", line 3 (mod
>>>> TEST-DO-NOT-USE-THIS-NAME): module AGENT-SYNTAX does not exist.
>>>> Warning: "programCompile.maude", line 9: bad token +.
>>>> Warning: "programCompile.maude", line 9: no parse for term.
>>>> Can't call method "getChildNodes" on an undefined value at
>>>> /home/k/k-framework/core/perl/ast.pl line 23.
>>>>
>>>> Error:
>>>> Fatal: kast returned a non-zero exit code: ExitFailure 9
>>>> Attempted command:
>>>> kast --k-definition ./agent --main-module AGENT --syntax-module
>>>> AGENT-SYNTAX 
>>>> /home/k/k-shared/k-examples/languages/research/agent/.k/krun_tmp/pgm1894.in
>>>>
>>>>
>>>>
>>>>
>>>>
>>>> On Tue, Nov 15, 2011 at 6:22 PM, Rosu, Grigore 
>>>> <grosu AT illinois.edu>
>>>>  wrote:
>>>>> 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
>>>>
>>>> _______________________________________________
>>>> k-user mailing list
>>>> k-user AT cs.uiuc.edu
>>>> http://lists.cs.uiuc.edu/mailman/listinfo/k-user
>>>>
>>>
>>
>