K-user mailing list

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